case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v

case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
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
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
⊢ IsCoseparator (∏ f) ↔ IsCoseparating (Set.range f)
refine'
  ⟨fun h X Y u v huv => _, fun h =>
    (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), 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
case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v
refine' h.def _ _ fun g => limit.hom_ext fun b => _
no goals
case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), 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
simpa using huv (f b.as) (by simp) (g ≫ limit.π (Discrete.functor f) _)
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ ∏ f
b : Discrete β
⊢ f b.as ∈ Set.range f
simp
case refine'_2.intro
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
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
case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
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
obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ
no goals
case refine'_2.intro
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
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
classical simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b
no goals
case refine'_2.intro
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
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
simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b