-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean
theorem IsLimit.pushout_hom_ext [HasPushouts C] [HasLimitsOfShape J C]
    [HasExactLimitsOfShape J C] {F : J ⥤ C} {c : Cone F} (hc : IsLimit c) {X Y : C}
    {g h : Y ⟶ c.pt} {f : c.pt ⟶ X}
    (hf : ∀ j, g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f) :
    g ≫ f = h ≫ f

Proof state:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
j : J
⊢ (g ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j =
    (h ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j

Tactic:
rw [← cancel_mono (pushoutObjIso _ _ _).hom]

Result:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
j : J
⊢ ((g ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j) ≫
      (pushoutObjIso c.π ((Functor.const J).map f) j).hom =
    ((h ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j) ≫
      (pushoutObjIso c.π ((Functor.const J).map f) j).hom

Proof state:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
j : J
⊢ ((g ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j) ≫
      (pushoutObjIso c.π ((Functor.const J).map f) j).hom =
    ((h ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j) ≫
      (pushoutObjIso c.π ((Functor.const J).map f) j).hom

Tactic:
simpa using hf j

Result:
no goals

Proof state:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
⊢ g ≫ f = h ≫ f

Tactic:
refine (hc.pushoutOfHasExactLimitsOfShape 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✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g h : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = h ≫ f ≫ pushout.inr (c.π.app j) f
j : J
⊢ (g ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j =
    (h ≫ f) ≫ { pt := X, π := pushout.inr c.π ((Functor.const J).map f) }.π.app j