Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ ∀ {X Y : WalkingCospan} (f : X ⟶ Y),
    (cospan (F.map (D.ι i)) (F.map (D.ι j))).map f ≫
        (Option.casesOn (motive := fun t ↦
            Y = t →
              ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj Y ≅
                (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj Y))
            Y (fun h ↦ ⋯ ▸ D.gluedIso F)
            (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom =
      (Option.casesOn (motive := fun t ↦
            X = t →
              ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj X ≅
                (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj X))
            X (fun h ↦ ⋯ ▸ D.gluedIso F)
            (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom ≫
        (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).map f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _)

Goal state after:
case none.none.id
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).map (WidePullbackShape.Hom.id none) ≫
      (Option.casesOn (motive := fun t ↦
          none = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj none ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none))
          none (fun h ↦ ⋯ ▸ D.gluedIso F)
          (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom =
    (Option.casesOn (motive := fun t ↦
          none = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj none ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none))
          none (fun h ↦ ⋯ ▸ D.gluedIso F)
          (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom ≫
      (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).map (WidePullbackShape.Hom.id none)

case some.none.term.left
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).map (WidePullbackShape.Hom.term WalkingPair.left) ≫
      (Option.casesOn (motive := fun t ↦
          none = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj none ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none))
          none (fun h ↦ ⋯ ▸ D.gluedIso F)
          (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom =
    (Option.casesOn (motive := fun t ↦
          some WalkingPair.left = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some WalkingPair.left) ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (some WalkingPair.left)))
          (some WalkingPair.left) (fun h ↦ ⋯ ▸ D.gluedIso F)
          (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom ≫
      (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).map (WidePullbackShape.Hom.term WalkingPair.left)

case some.none.term.right
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).map (WidePullbackShape.Hom.term WalkingPair.right) ≫
      (Option.casesOn (motive := fun t ↦
          none = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj none ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none))
          none (fun h ↦ ⋯ ▸ D.gluedIso F)
          (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom =
    (Option.casesOn (motive := fun t ↦
          some WalkingPair.right = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some WalkingPair.right) ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (some WalkingPair.right)))
          (some WalkingPair.right) (fun h ↦ ⋯ ▸ D.gluedIso F)
          (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom ≫
      (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).map (WidePullbackShape.Hom.term WalkingPair.right)

case some.some.id
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
val✝ : WalkingPair
⊢ (cospan (F.map (D.ι i)) (F.map (D.ι j))).map (WidePullbackShape.Hom.id (some val✝)) ≫
      (Option.casesOn (motive := fun t ↦
          some val✝ = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val✝) ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (some val✝)))
          (some val✝) (fun h ↦ ⋯ ▸ D.gluedIso F)
          (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom =
    (Option.casesOn (motive := fun t ↦
          some val✝ = t →
            ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val✝) ≅
              (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (some val✝)))
          (some val✝) (fun h ↦ ⋯ ▸ D.gluedIso F)
          (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯).hom ≫
      (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).map (WidePullbackShape.Hom.id (some val✝))