C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
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)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
⊢ IsSeparator G ↔ ∀ (A : C), Epi (Sigma.desc fun f => f)
rw [isSeparator_def]
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
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 C
D : Type u₂
inst✝¹ : Category D
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
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
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)
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), 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
simpa using Sigma.ι _ i ≫= huv
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
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
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
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
haveI := h X
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
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
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
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
refine' (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.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), 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
simpa using hh j.as