Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case left.id
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝))) ≫
      (match WalkingMultispan.left (fst✝, snd✝) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left (fst✝, snd✝) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝)))

pp: case left.fst
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.fst (fst✝, snd✝)) ≫
      (match WalkingMultispan.right ((MultispanShape.prod D.J).fst (fst✝, snd✝)) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left (fst✝, snd✝) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.fst (fst✝, snd✝))

pp: case left.snd
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.snd (fst✝, snd✝)) ≫
      (match WalkingMultispan.right ((MultispanShape.prod D.J).snd (fst✝, snd✝)) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left (fst✝, snd✝) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.snd (fst✝, snd✝))

pp: case right.id
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
a✝ : (MultispanShape.prod D.J).R
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      (match WalkingMultispan.right a✝ with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.right a✝ with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))

Tactic:
<;>

Goal state after:
case left.id
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝))) ≫
      (match WalkingMultispan.left (fst✝, snd✝) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left (fst✝, snd✝) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.left (fst✝, snd✝)))

case left.fst
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.fst (fst✝, snd✝)) ≫
      (match WalkingMultispan.right ((MultispanShape.prod D.J).fst (fst✝, snd✝)) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left (fst✝, snd✝) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.fst (fst✝, snd✝))

case left.snd
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst✝ snd✝ : D.J
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.snd (fst✝, snd✝)) ≫
      (match WalkingMultispan.right ((MultispanShape.prod D.J).snd (fst✝, snd✝)) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left (fst✝, snd✝) with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.snd (fst✝, snd✝))

case right.id
C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
a✝ : (MultispanShape.prod D.J).R
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝)) ≫
      (match WalkingMultispan.right a✝ with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.right a✝ with
        | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a))).hom ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a✝))