-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparating_iff_mono (𝒢 : Set C)
    [∀ A : C, HasProduct fun f : ΣG : 𝒢, A ⟶ (G : C) => (f.1 : C)] :
    IsCoseparating 𝒢 ↔ ∀ A : C, Mono (Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C)))

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

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

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
inst✝ : ∀ (A : C), HasProduct fun f => ↑f.fst
⊢ IsCoseparating 𝒢 ↔ ∀ (A : C), Mono (Pi.lift 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), HasProduct fun f => ↑f.fst
h : IsCoseparating 𝒢
A Z✝ : C
u v : Z✝ ⟶ A
huv : u ≫ Pi.lift Sigma.snd = v ≫ Pi.lift Sigma.snd
G : C
hG : G ∈ 𝒢
f : A ⟶ G
⊢ u ≫ f = v ≫ f

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

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

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

Result:
no goals

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

Tactic:
refine (cancel_mono (Pi.lift (@Sigma.snd 𝒢 fun G => Y ⟶ (G : C)))).1 (limit.hom_ext fun j => ?_)

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

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

Tactic:
haveI := h Y

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