C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔ ∀ (A : C), Mono (Pi.lift fun f => f)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
⊢ IsCoseparator G ↔ ∀ (A : C), Mono (Pi.lift fun f => f)
rw [isCoseparator_def]
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
A Z✝ : C
u v : Z✝ ⟶ A
huv : (u ≫ Pi.lift fun f => f) = v ≫ Pi.lift fun f => f
i : A ⟶ G
⊢ u ≫ i = v ≫ i

case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔ ∀ (A : C), Mono (Pi.lift fun f => f)
refine' ⟨fun h A => ⟨fun u v huv => h _ _ fun i => _⟩, fun h X Y f g hh => _⟩
no goals
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
A Z✝ : C
u v : Z✝ ⟶ A
huv : (u ≫ Pi.lift fun f => f) = v ≫ Pi.lift fun f => f
i : A ⟶ G
⊢ u ≫ i = v ≫ i
simpa using huv =≫ Pi.π _ i
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f => f)
⊢ f = g
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
haveI := h Y
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f => f)
j : Discrete (Y ⟶ G)
⊢ (f ≫ Pi.lift fun f => f) ≫ limit.π (Discrete.functor fun f => G) j =
    (g ≫ Pi.lift fun f => f) ≫ limit.π (Discrete.functor fun f => G) j
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f => f)
⊢ f = g
refine' (cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => _)
no goals
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f => f)
j : Discrete (Y ⟶ G)
⊢ (f ≫ Pi.lift fun f => f) ≫ limit.π (Discrete.functor fun f => G) j =
    (g ≫ Pi.lift fun f => f) ≫ limit.π (Discrete.functor fun f => G) j
simpa using hh j.as