Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: 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
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
a : S.shape.L
⊢ (S.index (P ⋙ F)).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a)) ≫
      (match WalkingMulticospan.left a with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left a with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      ((S.index P).multicospan ⋙ F).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a))

pp: 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
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
b : S.shape.R
⊢ (S.index (P ⋙ F)).multicospan.map (WalkingMulticospan.Hom.fst b) ≫
      (match WalkingMulticospan.right b with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left (S.shape.fst b) with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      ((S.index P).multicospan ⋙ F).map (WalkingMulticospan.Hom.fst b)

pp: 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
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
b : S.shape.R
⊢ (S.index (P ⋙ F)).multicospan.map (WalkingMulticospan.Hom.snd b) ≫
      (match WalkingMulticospan.right b with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left (S.shape.snd b) with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      ((S.index P).multicospan ⋙ F).map (WalkingMulticospan.Hom.snd b)

pp: 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
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
b : S.shape.R
⊢ (S.index (P ⋙ F)).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b)) ≫
      (match WalkingMulticospan.right b with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.right b with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      ((S.index P).multicospan ⋙ F).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))

Tactic:
all_goals cat_disch

Goal state after: