-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
lemma homRestrict_hasLift (ψ : K ⟶ L.extend e) :
    e.HasLift (e.homRestrict ψ)

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

Tactic:
apply (L.isZero_extend_X e i' (hj.not_mem hij')).eq_of_src

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (e.homRestrict ψ).f j = 0

Tactic:
have : (L.extend e).d i' (e.f j) = 0 := by
  apply (L.isZero_extend_X e i' (hj.not_mem hij')).eq_of_src

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ (e.homRestrict ψ).f j = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ (e.homRestrict ψ).f j = 0

Tactic:
dsimp [homRestrict]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
⊢ e.HasLift (e.homRestrict ψ)

Tactic:
intro j hj i' hij'

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (e.homRestrict ψ).f j = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0

Tactic:
rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
  ← ψ.comm_assoc, this, zero_comp, comp_zero]

Result:
no goals