A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ a = b
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h : a ≫ ι f g w = b ≫ ι f g w
⊢ a = b
dsimp [ι] at h
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) a = (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) b

case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ Function.Injective fun e => e ≫ (homologyIsoKernelDesc f g w).hom
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ a = b
apply_fun fun e => e ≫ (homologyIsoKernelDesc f g w).hom
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ Function.Injective fun e => e ≫ (homologyIsoKernelDesc f g w).hom

A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) a = (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) b
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) a = (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) b

case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ Function.Injective fun e => e ≫ (homologyIsoKernelDesc f g w).hom
swap
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  (a ≫ (homologyIsoKernelDesc f g w).hom) ≫ kernel.ι (cokernel.desc f g w) =
    (b ≫ (homologyIsoKernelDesc f g w).hom) ≫ kernel.ι (cokernel.desc f g w)
⊢ (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) a = (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) b
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) a = (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) b
simp only [← Category.assoc] at h
no goals
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  (a ≫ (homologyIsoKernelDesc f g w).hom) ≫ kernel.ι (cokernel.desc f g w) =
    (b ≫ (homologyIsoKernelDesc f g w).hom) ≫ kernel.ι (cokernel.desc f g w)
⊢ (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) a = (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) b
exact equalizer.hom_ext h
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
i j : W ⟶ homology f g w
hh : (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) i = (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) j
⊢ i = j
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
⊢ Function.Injective fun e => e ≫ (homologyIsoKernelDesc f g w).hom
intro i j hh
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
i j : W ⟶ homology f g w
hh :
  (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) i ≫ (homologyIsoKernelDesc f g w).inv =
    (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) j ≫ (homologyIsoKernelDesc f g w).inv
⊢ i = j
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
i j : W ⟶ homology f g w
hh : (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) i = (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) j
⊢ i = j
apply_fun fun e => e ≫ (homologyIsoKernelDesc f g w).inv  at hh
no goals
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
a b : W ⟶ homology f g w
h :
  a ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    b ≫ (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)
i j : W ⟶ homology f g w
hh :
  (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) i ≫ (homologyIsoKernelDesc f g w).inv =
    (fun e => e ≫ (homologyIsoKernelDesc f g w).hom) j ≫ (homologyIsoKernelDesc f g w).inv
⊢ i = j
simpa using hh