-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma extend_d_to_eq_zero (i' j' : ι') (j : ι) (hj : e.f j = j') (hj' : ¬ c.Rel (c.prev j) j) :
    (K.extend e).d i' j' = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
⊢ (K.extend e).d i' j' = 0

Tactic:
obtain hi'|⟨i, hi⟩ := (e.r i').eq_none_or_eq_some

Result:
case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi' : e.r i' = none
⊢ (K.extend e).d i' j' = 0

case inr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
⊢ (K.extend e).d i' j' = 0

Proof state:
case inr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
⊢ (K.extend e).d i' j' = 0

Tactic:
rw [extend_d_eq K e (e.f_eq_of_r_eq_some hi) hj, K.shape, zero_comp, comp_zero]

Result:
case inr.intro.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
⊢ ¬c.Rel i j

Proof state:
case inr.intro.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi : e.r i' = some (c.prev j)
hij : c.Rel (c.prev j) j
⊢ False

Tactic:
exact hj' hij

Result:
no goals

Proof state:
case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi' : e.r i' = none
⊢ (K.extend e).d i' j' = 0

Tactic:
exact extend.d_none_eq_zero _ _ _ hi'

Result:
no goals

Proof state:
case inr.intro.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
⊢ ¬c.Rel i j

Tactic:
intro hij

Result:
case inr.intro.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
hij : c.Rel i j
⊢ False

Proof state:
case inr.intro.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
hij : c.Rel i j
⊢ False

Tactic:
obtain rfl := c.prev_eq' hij

Result:
case inr.intro.a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi : e.r i' = some (c.prev j)
hij : c.Rel (c.prev j) j
⊢ False