-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparating_iff_epi (𝒢 : Set C)
    [∀ A : C, HasCoproduct fun f : ΣG : 𝒢, (G : C) ⟶ A => (f.1 : C)] :
    IsSeparating 𝒢 ↔ ∀ A : C, Epi (Sigma.desc (@Sigma.snd 𝒢 fun G => (G : C) ⟶ A))

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
h : ∀ (A : C), Epi (Sigma.desc Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ G ∈ 𝒢, ∀ (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
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
h : ∀ (A : C), Epi (Sigma.desc Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc Sigma.snd)
⊢ f = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
⊢ IsSeparating 𝒢 ↔ ∀ (A : C), Epi (Sigma.desc Sigma.snd)

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

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
h : IsSeparating 𝒢
A Z✝ : C
u v : A ⟶ Z✝
huv : Sigma.desc Sigma.snd ≫ u = Sigma.desc Sigma.snd ≫ v
G : C
hG : G ∈ 𝒢
f : G ⟶ A
⊢ f ≫ u = f ≫ v

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

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

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

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

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
h : IsSeparating 𝒢
A Z✝ : C
u v : A ⟶ Z✝
huv : Sigma.desc Sigma.snd ≫ u = Sigma.desc Sigma.snd ≫ v
G : C
hG : G ∈ 𝒢
f : G ⟶ A
⊢ f ≫ u = f ≫ v

Tactic:
simpa using Sigma.ι (fun f : ΣG : 𝒢, (G : C) ⟶ A => (f.1 : C)) ⟨⟨G, hG⟩, f⟩ ≫= huv

Result:
no goals

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

Tactic:
simpa using hh j.as.1.1 j.as.1.2 j.as.2

Result:
no goals