-- Mathlib/CategoryTheory/EffectiveEpi/Basic.lean
lemma EffectiveEpiFamily.hom_ext {B W : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B))
    [EffectiveEpiFamily X π] (m₁ m₂ : B ⟶ W) (h : ∀ a, π a ≫ m₁ = π a ≫ m₂) :
    m₁ = m₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
this : m₂ = desc X π (fun a => π a ≫ m₂) ⋯
⊢ m₁ = m₂

Tactic:
rw [this]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
this : m₂ = desc X π (fun a => π a ≫ m₂) ⋯
⊢ m₁ = desc X π (fun a => π a ≫ m₂) ⋯

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ m₂ = desc X π (fun a => π a ≫ m₂) ⋯

Tactic:
apply EffectiveEpiFamily.uniq

Result:
case hm
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ ∀ (a : α), π a ≫ m₂ = π a ≫ m₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ m₁ = m₂

Tactic:
have : m₂ = EffectiveEpiFamily.desc X π (fun a => π a ≫ m₂)
    (fun a₁ a₂ g₁ g₂ h => by simp only [← Category.assoc, h]) := by
  apply EffectiveEpiFamily.uniq; intro; rfl

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
this : m₂ = desc X π (fun a => π a ≫ m₂) ⋯
⊢ m₁ = m₂

Proof state:
case hm
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ ∀ (a : α), π a ≫ m₂ = π a ≫ m₂

Tactic:
intro

Result:
case hm
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
a✝ : α
⊢ π a✝ ≫ m₂ = π a✝ ≫ m₂

Proof state:
case hm
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
a✝ : α
⊢ π a✝ ≫ m₂ = π a✝ ≫ m₂

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h✝ : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ (fun a => π a ≫ m₂) a₁ = g₂ ≫ (fun a => π a ≫ m₂) a₂

Tactic:
simp only [← Category.assoc, h]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
this : m₂ = desc X π (fun a => π a ≫ m₂) ⋯
⊢ m₁ = desc X π (fun a => π a ≫ m₂) ⋯

Tactic:
exact EffectiveEpiFamily.uniq _ _ _ _ _ h

Result:
no goals