-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
@[simp]
lemma liftExtend_homRestrict (ψ : K ⟶ L.extend e) :
    e.liftExtend (e.homRestrict ψ) (e.homRestrict_hasLift ψ) = ψ

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.liftExtend (e.homRestrict ψ) ⋯ = ψ

Tactic:
ext i'

Result:
case h
ι : 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
i' : ι'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

Proof state:
case h
ι : 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
i' : ι'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

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

Result:
case pos
ι : 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
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

case neg
ι : 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
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

Proof state:
case pos.intro
ι : 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
i : ι
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f (e.f i) = ψ.f (e.f i)

Tactic:
simp [e.homRestrict_f _ rfl, e.liftExtend_f _ _ rfl]

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
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi'

Result:
no goals

Proof state:
case neg
ι : 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
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

Tactic:
apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_tgt

Result:
no goals

Proof state:
case pos
ι : 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
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

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

Result:
case pos.intro
ι : 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
i : ι
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f (e.f i) = ψ.f (e.f i)