[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⟩
