case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : Set C
inst✝ : ∀ (A : C), HasProduct fun f => ↑f.fst
⊢ IsCoseparating 𝒢 ↔ ∀ (A : C), Mono (Pi.lift 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), 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
simpa using huv =≫ Pi.π (fun f : ΣG : 𝒢, A ⟶ (G : C) => (f.1 : C)) ⟨⟨G, hG⟩, f⟩
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift Sigma.snd)
⊢ f = g
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), G ∈ 𝒢 → ∀ (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
𝒢 : 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 : C), 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
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
𝒢 : 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 : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift Sigma.snd)
⊢ f = g
refine' (cancel_mono (Pi.lift (@Sigma.snd 𝒢 fun G => Y ⟶ (G : C)))).1 (limit.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), HasProduct fun f => ↑f.fst
h : ∀ (A : C), Mono (Pi.lift Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ (G : C), 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
simpa using hh j.as.1.1 j.as.1.2 j.as.2