-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparator_iff_epi (G : C) [∀ A : C, HasCoproduct fun _ : G ⟶ A => G] :
    IsSeparator G ↔ ∀ A : C, Epi (Sigma.desc fun f : G ⟶ A => f)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
⊢ IsSeparator G ↔ ∀ (A : C), Epi (Sigma.desc fun f => f)

Tactic:
rw [isSeparator_def]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔ ∀ (A : C), Epi (Sigma.desc fun f => f)

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
A Z✝ : C
u v : A ⟶ Z✝
huv : (Sigma.desc fun f => f) ≫ u = (Sigma.desc fun f => f) ≫ v
i : G ⟶ A
⊢ i ≫ u = i ≫ v

Tactic:
simpa using Sigma.ι _ i ≫= huv

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
haveI := h X

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f => f)
⊢ f = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔ ∀ (A : C), Epi (Sigma.desc fun f => f)

Tactic:
refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
A Z✝ : C
u v : A ⟶ Z✝
huv : (Sigma.desc fun f => f) ≫ u = (Sigma.desc fun f => f) ≫ v
i : G ⟶ A
⊢ i ≫ u = i ≫ v

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f => f)
j : Discrete (G ⟶ X)
⊢ colimit.ι (Discrete.functor fun f => G) j ≫ (Sigma.desc fun f => f) ≫ f =
    colimit.ι (Discrete.functor fun f => G) j ≫ (Sigma.desc fun f => f) ≫ g

Tactic:
simpa using hh j.as

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f => f)
⊢ f = g

Tactic:
refine (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f => f)
j : Discrete (G ⟶ X)
⊢ colimit.ι (Discrete.functor fun f => G) j ≫ (Sigma.desc fun f => f) ≫ f =
    colimit.ι (Discrete.functor fun f => G) j ≫ (Sigma.desc fun f => f) ≫ g