mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).iCycles =
    (K.sc j).homologyData.left.cyclesIso.hom ≫
      ((K.sc j).homologyData.left.i ≫ (K.extendXIso e hj').inv) ≫ (K.extendXIso e hj').hom

Tactic:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).iCycles =
    (K.sc j).homologyData.left.cyclesIso.hom ≫
      (K.sc j).homologyData.left.i ≫ (K.extendXIso e hj').inv ≫ (K.extendXIso e hj').hom
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ 0 =
    K.d j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ (K.truncGE'XIsoOpcycles e hk' hj).inv ≫ ((K.truncGE' e).extendXIso e hk').inv

Tactic:
d_pOpcycles_assoc,

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ 0 = 0 ≫ (K.truncGE'XIsoOpcycles e hk' hj).inv ≫ ((K.truncGE' e).extendXIso e hk').inv
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ ((extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
        (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫ (K.sc j).homologyData.left.homologyIso.inv) ≫
      (K.sc j).homologyData.left.homologyIso.hom =
    ((K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ) ≫ (K.sc j).homologyData.left.homologyIso.hom

Tactic:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      ((extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫ (K.sc j).homologyData.left.homologyIso.inv) ≫
        (K.sc j).homologyData.left.homologyIso.hom =
    ((K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ) ≫ (K.sc j).homologyData.left.homologyIso.hom
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      ((extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫ (K.sc j).homologyData.left.homologyIso.inv) ≫
        (K.sc j).homologyData.left.homologyIso.hom =
    ((K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ) ≫ (K.sc j).homologyData.left.homologyIso.hom

Tactic:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫
        (K.sc j).homologyData.left.homologyIso.inv ≫ (K.sc j).homologyData.left.homologyIso.hom =
    ((K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ) ≫ (K.sc j).homologyData.left.homologyIso.hom
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫
        (K.sc j).homologyData.left.homologyIso.inv ≫ (K.sc j).homologyData.left.homologyIso.hom =
    ((K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ) ≫ (K.sc j).homologyData.left.homologyIso.hom

Tactic:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫
        (K.sc j).homologyData.left.homologyIso.inv ≫ (K.sc j).homologyData.left.homologyIso.hom =
    (K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ ≫ (K.sc j).homologyData.left.homologyIso.hom
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extend e).homologyπ j' ≫ (K.extendHomologyIso e hj').hom = (K.extendCyclesIso e hj').hom ≫ K.homologyπ j

Tactic:
dsimp [extendHomologyIso, homologyπ]
  rw [ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc,
    ← cancel_mono (K.sc j).homologyData.left.homologyIso.hom,
    assoc, assoc, assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom]
  dsimp [extendCyclesIso]
  simp only [assoc, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv) ≫ (K.extendOpcyclesIso e hj').hom =
    ((K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j') ≫ (K.extendOpcyclesIso e hj').hom

Tactic:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv ≫ (K.extendOpcyclesIso e hj').hom =
    ((K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j') ≫ (K.extendOpcyclesIso e hj').hom
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv ≫ (K.extendOpcyclesIso e hj').hom =
    ((K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j') ≫ (K.extendOpcyclesIso e hj').hom

Tactic:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv ≫ (K.extendOpcyclesIso e hj').hom =
    (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j' ≫ (K.extendOpcyclesIso e hj').hom
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
⊢ K.restrictionToTruncGE' e ≫ truncGE'Map φ e = restrictionMap φ e ≫ L.restrictionToTruncGE' e

Tactic:
by
  ext i
  by_cases hi : e.BoundaryGE i
  · simp [restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv _ e rfl hi,
      truncGE'Map_f_eq_opcyclesMap φ e hi rfl, restrictionXIso]
  · simp [restrictionToTruncGE'_f_eq_iso_hom_iso_inv _ e rfl hi,
      truncGE'Map_f_eq φ e hi rfl, restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).pOpcycles =
    (K.extendXIso e hj').inv ≫
      ((K.extendXIso e hj').hom ≫ (K.sc j).homologyData.right.p) ≫ (K.sc j).homologyData.right.opcyclesIso.inv

Tactic:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).pOpcycles =
    (K.extendXIso e hj').inv ≫
      (K.extendXIso e hj').hom ≫ (K.sc j).homologyData.right.p ≫ (K.sc j).homologyData.right.opcyclesIso.inv
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{v_1, u_3} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ QuasiIsoAt (extendMap φ e) j' ↔ QuasiIsoAt φ j

Tactic:
simp only [quasiIsoAt_iff_isIso_homologyMap]
  exact (MorphismProperty.isomorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (K.extendHomologyIso e hj') (L.extendHomologyIso e hj'))

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{v_1, u_3} C
inst✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
⊢ IsIso ((K.restrictionToTruncGE' e).f i)

Tactic:
by_cases hi : e.BoundaryGE i
  · rw [K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e rfl hi]
    have : IsIso (K.pOpcycles (e.f i)) := K.isIso_pOpcycles _ _ rfl (by
      obtain ⟨hi₁, hi₂⟩ := hi
      apply IsZero.eq_of_src (K.isZero_X_of_isStrictlySupported e _
        (fun j hj ↦ hi₂ j (by simpa only [hj] using hi₁))))
    infer_instance
  · rw [K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi]
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, 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:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, 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
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, 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:
assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, 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
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ ac.desc x₁ x₂ (e₁.f i₁) = x₁ i₁

Tactic:
dsimp [desc]

Goal state after:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ (desc.aux X (ac.equiv (ac.equiv.symm (e₁.f i₁))) (e₁.f i₁) ⋯) (ac.desc' x₁ x₂ (ac.equiv.symm (e₁.f i₁))) = x₁ i₁
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ ac.desc x₁ x₂ (e₂.f i₂) = x₂ i₂

Tactic:
dsimp [desc]

Goal state after:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ (desc.aux X (ac.equiv (ac.equiv.symm (e₂.f i₂))) (e₂.f i₂) ⋯) (ac.desc' x₁ x₂ (ac.equiv.symm (e₂.f i₂))) = x₂ i₂
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
hi : ¬∃ j', c'.Rel (e.f i) j'
this : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i))
⊢ homologyMap ((K.shortComplexTruncLE e).f ≫ (K.shortComplexTruncLE e).g) (e.f i) = 0

Tactic:
ShortComplex.zero,

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
hi : ¬∃ j', c'.Rel (e.f i) j'
this : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i))
⊢ homologyMap 0 (e.f i) = 0
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyGE n → ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)

Tactic:
intro _ i hi

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero (K.X i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyLE n → ∀ (i : ℤ), n < i → IsZero (K.X i)

Tactic:
intro _ i hi

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ IsZero (K.X i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsGE n → ∀ i < n, ExactAt K i

Tactic:
intro _ i hi

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsGE n
i : ℤ
hi : i < n
⊢ ExactAt K i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsLE n → ∀ (i : ℤ), n < i → ExactAt K i

Tactic:
intro _ i hi

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsLE n
i : ℤ
hi : n < i
⊢ ExactAt K i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n : ℤ
⊢ IsStrictlyLE ((single C (up ℤ) n).obj A) n

Tactic:
rw [isStrictlyLE_iff]
  intro i hi
  exact isZero_single_obj_X _ _ _ _ (by lia)

Goal state after:
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom) ≫ (singleObjCyclesSelfIso c j B).inv =
    ((singleObjCyclesSelfIso c j A).hom ≫ f) ≫ (singleObjCyclesSelfIso c j B).inv

Tactic:
assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom ≫ (singleObjCyclesSelfIso c j B).inv =
    ((singleObjCyclesSelfIso c j A).hom ≫ f) ≫ (singleObjCyclesSelfIso c j B).inv
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom ≫ (singleObjCyclesSelfIso c j B).inv =
    ((singleObjCyclesSelfIso c j A).hom ≫ f) ≫ (singleObjCyclesSelfIso c j B).inv

Tactic:
assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom ≫ (singleObjCyclesSelfIso c j B).inv =
    (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ ((singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j) ≫ (singleObjHomologySelfIso c j B).hom =
    (f ≫ (singleObjHomologySelfIso c j B).inv) ≫ (singleObjHomologySelfIso c j B).hom

Tactic:
assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j ≫ (singleObjHomologySelfIso c j B).hom =
    (f ≫ (singleObjHomologySelfIso c j B).inv) ≫ (singleObjHomologySelfIso c j B).hom
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j ≫ (singleObjHomologySelfIso c j B).hom =
    (f ≫ (singleObjHomologySelfIso c j B).inv) ≫ (singleObjHomologySelfIso c j B).hom

Tactic:
assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j ≫ (singleObjHomologySelfIso c j B).hom =
    f ≫ (singleObjHomologySelfIso c j B).inv ≫ (singleObjHomologySelfIso c j B).hom