Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: 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
⊢ ∀ {X_1 Y : WalkingMulticospan S.shape} (f : X_1 ⟶ Y),
    (S.index (P ⋙ F)).multicospan.map f ≫
        (match Y 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 X_1 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 f

Tactic:
rintro (a | b) (a | b) (f | f | f)

Goal state after:
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))

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)

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)

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))