Module: Mathlib.CategoryTheory.GlueData

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

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

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

pp: 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✝))

Tactic:
<;>

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