-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc]
lemma homologyι_descOpcycles_eq_zero_of_boundary {A : C} (k : K.X i ⟶ A) (j : ι)
    (hj : c.prev i = j) {i' : ι} (x : K.X i' ⟶ A) (hx : k = K.d i i' ≫ x) :
    K.homologyι i ≫ K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.d j i ≫ k = 0

Tactic:
rw [hx, K.d_comp_d_assoc, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{?u.64639, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
⊢ K.d j i ≫ k = 0

Tactic:
rw [hx, K.d_comp_d_assoc, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx✝ : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
⊢ K.descOpcycles k j hj ⋯ = 0

Tactic:
rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]

Result:
no goals

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
obtain rfl := c.next_eq' h

Result:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
x : K.X (c.next i) ⟶ A
hx : k = K.d i (c.next i) ≫ x
h : c.Rel i (c.next i)
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
by_cases h : c.Rel i i'

Result:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

case neg
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.descOpcycles k j hj ⋯ = 0

Tactic:
rw [K.shape _ _ h, zero_comp] at hx

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx✝ : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
⊢ K.descOpcycles k j hj ⋯ = 0

Proof state:
case neg
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
have : K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 := by
  rw [K.shape _ _ h, zero_comp] at hx
  rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]

Result:
case neg
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
this : K.descOpcycles k j hj ⋯ = 0
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Proof state:
case neg
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
this : K.descOpcycles k j hj ⋯ = 0
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
rw [this, comp_zero]

Result:
no goals

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
x : K.X (c.next i) ⟶ A
hx : k = K.d i (c.next i) ≫ x
h : c.Rel i (c.next i)
⊢ K.homologyι i ≫ K.descOpcycles k j hj ⋯ = 0

Tactic:
exact (K.sc i).homologyι_descOpcycles_eq_zero_of_boundary _ x hx

Result:
no goals