case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
⊢ IsSeparating 𝒢 ↔ ∀ (A : C), Epi (Sigma.desc Sigma.snd)
refine' ⟨fun h A => ⟨fun u v huv => h _ _ fun G hG f => _⟩, fun h X Y f g hh => _⟩
no goals
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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
simpa using Sigma.ι (fun f : ΣG : 𝒢, (G : C) ⟶ A => (f.1 : C)) ⟨⟨G, hG⟩, f⟩ ≫= huv
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc Sigma.snd)
⊢ f = g
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), G ∈ 𝒢 → ∀ (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
𝒢 : 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 : C), 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
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc Sigma.snd)
⊢ f = g
refine'
  (cancel_epi (Sigma.desc (@Sigma.snd 𝒢 fun G => (G : C) ⟶ X))).1 (colimit.hom_ext fun j => _)
no goals
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), 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
simpa using hh j.as.1.1 j.as.1.2 j.as.2