case right_cancellation
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ∀ {Z : W} (g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0),
    g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0 → g = h
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ Mono (HomologicalComplex.Hom.f f 0)
constructor
case right_cancellation
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ g = h
case right_cancellation
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ∀ {Z : W} (g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0),
    g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0 → g = h
intro Z g h Hgh
case right_cancellation
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh✝ : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
Hgh :
  g ≫ (fromSingle₀KernelAtZeroIso f).inv ≫ kernel.ι (d X 0 1) =
    h ≫ (fromSingle₀KernelAtZeroIso f).inv ≫ kernel.ι (d X 0 1)
⊢ g = h
case right_cancellation
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ g = h
rw [← kernel.lift_ι (X.d 0 1) (f.f 0) (by rw [f.2 0 1 rfl]; exact zero_comp),
  ← fromSingle₀KernelAtZeroIso_inv_eq] at Hgh
no goals
case right_cancellation
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh✝ : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
Hgh :
  g ≫ (fromSingle₀KernelAtZeroIso f).inv ≫ kernel.ι (d X 0 1) =
    h ≫ (fromSingle₀KernelAtZeroIso f).inv ≫ kernel.ι (d X 0 1)
⊢ g = h
rw [(@cancel_mono _ _ _ _ _ _ (mono_comp _ _) _ _).1 Hgh]
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ d ((CochainComplex.single₀ W).obj Y) 0 1 ≫ HomologicalComplex.Hom.f f 1 = 0
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
rw [f.2 0 1 rfl]
no goals
ι : Type ?u.86854
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ d ((CochainComplex.single₀ W).obj Y) 0 1 ≫ HomologicalComplex.Hom.f f 1 = 0
exact zero_comp