-- Mathlib/Algebra/Homology/Embedding/Extend.lean
@[simp]
lemma extendMap_add [Preadditive C] {K L : HomologicalComplex C c} (φ φ' : K ⟶ L)
    (e : c.Embedding c') : extendMap (φ + φ' : K ⟶ L) e = extendMap φ e + extendMap φ' e

Proof state:
case h
ι : 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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'

Result:
case pos
ι : 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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

case neg
ι : 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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
⊢ extendMap (φ + φ') e = extendMap φ e + extendMap φ' e

Tactic:
ext i'

Result:
case h
ι : 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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

Proof state:
case pos
ι : 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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

Tactic:
obtain ⟨i, hi⟩ := hi'

Result:
case pos.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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

Proof state:
case pos.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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

Tactic:
simp [extendMap_f _ e hi]

Result:
no goals

Proof state:
case neg
ι : 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✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

Result:
no goals