-- Mathlib/CategoryTheory/GlueData.lean
theorem ι_gluedIso_hom (i : D.J) : F.map (D.ι i) ≫ (D.gluedIso F).hom = (D.mapGlueData F).ι i

Proof state:
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 : D.J
this : HasColimit (D.mapGlueData F).diagram.multispan
⊢ (D.diagramIso F).hom.app (WalkingMultispan.right i) ≫
      colimit.ι (D.mapGlueData F).diagram.multispan (WalkingMultispan.right i) =
    (D.mapGlueData F).ι i

Tactic:
erw [Category.id_comp]

Result:
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 : D.J
this : HasColimit (D.mapGlueData F).diagram.multispan
⊢ colimit.ι (D.mapGlueData F).diagram.multispan (WalkingMultispan.right i) = (D.mapGlueData F).ι i

Proof state:
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 : D.J
this : HasColimit (D.mapGlueData F).diagram.multispan
⊢ F.map (D.ι i) ≫ (D.gluedIso F).hom = (D.mapGlueData F).ι i

Tactic:
erw [ι_preservesColimitIso_hom_assoc]

Result:
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 : D.J
this : HasColimit (D.mapGlueData F).diagram.multispan
⊢ colimit.ι (D.diagram.multispan ⋙ F) (WalkingMultispan.right i) ≫ (HasColimit.isoOfNatIso (D.diagramIso F)).hom =
    (D.mapGlueData F).ι i

Proof state:
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 : D.J
⊢ F.map (D.ι i) ≫ (D.gluedIso F).hom = (D.mapGlueData F).ι i

Tactic:
haveI : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance

Result:
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 : D.J
this : HasColimit (D.mapGlueData F).diagram.multispan
⊢ F.map (D.ι i) ≫ (D.gluedIso F).hom = (D.mapGlueData F).ι i

Proof state:
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 : D.J
this : HasColimit (D.mapGlueData F).diagram.multispan
⊢ colimit.ι (D.mapGlueData F).diagram.multispan (WalkingMultispan.right i) = (D.mapGlueData F).ι i

Tactic:
rfl

Result:
no goals

Proof state:
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 : D.J
this : HasColimit (D.mapGlueData F).diagram.multispan
⊢ colimit.ι (D.diagram.multispan ⋙ F) (WalkingMultispan.right i) ≫ (HasColimit.isoOfNatIso (D.diagramIso F)).hom =
    (D.mapGlueData F).ι i

Tactic:
rw [HasColimit.isoOfNatIso_ι_hom]

Result:
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 : D.J
this : HasColimit (D.mapGlueData F).diagram.multispan
⊢ (D.diagramIso F).hom.app (WalkingMultispan.right i) ≫
      colimit.ι (D.mapGlueData F).diagram.multispan (WalkingMultispan.right i) =
    (D.mapGlueData F).ι i