-- Mathlib/Algebra/Homology/Embedding/TruncLE.lean
lemma truncLE'Map_f_eq_cyclesMap {i : ι} (hi : e.BoundaryLE i) {i' : ι'} (h : e.f i = i') :
    (truncLE'Map φ e).f i =
      (K.truncLE'XIsoCycles e h hi).hom ≫ cyclesMap φ i' ≫
        (L.truncLE'XIsoCycles e h hi).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ e.op.BoundaryGE i

Tactic:
simpa

Result:
no goals

Proof state:
case a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ ((truncLE'Map φ e).f i).op =
    ((K.truncLE'XIsoCycles e h hi).hom ≫ cyclesMap φ i' ≫ (L.truncLE'XIsoCycles e h hi).inv).op

Tactic:
dsimp [truncLE'Map, truncLE'XIsoCycles]

Result:
case a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (truncGE'Map ((opFunctor C c').map φ.op) e.op).f i =
    (((L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫ (L.opcyclesOpIso i').hom) ≫ (cyclesMap φ i').op) ≫
      (K.opcyclesOpIso i').inv ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (truncLE'Map φ e).f i = (K.truncLE'XIsoCycles e h hi).hom ≫ cyclesMap φ i' ≫ (L.truncLE'XIsoCycles e h hi).inv

Tactic:
apply Quiver.Hom.op_inj

Result:
case a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ ((truncLE'Map φ e).f i).op =
    ((K.truncLE'XIsoCycles e h hi).hom ≫ cyclesMap φ i' ≫ (L.truncLE'XIsoCycles e h hi).inv).op

Proof state:
case a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (truncGE'Map ((opFunctor C c').map φ.op) e.op).f i =
    (((L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫ (L.opcyclesOpIso i').hom) ≫ (cyclesMap φ i').op) ≫
      (K.opcyclesOpIso i').inv ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv

Tactic:
rw [assoc, assoc, truncGE'Map_f_eq_opcyclesMap _ e.op (by simpa) h,
  opcyclesOpIso_inv_naturality_assoc, Iso.hom_inv_id_assoc]

Result:
no goals