-- Mathlib/CategoryTheory/Comma/Arrow.lean
lemma mk_eq_mk_iff {X Y X' Y' : T} (f : X ⟶ Y) (f' : X' ⟶ Y') :
    Arrow.mk f = Arrow.mk f' ↔
      ∃ (hX : X = X') (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom hY.symm

Proof state:
case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ (∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯) → mk f = mk f'

Tactic:
rintro ⟨rfl, rfl, h⟩

Result:
case mpr.intro.intro
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯
⊢ mk f = mk f'

Proof state:
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' ↔ ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
constructor

Result:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' → ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ (∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯) → mk f = mk f'

Proof state:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Tactic:
have := (eqToIso h).hom.w

Result:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
this : (𝟭 T).map (eqToIso h).hom.left ≫ (mk f').hom = (mk f).hom ≫ (𝟭 T).map (eqToIso h).hom.right
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Proof state:
case mpr.intro.intro
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = f'
⊢ mk f = mk f'

Tactic:
rw [h]

Result:
no goals

Proof state:
case mpr.intro.intro
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯
⊢ mk f = mk f'

Tactic:
simp only [eqToHom_refl, Category.comp_id, Category.id_comp] at h

Result:
case mpr.intro.intro
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = f'
⊢ mk f = mk f'

Proof state:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
this : eqToHom ⋯ ≫ f' = f ≫ eqToHom ⋯
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Tactic:
rw [reassoc_of% this, eqToHom_trans, eqToHom_refl, Category.comp_id]

Result:
no goals

Proof state:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
⊢ ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
refine ⟨congr_arg Comma.left h, congr_arg Comma.right h, ?_⟩

Result:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Proof state:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
this : (𝟭 T).map (eqToIso h).hom.left ≫ (mk f').hom = (mk f).hom ≫ (𝟭 T).map (eqToIso h).hom.right
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Tactic:
dsimp at this

Result:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
this : (eqToHom h).left ≫ f' = f ≫ (eqToHom h).right
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Proof state:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' → ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
intro h

Result:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
⊢ ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Proof state:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
this : (eqToHom h).left ≫ f' = f ≫ (eqToHom h).right
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Tactic:
rw [Comma.eqToHom_left, Comma.eqToHom_right] at this

Result:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
this : eqToHom ⋯ ≫ f' = f ≫ eqToHom ⋯
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯