case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
⊢ u = v

case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ G ⨯ H), u ≫ h = v ≫ h
Z : C
hZ : Z ∈ {G, H}
g : Y ⟶ Z
⊢ u ≫ g = v ≫ g
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ IsCoseparator (G ⨯ H) ↔ IsCoseparating {G, H}
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.refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ (u ≫ g) ≫ prod.fst = (v ≫ g) ≫ prod.fst

case refine'_1.refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ (u ≫ g) ≫ prod.snd = (v ≫ g) ≫ prod.snd
case refine'_1
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
⊢ u = v
refine' h.def _ _ fun g => prod.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✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ (u ≫ g) ≫ prod.fst = (v ≫ g) ≫ prod.fst
simpa using huv G (by simp) (g ≫ Limits.prod.fst)
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ 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✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ (u ≫ g) ≫ prod.snd = (v ≫ g) ≫ prod.snd
simpa using huv H (by simp) (g ≫ Limits.prod.snd)
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ 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✝ : HasBinaryProduct G H
h : IsCoseparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ G ⨯ H), u ≫ h = v ≫ h
Z : C
g : Y ⟶ Z
hZ : Z = G ∨ Z = H
⊢ u ≫ g = v ≫ g
case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ G ⨯ H), u ≫ h = v ≫ h
Z : C
hZ : Z ∈ {G, H}
g : Y ⟶ Z
⊢ u ≫ g = v ≫ g
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 : Y ⟶ Z
inst✝ : HasBinaryProduct Z H
h : IsCoseparating {Z, H}
huv : ∀ (h : Y ⟶ Z ⨯ H), u ≫ h = v ≫ h
⊢ u ≫ g = v ≫ g

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 : Y ⟶ Z
inst✝ : HasBinaryProduct G Z
h : IsCoseparating {G, Z}
huv : ∀ (h : Y ⟶ G ⨯ Z), u ≫ h = v ≫ h
⊢ u ≫ g = v ≫ g
case refine'_2
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ G ⨯ H), u ≫ h = v ≫ h
Z : C
g : Y ⟶ Z
hZ : Z = G ∨ Z = H
⊢ u ≫ g = v ≫ g
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 : Y ⟶ Z
inst✝ : HasBinaryProduct Z H
h : IsCoseparating {Z, H}
huv : ∀ (h : Y ⟶ Z ⨯ H), u ≫ h = v ≫ h
⊢ u ≫ g = v ≫ g
simpa using huv (prod.lift g 0) =≫ Limits.prod.fst
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 : Y ⟶ Z
inst✝ : HasBinaryProduct G Z
h : IsCoseparating {G, Z}
huv : ∀ (h : Y ⟶ G ⨯ Z), u ≫ h = v ≫ h
⊢ u ≫ g = v ≫ g
simpa using huv (prod.lift 0 g) =≫ Limits.prod.snd