case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
⊢ 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✝ : HasCoproduct f
h : IsSeparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v
Z : C
hZ : Z ∈ Set.range f
g : Z ⟶ X
⊢ g ≫ u = g ≫ v
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
⊢ IsSeparator (∐ f) ↔ IsSeparating (Set.range f)
refine'
  ⟨fun h X Y u v huv => _, fun h =>
    (isSeparator_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✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : ∐ f ⟶ X
b : Discrete β
⊢ colimit.ι (Discrete.functor f) b ≫ g ≫ u = colimit.ι (Discrete.functor f) b ≫ g ≫ v
case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
⊢ u = v
refine' h.def _ _ fun g => colimit.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✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : ∐ f ⟶ X
b : Discrete β
⊢ colimit.ι (Discrete.functor f) b ≫ g ≫ u = colimit.ι (Discrete.functor f) b ≫ g ≫ v
simpa using huv (f b.as) (by simp) (colimit.ι (Discrete.functor f) _ ≫ g)
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : ∐ f ⟶ X
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✝ : HasCoproduct f
h : IsSeparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v
b : β
hZ : f b ∈ Set.range f
g : f b ⟶ X
⊢ g ≫ u = g ≫ v
case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v
Z : C
hZ : Z ∈ Set.range f
g : Z ⟶ X
⊢ g ≫ u = g ≫ v
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✝ : HasCoproduct f
h : IsSeparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v
b : β
hZ : f b ∈ Set.range f
g : f b ⟶ X
⊢ g ≫ u = g ≫ v
classical simpa using Sigma.ι f b ≫= huv (Sigma.desc (Pi.single b g))
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✝ : HasCoproduct f
h : IsSeparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v
b : β
hZ : f b ∈ Set.range f
g : f b ⟶ X
⊢ g ≫ u = g ≫ v
simpa using Sigma.ι f b ≫= huv (Sigma.desc (Pi.single b g))