-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
@[reassoc (attr := simp)]
lemma comm (hφ : e.HasLift φ) (i' j' : ι') :
    f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

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.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).inv ≫ φ.f j ≫ (L.extendXIso e ⋯).inv

Tactic:
dsimp [restrictionXIso]

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.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ 𝟙 (K.X (e.f j)) ≫ φ.f j ≫ (L.extendXIso e ⋯).inv

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.restriction e ⟶ L
hφ : e.HasLift φ
i j : ι
hij' : c'.Rel (e.f i) (e.f j)
⊢ ((K.restrictionXIso e ⋯).inv ≫ φ.f i ≫ (L.extendXIso e ⋯).inv) ≫
      (L.extendXIso e ⋯).hom ≫ L.d i j ≫ (L.extendXIso e ⋯).inv =
    K.d (e.f i) (e.f j) ≫ (K.restrictionXIso e ⋯).inv ≫ φ.f j ≫ (L.extendXIso e ⋯).inv

Tactic:
simp [HomologicalComplex.restrictionXIso]

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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj' : ∃ j, e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
obtain ⟨j, hj⟩ := hj'

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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this : (L.extend e).d i' j' = 0
hj' : ¬∃ j, e.f j = j'
⊢ 0 = K.d i' j' ≫ f φ j'

Tactic:
have : f φ j' = 0 := by
  apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt

Result:
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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this✝ : (L.extend e).d i' j' = 0
hj' : ¬∃ j, e.f j = j'
this : f φ j' = 0
⊢ 0 = K.d i' j' ≫ f φ j'

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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ∃ i, e.f i = i'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
obtain ⟨i, hi⟩ := 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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this : (L.extend e).d i' j' = 0
hj' : ¬∃ j, e.f j = j'
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
simpa using hj'

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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this✝ : (L.extend e).d i' j' = 0
hj' : ¬∃ j, e.f j = j'
this : f φ j' = 0
⊢ 0 = K.d i' j' ≫ f φ j'

Tactic:
rw [this, comp_zero]

Result:
no goals

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.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ 𝟙 (K.X (e.f j)) ≫ φ.f j ≫ (L.extendXIso e ⋯).inv

Tactic:
rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij'
  (by simpa using hi')) i' hij'), zero_comp]

Result:
no goals

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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
rw [f_eq φ hj, L.extend_d_eq e hi hj]

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.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫
      (L.extendXIso e hi).hom ≫ L.d i j ≫ (L.extendXIso e hj).inv =
    K.d i' j' ≫ (K.restrictionXIso e hj).inv ≫ φ.f j ≫ (L.extendXIso e hj).inv