-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparator_pi {β : Type w} (f : β → C) [HasProduct f] :
    IsCoseparator (∏ᶜ f) ↔ IsCoseparating (Set.range f)

Proof state:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ᶜ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v

Tactic:
refine h.def _ _ fun g => limit.hom_ext fun b => ?_

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ᶜ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ ∏ᶜ f
b : Discrete β
⊢ (u ≫ g) ≫ limit.π (Discrete.functor f) b = (v ≫ g) ≫ limit.π (Discrete.functor f) b

Proof state:
case refine_2.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ ∏ᶜ f), u ≫ h = v ≫ h
b : β
hZ : f b ∈ Set.range f
g : Y ⟶ f b
⊢ u ≫ g = v ≫ g

Tactic:
classical simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b

Result:
no goals

Proof state:
case refine_2.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ ∏ᶜ f), u ≫ h = v ≫ h
b : β
hZ : f b ∈ Set.range f
g : Y ⟶ f b
⊢ u ≫ g = v ≫ g

Tactic:
simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ᶜ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ ∏ᶜ f
b : Discrete β
⊢ (u ≫ g) ≫ limit.π (Discrete.functor f) b = (v ≫ g) ≫ limit.π (Discrete.functor f) b

Tactic:
simpa using huv (f b.as) (by simp) (g ≫ limit.π (Discrete.functor f) _)

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ᶜ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ ∏ᶜ f
b : Discrete β
⊢ f b.as ∈ Set.range f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
⊢ IsCoseparator (∏ᶜ f) ↔ IsCoseparating (Set.range f)

Tactic:
refine
  ⟨fun h X Y u v huv => ?_, fun h =>
    (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => ?_⟩

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ᶜ f)
X Y : C
u v : X ⟶ Y
huv : ∀ G ∈ Set.range f, ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ ∏ᶜ f), u ≫ h = v ≫ h
Z : C
hZ : Z ∈ Set.range f
g : Y ⟶ Z
⊢ u ≫ g = v ≫ g

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ ∏ᶜ f), u ≫ h = v ≫ h
Z : C
hZ : Z ∈ Set.range f
g : Y ⟶ Z
⊢ u ≫ g = v ≫ g

Tactic:
obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ

Result:
case refine_2.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ ∏ᶜ f), u ≫ h = v ≫ h
b : β
hZ : f b ∈ Set.range f
g : Y ⟶ f b
⊢ u ≫ g = v ≫ g