-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernel_hom_ext {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y}
    (e₁ e₂ : explicitCokernel f ⟶ Z) (h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂) :
    e₁ = e₂

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ e₁ = explicitCokernelDesc w

Tactic:
apply explicitCokernelDesc_unique

Result:
case he
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ explicitCokernelπ f ≫ e₁ = g

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂

Tactic:
have w : f ≫ g = 0 := by simp [g]

Result:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₁ = e₂

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ f ≫ g = 0

Tactic:
simp [g]

Result:
no goals

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₂ = explicitCokernelDesc w

Tactic:
apply explicitCokernelDesc_unique

Result:
case he
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ e₂ = g

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂

Tactic:
let g : Y ⟶ Z := explicitCokernelπ f ≫ e₂

Result:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ e₁ = e₂

Tactic:
rw [this]

Result:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ e₁ = explicitCokernelDesc w

Proof state:
case he
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ e₂ = g

Tactic:
rfl

Result:
no goals

Proof state:
case he
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ explicitCokernelπ f ≫ e₁ = g

Tactic:
exact h

Result:
no goals

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₁ = e₂

Tactic:
have : e₂ = explicitCokernelDesc w := by apply explicitCokernelDesc_unique; rfl

Result:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
this : e₂ = explicitCokernelDesc w
⊢ e₁ = e₂