case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ 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
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : G ⨿ H ⟶ X), h ≫ u = h ≫ v
Z : C
hZ : Z ∈ {G, H}
g : Z ⟶ X
⊢ g ≫ u = g ≫ v
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ IsSeparator (G ⨿ H) ↔ IsSeparating {G, H}
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.refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ coprod.inl ≫ g ≫ u = coprod.inl ≫ g ≫ v

case refine'_1.refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ coprod.inr ≫ g ≫ u = coprod.inr ≫ g ≫ v
case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
⊢ u = v
refine' h.def _ _ fun g => coprod.hom_ext _ _
no goals
case refine'_1.refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ coprod.inl ≫ g ≫ u = coprod.inl ≫ g ≫ v
simpa using huv G (by simp) (coprod.inl ≫ g)
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ G ∈ {G, H}
simp
no goals
case refine'_1.refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ coprod.inr ≫ g ≫ u = coprod.inr ≫ g ≫ v
simpa using huv H (by simp) (coprod.inr ≫ g)
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ H ∈ {G, H}
simp
case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : G ⨿ H ⟶ X), h ≫ u = h ≫ v
Z : C
g : Z ⟶ X
hZ : Z = G ∨ Z = H
⊢ g ≫ u = g ≫ v
case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : G ⨿ H ⟶ X), h ≫ u = h ≫ v
Z : C
hZ : Z ∈ {G, H}
g : Z ⟶ X
⊢ g ≫ u = g ≫ v
simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ
case refine'_2.inl
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
H X Y : C
u v : X ⟶ Y
Z : C
g : Z ⟶ X
inst✝ : HasBinaryCoproduct Z H
h : IsSeparating {Z, H}
huv : ∀ (h : Z ⨿ H ⟶ X), h ≫ u = h ≫ v
⊢ g ≫ u = g ≫ v

case refine'_2.inr
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G X Y : C
u v : X ⟶ Y
Z : C
g : Z ⟶ X
inst✝ : HasBinaryCoproduct G Z
h : IsSeparating {G, Z}
huv : ∀ (h : G ⨿ Z ⟶ X), h ≫ u = h ≫ v
⊢ g ≫ u = g ≫ v
case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : G ⨿ H ⟶ X), h ≫ u = h ≫ v
Z : C
g : Z ⟶ X
hZ : Z = G ∨ Z = H
⊢ g ≫ u = g ≫ v
rcases hZ with (rfl | rfl)
no goals
case refine'_2.inl
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
H X Y : C
u v : X ⟶ Y
Z : C
g : Z ⟶ X
inst✝ : HasBinaryCoproduct Z H
h : IsSeparating {Z, H}
huv : ∀ (h : Z ⨿ H ⟶ X), h ≫ u = h ≫ v
⊢ g ≫ u = g ≫ v
simpa using coprod.inl ≫= huv (coprod.desc g 0)
no goals
case refine'_2.inr
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G X Y : C
u v : X ⟶ Y
Z : C
g : Z ⟶ X
inst✝ : HasBinaryCoproduct G Z
h : IsSeparating {G, Z}
huv : ∀ (h : G ⨿ Z ⟶ X), h ≫ u = h ≫ v
⊢ g ≫ u = g ≫ v
simpa using coprod.inr ≫= huv (coprod.desc 0 g)