[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
⊢ ∀ {X_1 Y : WalkingMulticospan (index S (P ⋙ F)).fstTo (index S (P ⋙ F)).sndTo} (f : X_1 ⟶ Y),
    (MulticospanIndex.multicospan (index S (P ⋙ F))).map f ≫
        ((fun t =>
              match t with
              | WalkingMulticospan.left a =>
                eqToIso
                  (_ :
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                      (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
              | WalkingMulticospan.right b =>
                eqToIso
                  (_ :
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                      (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
            Y).hom =
      ((fun t =>
              match t with
              | WalkingMulticospan.left a =>
                eqToIso
                  (_ :
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                      (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
              | WalkingMulticospan.right b =>
                eqToIso
                  (_ :
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                      (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
            X_1).hom ≫
        (MulticospanIndex.multicospan (index S P) ⋙ F).map f
[PROOFSTEP]
rintro (a | b) (a | b) (f | f | f)
[GOAL]
case left.left.id
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
a : (index S (P ⋙ F)).L
⊢ (MulticospanIndex.multicospan (index S (P ⋙ F))).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a)) ≫
      ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.left a)).hom =
    ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.left a)).hom ≫
      (MulticospanIndex.multicospan (index S P) ⋙ F).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a))
case left.right.fst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S (P ⋙ F)).R
⊢ (MulticospanIndex.multicospan (index S (P ⋙ F))).map (WalkingMulticospan.Hom.fst b) ≫
      ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.right b)).hom =
    ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.left (MulticospanIndex.fstTo (index S (P ⋙ F)) b))).hom ≫
      (MulticospanIndex.multicospan (index S P) ⋙ F).map (WalkingMulticospan.Hom.fst b)
case left.right.snd
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S (P ⋙ F)).R
⊢ (MulticospanIndex.multicospan (index S (P ⋙ F))).map (WalkingMulticospan.Hom.snd b) ≫
      ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.right b)).hom =
    ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.left (MulticospanIndex.sndTo (index S (P ⋙ F)) b))).hom ≫
      (MulticospanIndex.multicospan (index S P) ⋙ F).map (WalkingMulticospan.Hom.snd b)
case right.right.id
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S (P ⋙ F)).R
⊢ (MulticospanIndex.multicospan (index S (P ⋙ F))).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b)) ≫
      ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.right b)).hom =
    ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.right b)).hom ≫
      (MulticospanIndex.multicospan (index S P) ⋙ F).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))
[PROOFSTEP]
all_goals aesop_cat
[GOAL]
case left.left.id
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
a : (index S (P ⋙ F)).L
⊢ (MulticospanIndex.multicospan (index S (P ⋙ F))).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a)) ≫
      ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.left a)).hom =
    ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.left a)).hom ≫
      (MulticospanIndex.multicospan (index S P) ⋙ F).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a))
[PROOFSTEP]
aesop_cat
[GOAL]
case left.right.fst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S (P ⋙ F)).R
⊢ (MulticospanIndex.multicospan (index S (P ⋙ F))).map (WalkingMulticospan.Hom.fst b) ≫
      ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.right b)).hom =
    ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.left (MulticospanIndex.fstTo (index S (P ⋙ F)) b))).hom ≫
      (MulticospanIndex.multicospan (index S P) ⋙ F).map (WalkingMulticospan.Hom.fst b)
[PROOFSTEP]
aesop_cat
[GOAL]
case left.right.snd
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S (P ⋙ F)).R
⊢ (MulticospanIndex.multicospan (index S (P ⋙ F))).map (WalkingMulticospan.Hom.snd b) ≫
      ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.right b)).hom =
    ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.left (MulticospanIndex.sndTo (index S (P ⋙ F)) b))).hom ≫
      (MulticospanIndex.multicospan (index S P) ⋙ F).map (WalkingMulticospan.Hom.snd b)
[PROOFSTEP]
aesop_cat
[GOAL]
case right.right.id
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S (P ⋙ F)).R
⊢ (MulticospanIndex.multicospan (index S (P ⋙ F))).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b)) ≫
      ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.right b)).hom =
    ((fun t =>
            match t with
            | WalkingMulticospan.left a =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.left a))
            | WalkingMulticospan.right b =>
              eqToIso
                (_ :
                  (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b) =
                    (MulticospanIndex.multicospan (index S (P ⋙ F))).obj (WalkingMulticospan.right b)))
          (WalkingMulticospan.right b)).hom ≫
      (MulticospanIndex.multicospan (index S P) ⋙ F).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
⊢ ∀ (j : WalkingMulticospan (index S P).fstTo (index S P).sndTo),
    NatTrans.app (F.mapCone (multifork S P)).π j =
      (eqToIso (_ : (F.mapCone (multifork S P)).pt = (F.mapCone (multifork S P)).pt)).hom ≫
        NatTrans.app ((Cones.postcompose (multicospanComp F P S).hom).obj (multifork S (P ⋙ F))).π j
[PROOFSTEP]
rintro (a | b)
[GOAL]
case left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
a : (index S P).L
⊢ NatTrans.app (F.mapCone (multifork S P)).π (WalkingMulticospan.left a) =
    (eqToIso (_ : (F.mapCone (multifork S P)).pt = (F.mapCone (multifork S P)).pt)).hom ≫
      NatTrans.app ((Cones.postcompose (multicospanComp F P S).hom).obj (multifork S (P ⋙ F))).π
        (WalkingMulticospan.left a)
[PROOFSTEP]
dsimp
[GOAL]
case left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
a : (index S P).L
⊢ F.map (P.map a.f.op) =
    𝟙 (F.obj (P.obj (Opposite.op X))) ≫
      F.map (P.map a.f.op) ≫ NatTrans.app (multicospanComp F P S).hom (WalkingMulticospan.left a)
[PROOFSTEP]
erw [Category.id_comp, multicospanComp_hom_app_left, eqToHom_refl, Category.comp_id]
[GOAL]
case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S P).R
⊢ NatTrans.app (F.mapCone (multifork S P)).π (WalkingMulticospan.right b) =
    (eqToIso (_ : (F.mapCone (multifork S P)).pt = (F.mapCone (multifork S P)).pt)).hom ≫
      NatTrans.app ((Cones.postcompose (multicospanComp F P S).hom).obj (multifork S (P ⋙ F))).π
        (WalkingMulticospan.right b)
[PROOFSTEP]
dsimp
[GOAL]
case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S P).R
⊢ F.map (P.map (MulticospanIndex.fstTo (index S P) b).f.op ≫ MulticospanIndex.fst (index S P) b) =
    𝟙 (F.obj (P.obj (Opposite.op X))) ≫
      (F.map (P.map (MulticospanIndex.fstTo (index S (P ⋙ F)) b).f.op) ≫ MulticospanIndex.fst (index S (P ⋙ F)) b) ≫
        NatTrans.app (multicospanComp F P S).hom (WalkingMulticospan.right b)
[PROOFSTEP]
erw [Functor.map_comp, Category.assoc, Category.id_comp, multicospanComp_hom_app_right, eqToHom_refl, Category.comp_id]
[GOAL]
case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
P : Cᵒᵖ ⥤ A
X : C
S : Cover J X
b : (index S P).R
⊢ F.map (P.map (MulticospanIndex.fstTo (index S P) b).f.op) ≫ F.map (MulticospanIndex.fst (index S P) b) =
    F.map (P.map (MulticospanIndex.fstTo (index S (P ⋙ F)) b).f.op) ≫ MulticospanIndex.fst (index S (P ⋙ F)) b
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
inst✝¹ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) G
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) H
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
⊢ IsSheaf J (P ⋙ F)
[PROOFSTEP]
rw [Presheaf.isSheaf_iff_multifork] at hP ⊢
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
inst✝¹ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) G
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) H
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
⊢ ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
[PROOFSTEP]
intro X S
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
inst✝¹ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) G
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) H
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
[PROOFSTEP]
obtain ⟨h⟩ := hP X S
[GOAL]
case intro
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
inst✝¹ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) G
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) H
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (GrothendieckTopology.Cover.multifork S P)
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
[PROOFSTEP]
replace h := isLimitOfPreserves F h
[GOAL]
case intro
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
inst✝¹ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) G
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) H
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h : IsLimit (F.mapCone (GrothendieckTopology.Cover.multifork S P))
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
[PROOFSTEP]
replace h := Limits.IsLimit.ofIsoLimit h (S.mapMultifork F P)
[GOAL]
case intro
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) F
inst✝¹ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) G
inst✝ :
  (X : C) →
    (S : GrothendieckTopology.Cover J X) →
      (P : Cᵒᵖ ⥤ A) → PreservesLimit (MulticospanIndex.multicospan (GrothendieckTopology.Cover.index S P)) H
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : GrothendieckTopology.Cover J X), Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S P))
X : C
S : GrothendieckTopology.Cover J X
h :
  IsLimit
    ((Cones.postcompose (GrothendieckTopology.Cover.multicospanComp F P S).hom).obj
      (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
⊢ Nonempty (IsLimit (GrothendieckTopology.Cover.multifork S (P ⋙ F)))
[PROOFSTEP]
exact ⟨Limits.IsLimit.postcomposeHomEquiv (S.multicospanComp F P) _ h⟩


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
hS : IsClosed J₁ S
Z : C
g : Z ⟶ Y
hg : Covers J₁ (Sieve.pullback f S) g
⊢ Covers J₁ S (g ≫ f)
[PROOFSTEP]
rwa [J₁.covers_iff, Sieve.pullback_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ IsClosed J₁ S ↔ close J₁ S = S
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ IsClosed J₁ S → close J₁ S = S
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ close J₁ S = S
[PROOFSTEP]
apply le_antisymm
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ close J₁ S ≤ S
[PROOFSTEP]
intro Y f hf
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
Y : C
f : Y ⟶ X
hf : (close J₁ S).arrows f
⊢ S.arrows f
[PROOFSTEP]
rw [← J₁.covers_iff_mem_of_isClosed h]
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
Y : C
f : Y ⟶ X
hf : (close J₁ S).arrows f
⊢ Covers J₁ S f
[PROOFSTEP]
apply hf
[GOAL]
case mp.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : IsClosed J₁ S
⊢ S ≤ close J₁ S
[PROOFSTEP]
apply J₁.le_close
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = S → IsClosed J₁ S
[PROOFSTEP]
intro e
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
e : close J₁ S = S
⊢ IsClosed J₁ S
[PROOFSTEP]
rw [← e]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
e : close J₁ S = S
⊢ IsClosed J₁ (close J₁ S)
[PROOFSTEP]
apply J₁.close_isClosed
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ close J₁ (Sieve.pullback f S) = Sieve.pullback f (close J₁ S)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ close J₁ (Sieve.pullback f S) ≤ Sieve.pullback f (close J₁ S)
[PROOFSTEP]
refine' J₁.le_close_of_isClosed (Sieve.pullback_monotone _ (J₁.le_close S)) _
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ IsClosed J₁ (Sieve.pullback f (close J₁ S))
[PROOFSTEP]
apply J₁.isClosed_pullback _ _ (J₁.close_isClosed _)
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ Sieve.pullback f (close J₁ S) ≤ close J₁ (Sieve.pullback f S)
[PROOFSTEP]
intro Z g hg
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ (close J₁ (Sieve.pullback f S)).arrows g
[PROOFSTEP]
change _ ∈ J₁ _
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ Sieve.pullback g (Sieve.pullback f S) ∈ sieves J₁ Z
[PROOFSTEP]
rw [← Sieve.pullback_comp]
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (close J₁ S)).arrows g
⊢ Sieve.pullback (g ≫ f) S ∈ sieves J₁ Z
[PROOFSTEP]
apply hg
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = ⊤ ↔ S ∈ sieves J₁ X
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ close J₁ S = ⊤ → S ∈ sieves J₁ X
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
⊢ S ∈ sieves J₁ X
[PROOFSTEP]
apply J₁.transitive (J₁.top_mem X)
[GOAL]
case mp.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⊤.arrows f → Sieve.pullback f S ∈ sieves J₁ Y
[PROOFSTEP]
intro Y f hf
[GOAL]
case mp.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ Sieve.pullback f S ∈ sieves J₁ Y
[PROOFSTEP]
change J₁.close S f
[GOAL]
case mp.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
h : close J₁ S = ⊤
Y : C
f : Y ⟶ X
hf : ⊤.arrows f
⊢ (close J₁ S).arrows f
[PROOFSTEP]
rwa [h]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ sieves J₁ X → close J₁ S = ⊤
[PROOFSTEP]
intro hS
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
⊢ close J₁ S = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
⊢ ⊤ ≤ close J₁ S
[PROOFSTEP]
intro Y f _
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves J₁ X
Y : C
f : Y ⟶ X
a✝ : ⊤.arrows f
⊢ (close J₁ S).arrows f
[PROOFSTEP]
apply J₁.pullback_stable _ hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁)
[PROOFSTEP]
intro X S hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSheafFor (Functor.closedSieves J₁) S.arrows
[PROOFSTEP]
rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows ∧
    ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows),
      Presieve.FamilyOfElements.Compatible x → ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ Presieve.IsSeparatedFor (Functor.closedSieves J₁) S.arrows
[PROOFSTEP]
rintro x ⟨M, hM⟩ ⟨N, hN⟩ hM₂ hN₂
[GOAL]
case refine'_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
⊢ { val := M, property := hM } = { val := N, property := hN }
[PROOFSTEP]
simp only [Functor.closedSieves_obj]
[GOAL]
case refine'_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
⊢ { val := M, property := hM } = { val := N, property := hN }
[PROOFSTEP]
ext Y f
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
⊢ (↑{ val := M, property := hM }).arrows f ↔ (↑{ val := N, property := hN }).arrows f
[PROOFSTEP]
dsimp only [Subtype.coe_mk]
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
⊢ M.arrows f ↔ N.arrows f
[PROOFSTEP]
rw [← J₁.covers_iff_mem_of_isClosed hM, ← J₁.covers_iff_mem_of_isClosed hN]
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
have q : ∀ ⦃Z : C⦄ (g : Z ⟶ X) (_ : S g), M.pullback g = N.pullback g := fun Z g hg =>
  congr_arg Subtype.val ((hM₂ g hg).trans (hN₂ g hg).symm)
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
have MSNS : M ⊓ S = N ⊓ S := by
  ext Z g
  rw [Sieve.inter_apply, Sieve.inter_apply]
  simp only [and_comm]
  apply and_congr_right
  intro hg
  rw [Sieve.pullback_eq_top_iff_mem, Sieve.pullback_eq_top_iff_mem, q g hg]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
⊢ M ⊓ S = N ⊓ S
[PROOFSTEP]
ext Z g
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
⊢ (M ⊓ S).arrows g ↔ (N ⊓ S).arrows g
[PROOFSTEP]
rw [Sieve.inter_apply, Sieve.inter_apply]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
⊢ M.arrows g ∧ S.arrows g ↔ N.arrows g ∧ S.arrows g
[PROOFSTEP]
simp only [and_comm]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
⊢ S.arrows g ∧ M.arrows g ↔ S.arrows g ∧ N.arrows g
[PROOFSTEP]
apply and_congr_right
[GOAL]
case h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
⊢ S.arrows g → (M.arrows g ↔ N.arrows g)
[PROOFSTEP]
intro hg
[GOAL]
case h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
Z : C
g : Z ⟶ (Opposite.op X).unop
hg : S.arrows g
⊢ M.arrows g ↔ N.arrows g
[PROOFSTEP]
rw [Sieve.pullback_eq_top_iff_mem, Sieve.pullback_eq_top_iff_mem, q g hg]
[GOAL]
case refine'_1.mk.mk.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ M f ↔ GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
constructor
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ M f → GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
intro hf
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ GrothendieckTopology.Covers J₁ N f
[PROOFSTEP]
rw [J₁.covers_iff]
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f N ∈ GrothendieckTopology.sieves J₁ Y
[PROOFSTEP]
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f (N ⊓ ?m.20423) ∈ GrothendieckTopology.sieves J₁ Y
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve (Opposite.op X).unop
[PROOFSTEP]
rw [← MSNS]
[GOAL]
case refine'_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ M f
⊢ Sieve.pullback f (M ⊓ S) ∈ GrothendieckTopology.sieves J₁ Y
[PROOFSTEP]
apply J₁.arrow_intersect f M S hf (J₁.pullback_stable _ hS)
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ GrothendieckTopology.Covers J₁ N f → GrothendieckTopology.Covers J₁ M f
[PROOFSTEP]
intro hf
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ GrothendieckTopology.Covers J₁ M f
[PROOFSTEP]
rw [J₁.covers_iff]
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f M ∈ GrothendieckTopology.sieves J₁ Y
[PROOFSTEP]
apply J₁.superset_covering (Sieve.pullback_monotone f inf_le_left)
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f (M ⊓ ?m.20633) ∈ GrothendieckTopology.sieves J₁ Y
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve (Opposite.op X).unop
[PROOFSTEP]
rw [MSNS]
[GOAL]
case refine'_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.op X).unop
hM : GrothendieckTopology.IsClosed J₁ M
N : Sieve (Opposite.op X).unop
hN : GrothendieckTopology.IsClosed J₁ N
hM₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := M, property := hM }
hN₂ : Presieve.FamilyOfElements.IsAmalgamation x { val := N, property := hN }
Y : C
f : Y ⟶ (Opposite.op X).unop
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : GrothendieckTopology.Covers J₁ N f
⊢ Sieve.pullback f (N ⊓ S) ∈ GrothendieckTopology.sieves J₁ Y
[PROOFSTEP]
apply J₁.arrow_intersect f N S hf (J₁.pullback_stable _ hS)
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ ∀ (x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows),
    Presieve.FamilyOfElements.Compatible x → ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.Compatible x
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
rw [Presieve.compatible_iff_sieveCompatible] at hx
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
let M := Sieve.bind S fun Y f hf => (x f hf).1
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
have : ∀ ⦃Y⦄ (f : Y ⟶ X) (hf : S f), M.pullback f = (x f hf).1 :=
  by
  intro Y f hf
  apply le_antisymm
  · rintro Z u ⟨W, g, f', hf', hg : (x f' hf').1 _, c⟩
    rw [Sieve.pullback_eq_top_iff_mem, ←
      show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)]
    conv_lhs => congr; congr;
      rw [← c]
        -- Porting note: Originally `simp_rw [← c]`
    rw [show (x (g ≫ f') _).1 = _ from congr_arg Subtype.val (hx f' g hf')]
    apply Sieve.pullback_eq_top_of_mem _ hg
  · apply Sieve.le_pullback_bind S fun Y f hf => (x f hf).1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
[PROOFSTEP]
intro Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M = ↑(x f hf)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f M ≤ ↑(x f hf)
[PROOFSTEP]
rintro Z u ⟨W, g, f', hf', hg : (x f' hf').1 _, c⟩
[GOAL]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ (↑(x f hf)).arrows u
[PROOFSTEP]
rw [Sieve.pullback_eq_top_iff_mem, ←
  show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)]
[GOAL]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ ↑(x (u ≫ f) (_ : S.arrows (u ≫ f))) = ⊤
[PROOFSTEP]
conv_lhs => congr; congr;
  rw [← c]
    -- Porting note: Originally `simp_rw [← c]`
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| ↑(x (u ≫ f) (_ : S.arrows (u ≫ f)))
[PROOFSTEP]
congr; congr;
  rw [← c]
    -- Porting note: Originally `simp_rw [← c]`
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| ↑(x (u ≫ f) (_ : S.arrows (u ≫ f)))
[PROOFSTEP]
congr; congr;
  rw [← c]
    -- Porting note: Originally `simp_rw [← c]`
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| ↑(x (u ≫ f) (_ : S.arrows (u ≫ f)))
[PROOFSTEP]
congr
[GOAL]
case self
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| x (u ≫ f) (_ : S.arrows (u ≫ f))
[PROOFSTEP]
congr
[GOAL]
case self.f
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| u ≫ f
[PROOFSTEP]
rw [← c]
  -- Porting note: Originally `simp_rw [← c]`
[GOAL]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ ↑(x (g ≫ f') (_ : S.arrows (g ≫ f'))) = ⊤
[PROOFSTEP]
rw [show (x (g ≫ f') _).1 = _ from congr_arg Subtype.val (hx f' g hf')]
[GOAL]
case a.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ ↑((Functor.closedSieves J₁).map g.op (x f' hf')) = ⊤
[PROOFSTEP]
apply Sieve.pullback_eq_top_of_mem _ hg
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(x f hf) ≤ Sieve.pullback f M
[PROOFSTEP]
apply Sieve.le_pullback_bind S fun Y f hf => (x f hf).1
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
⊢ ∃ t, Presieve.FamilyOfElements.IsAmalgamation x t
[PROOFSTEP]
refine' ⟨⟨_, J₁.close_isClosed M⟩, _⟩
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
⊢ Presieve.FamilyOfElements.IsAmalgamation x
    { val := GrothendieckTopology.close J₁ M,
      property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) }
[PROOFSTEP]
intro Y f hf
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₁).map f.op
      { val := GrothendieckTopology.close J₁ M,
        property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) } =
    x f hf
[PROOFSTEP]
simp only [Functor.closedSieves_obj]
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₁).map f.op
      { val := GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf)),
        property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) } =
    x f hf
[PROOFSTEP]
ext1
[GOAL]
case refine'_2.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₁).map f.op
        { val := GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf)),
          property := (_ : GrothendieckTopology.IsClosed J₁ (GrothendieckTopology.close J₁ M)) }) =
    ↑(x f hf)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (GrothendieckTopology.close J₁ (Sieve.bind S.arrows fun Y f hf => ↑(x f hf))) = ↑(x f hf)
[PROOFSTEP]
rw [← J₁.pullback_close, this _ hf]
[GOAL]
case refine'_2.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : Presieve.FamilyOfElements.SieveCompatible x
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ GrothendieckTopology.close J₁ ↑(x f hf) = ↑(x f hf)
[PROOFSTEP]
apply le_antisymm (J₁.le_close_of_isClosed le_rfl (x f hf).2) (J₁.le_close _)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
⊢ J₁ ≤ J₂
[PROOFSTEP]
intro X S hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ S ∈ GrothendieckTopology.sieves J₂ X
[PROOFSTEP]
rw [← J₂.close_eq_top_iff_mem]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ GrothendieckTopology.close J₂ S = ⊤
[PROOFSTEP]
have : J₂.IsClosed (⊤ : Sieve X) := by
  intro Y f _
  trivial
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
⊢ GrothendieckTopology.IsClosed J₂ ⊤
[PROOFSTEP]
intro Y f _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
Y : C
f : Y ⟶ X
a✝ : GrothendieckTopology.Covers J₂ ⊤ f
⊢ ⊤.arrows f
[PROOFSTEP]
trivial
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ GrothendieckTopology.close J₂ S = ⊤
[PROOFSTEP]
suffices (⟨J₂.close S, J₂.close_isClosed S⟩ : Subtype _) = ⟨⊤, this⟩
  by
  rw [Subtype.ext_iff] at this
  exact this
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this✝ : GrothendieckTopology.IsClosed J₂ ⊤
this :
  { val := GrothendieckTopology.close J₂ S,
      property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    { val := ⊤, property := this✝ }
⊢ GrothendieckTopology.close J₂ S = ⊤
[PROOFSTEP]
rw [Subtype.ext_iff] at this
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this✝ : GrothendieckTopology.IsClosed J₂ ⊤
this :
  ↑{ val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    ↑{ val := ⊤, property := this✝ }
⊢ GrothendieckTopology.close J₂ S = ⊤
[PROOFSTEP]
exact this
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ { val := GrothendieckTopology.close J₂ S,
      property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    { val := ⊤, property := this }
[PROOFSTEP]
apply (h S hS).isSeparatedFor.ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      (Functor.closedSieves J₂).map f.op
          { val := GrothendieckTopology.close J₂ S,
            property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
        (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
[PROOFSTEP]
intro Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op
      { val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
[PROOFSTEP]
simp only [Functor.closedSieves_obj]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (Functor.closedSieves J₂).map f.op
      { val := GrothendieckTopology.close J₂ S,
        property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) } =
    (Functor.closedSieves J₂).map f.op { val := ⊤, property := this }
[PROOFSTEP]
ext1
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑((Functor.closedSieves J₂).map f.op
        { val := GrothendieckTopology.close J₂ S,
          property := (_ : GrothendieckTopology.IsClosed J₂ (GrothendieckTopology.close J₂ S)) }) =
    ↑((Functor.closedSieves J₂).map f.op { val := ⊤, property := this })
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (GrothendieckTopology.close J₂ S) = Sieve.pullback f ⊤
[PROOFSTEP]
rw [Sieve.pullback_top, ← J₂.pullback_close, S.pullback_eq_top_of_mem hf, J₂.close_eq_top_iff_mem]
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
X : C
S : Sieve X
hS : S ∈ GrothendieckTopology.sieves J₁ X
this : GrothendieckTopology.IsClosed J₂ ⊤
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ⊤ ∈ GrothendieckTopology.sieves J₂ Y
[PROOFSTEP]
apply J₂.top_mem
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ ↔ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂ J₁ : GrothendieckTopology C
⊢ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
[PROOFSTEP]
intro P
[GOAL]
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂ J₁ : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type (max v u)
⊢ Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₁ P
[PROOFSTEP]
rfl
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ = J₂
[PROOFSTEP]
apply le_antisymm
[GOAL]
case mpr.a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ ≤ J₂
[PROOFSTEP]
apply le_topology_of_closedSieves_isSheaf
[GOAL]
case mpr.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₂)
[PROOFSTEP]
rw [h]
[GOAL]
case mpr.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₂)
[PROOFSTEP]
apply classifier_isSheaf
[GOAL]
case mpr.a
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₂ ≤ J₁
[PROOFSTEP]
apply le_topology_of_closedSieves_isSheaf
[GOAL]
case mpr.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₂ (Functor.closedSieves J₁)
[PROOFSTEP]
rw [← h]
[GOAL]
case mpr.a.h
C : Type u
inst✝ : Category.{v, u} C
J₁✝ J₂✝ J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁)
[PROOFSTEP]
apply classifier_isSheaf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ (fun X => {S | ↑(c X) S = ⊤}) X
⊢ Sieve.pullback f S ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
[PROOFSTEP]
rw [Set.mem_setOf_eq] at hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X Y : C
S : Sieve X
f : Y ⟶ X
hS : ↑(c X) S = ⊤
⊢ Sieve.pullback f S ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
[PROOFSTEP]
rw [Set.mem_setOf_eq, hc, hS, Sieve.pullback_top]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : S ∈ (fun X => {S | ↑(c X) S = ⊤}) X
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
⊢ R ∈ (fun X => {S | ↑(c X) S = ⊤}) X
[PROOFSTEP]
rw [Set.mem_setOf_eq] at hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
⊢ R ∈ (fun X => {S | ↑(c X) S = ⊤}) X
[PROOFSTEP]
rw [Set.mem_setOf_eq, ← (c X).idempotent, eq_top_iff, ← hS]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
⊢ ↑(c X) S ≤ ↑(c X) (↑(c X) R)
[PROOFSTEP]
apply (c X).monotone fun Y f hf => _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
⊢ ∀ (Y : C) (f : Y ⟶ X), S.arrows f → (↑(c X) R).arrows f
[PROOFSTEP]
intros Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (↑(c X) R).arrows f
[PROOFSTEP]
rw [Sieve.pullback_eq_top_iff_mem, ← hc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
hS : ↑(c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | ↑(c X) S = ⊤}) Y
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ↑(c Y) (Sieve.pullback f R) = ⊤
[PROOFSTEP]
apply hR hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ topologyOfClosureOperator (GrothendieckTopology.closureOperator J₁)
      (_ :
        ∀ (X Y : C) (f : Y ⟶ X) (S : Sieve X),
          GrothendieckTopology.close J₁ (Sieve.pullback f S) = Sieve.pullback f (GrothendieckTopology.close J₁ S)) =
    J₁
[PROOFSTEP]
ext X S
[GOAL]
case h.h.h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈
      GrothendieckTopology.sieves
        (topologyOfClosureOperator (GrothendieckTopology.closureOperator J₁)
          (_ :
            ∀ (X Y : C) (f : Y ⟶ X) (S : Sieve X),
              GrothendieckTopology.close J₁ (Sieve.pullback f S) = Sieve.pullback f (GrothendieckTopology.close J₁ S)))
        X ↔
    S ∈ GrothendieckTopology.sieves J₁ X
[PROOFSTEP]
apply GrothendieckTopology.close_eq_top_iff_mem
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
⊢ GrothendieckTopology.close (topologyOfClosureOperator c pb) S = ↑(c X) S
[PROOFSTEP]
ext Y f
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ (GrothendieckTopology.close (topologyOfClosureOperator c pb) S).arrows f ↔ (↑(c X) S).arrows f
[PROOFSTEP]
change c _ (Sieve.pullback f S) = ⊤ ↔ c _ S f
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), ↑(c Y) (Sieve.pullback f S) = Sieve.pullback f (↑(c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ ↑(c Y) (Sieve.pullback f S) = ⊤ ↔ (↑(c X) S).arrows f
[PROOFSTEP]
rw [pb, Sieve.pullback_eq_top_iff_mem]