-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean
theorem IsColimit.pullback_hom_ext [HasPullbacks C] [HasColimitsOfShape J C]
    [HasExactColimitsOfShape J C] {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c) {X Y : C}
    {f : X ⟶ c.pt} {g h : c.pt ⟶ Y}
    (hf : ∀ j, pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h) :
    f ≫ g = f ≫ h

Proof state:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h
j : J
⊢ { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ g =
    { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ h

Tactic:
rw [← cancel_epi (pullbackObjIso _ _ _).inv]

Result:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h
j : J
⊢ (pullbackObjIso c.ι ((Functor.const J).map f) j).inv ≫
      { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ g =
    (pullbackObjIso c.ι ((Functor.const J).map f) j).inv ≫
      { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ h

Proof state:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h
⊢ f ≫ g = f ≫ h

Tactic:
refine (hc.pullbackOfHasExactColimitsOfShape f).hom_ext (fun j => ?_)

Result:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h
j : J
⊢ { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ g =
    { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ h

Proof state:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h
j : J
⊢ (pullbackObjIso c.ι ((Functor.const J).map f) j).inv ≫
      { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ g =
    (pullbackObjIso c.ι ((Functor.const J).map f) j).inv ≫
      { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ h

Tactic:
simpa using hf j

Result:
no goals