awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
α : mk₁ f ⟶ mk₁ f'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
⊢ Eq (α := (mk₃ (𝟙 i) f (𝟙 j)).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ (mk₃ (𝟙 i') f' (𝟙 j')).obj' 3 _proof_300✝)
    ((mk₃ (𝟙 i) f (𝟙 j)).map' 2 3 _proof_299✝ _proof_300✝ ≫ α.app 1)
    (α.app 1 ≫ (mk₃ (𝟙 i') f' (𝟙 j')).map' 2 3 _proof_299✝ _proof_300✝)

Tactic:
simp [Precomp.obj, Precomp.map]

Premises used: CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.Precomp.map
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
α : mk₁ f ⟶ mk₁ f'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
hβ : β = homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
subst :
  α =
    homMk₁ (NatTrans.app (homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯) 1)
      (NatTrans.app (homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯) 2) ⋯
⊢ α = homMk₁ (β.app 1) (β.app 2) ⋯

Tactic:
subst hβ
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
α : mk₁ f ⟶ mk₁ f'
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ α =
    homMk₁ (NatTrans.app (homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯) 1)
      (NatTrans.app (homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯) 2) ⋯

Tactic:
hom_ext₁ rfl rfl

Premises used: CategoryTheory.ComposableArrows.hom_ext₁, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
α : mk₁ f ⟶ mk₁ f'
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ α =
    homMk₁ (NatTrans.app (homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯) 1)
      (NatTrans.app (homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯) 2) ⋯

Tactic:
exact hom_ext₁ rfl rfl

Premises used: CategoryTheory.ComposableArrows.hom_ext₁, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
α : mk₁ f ⟶ mk₁ f'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
hβ : β = homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
obtain :
  ∀
    (hβ :
      β =
        homMk₃ (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 0) (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 0)
          (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 1) (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 1) ⋯ ⋯ ⋯),
    X.map (𝟙 i) f (𝟙 j) (𝟙 i') f' (𝟙 j') β n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
      (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)
⊢ X.map (𝟙 i) f (𝟙 j) (𝟙 i') f' (𝟙 j') β n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.H n₁).map α

Tactic:
obtain rfl : α = homMk₁ (β.app 1) (β.app 2) (naturality' β 1 2) := by
    subst hβ
    exact hom_ext₁ rfl rfl

Premises used: CategoryTheory.ComposableArrows.homMk₁, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hβ :
  β =
    homMk₃ (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 0) (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 0)
      (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 1) (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 1) ⋯ ⋯ ⋯
⊢ X.map (𝟙 i) f (𝟙 j) (𝟙 i') f' (𝟙 j') β n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)

Tactic:
(ShortComplex.LeftHomologyMapData.ofZeros
    (X.shortComplexMap _ _ _ _ _ _ β n₀ n₁ n₂ hn₁ hn₂) ..).homologyMap_comm

Premises used: CategoryTheory.Abelian.SpectralObject.shortComplexMap, CategoryTheory.Abelian.SpectralObject.E, CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comm, CategoryTheory.ShortComplex.LeftHomologyData.ofZeros, CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros, CategoryTheory.Abelian.SpectralObject.map
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hβ :
  β =
    homMk₃ (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 0) (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 0)
      (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 1) (NatTrans.app (homMk₁ (β.app 1) (β.app 2) ⋯) 1) ⋯ ⋯ ⋯
⊢ X.map (𝟙 i) f (𝟙 j) (𝟙 i') f' (𝟙 j') β n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)

Tactic:
exact (ShortComplex.LeftHomologyMapData.ofZeros
    (X.shortComplexMap _ _ _ _ _ _ β n₀ n₁ n₂ hn₁ hn₂) ..).homologyMap_comm

Premises used: CategoryTheory.Abelian.SpectralObject.shortComplexMap, CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comm, CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ n₀ - 1 + 1 = n₀

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : autoParam (n₀ + 1 = n₁) cyclesIsoH_inv._auto_1
⊢ 𝟙 i₀ ≫ f = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw : (X.cyclesIsoH f n₀ n₁ hn₁).inv ≫ X.iCycles (𝟙 i₀) f n₀ = (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).inv = X.toCycles (𝟙 i₀) f f ⋯ n₀

Tactic:
rw [← cancel_mono (X.iCycles (𝟙 _) f n₀), toCycles_i]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.cancel_mono, CategoryTheory.Abelian.SpectralObject.toCycles_i, CategoryTheory.Abelian.SpectralObject.iCycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
dsimp :
  (Iso.inv
          (ShortComplex.LeftHomologyData.cyclesIso
            (ShortComplex.HomologyData.left (X.homologyDataIdId f (n₀ - 1) n₀ n₁ ⋯ ⋯))) ≫
        (X.cyclesIso (𝟙 i₀) f (𝟙 i₁) (n₀ - 1) n₀ n₁ ⋯ hn₁).hom) ≫
      X.iCycles (𝟙 i₀) f n₀ =
    (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).inv ≫ X.iCycles (𝟙 i₀) f n₀ = (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)

Tactic:
dsimp [cyclesIsoH]

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesIsoH
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
simp : (X.H n₀).map (𝟙 (mk₁ f)) = (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)
⊢ (Iso.inv
          (ShortComplex.LeftHomologyData.cyclesIso
            (ShortComplex.HomologyData.left (X.homologyDataIdId f (n₀ - 1) n₀ n₁ ⋯ ⋯))) ≫
        (X.cyclesIso (𝟙 i₀) f (𝟙 i₁) (n₀ - 1) n₀ n₁ ⋯ hn₁).hom) ≫
      X.iCycles (𝟙 i₀) f n₀ =
    (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)

Tactic:
simp only [Category.assoc, cyclesIso_hom_i, homologyDataIdId_left_i,
    ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles, ← Functor.map_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_i, CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i, CategoryTheory.Functor.map_id, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
e_a : 𝟙 (mk₁ f) = twoδ₁Toδ₀ (𝟙 i₀) f f ⋯
⊢ (X.H n₀).map (𝟙 (mk₁ f)) = (X.H n₀).map (twoδ₁Toδ₀ (𝟙 i₀) f f ⋯)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : autoParam (n₀ + 1 = n₁) cyclesIsoH_hom_inv_id._auto_1
⊢ 𝟙 i₀ ≫ f = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).hom ≫ X.toCycles (𝟙 i₀) f f ⋯ n₀ = 𝟙 (X.cycles (𝟙 i₀) f n₀)

Tactic:
simpa using (X.cyclesIsoH f n₀ n₁ hn₁).hom_inv_id

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesIsoH, CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : autoParam (n₀ + 1 = n₁) cyclesIsoH_inv_hom_id._auto_1
⊢ 𝟙 i₀ ≫ f = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.toCycles (𝟙 i₀) f f ⋯ n₀ ≫ (X.cyclesIsoH f n₀ n₁ hn₁).hom = 𝟙 ((X.H n₀).obj (mk₁ f))

Tactic:
simpa using (X.cyclesIsoH f n₀ n₁ hn₁).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Abelian.SpectralObject.cyclesIsoH
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ n₁ + 1 = n₁ + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : autoParam (n₀ + 1 = n₁) opcyclesIsoH_hom._auto_1
⊢ f ≫ 𝟙 i₁ = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
rw : X.pOpcycles f (𝟙 i₁) n₁ ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).hom = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)
⊢ (X.opcyclesIsoH f n₀ n₁ hn₁).hom = X.fromOpcycles f (𝟙 i₁) f ⋯ n₁

Tactic:
rw [← cancel_epi (X.pOpcycles f (𝟙 _) n₁), p_fromOpcycles]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.pOpcycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
dsimp :
  X.pOpcycles f (𝟙 i₁) n₁ ≫
      (X.opcyclesIso (𝟙 i₀) f (𝟙 i₁) n₀ n₁ (n₁ + 1) hn₁ ⋯).inv ≫
        Iso.hom
          (ShortComplex.RightHomologyData.opcyclesIso
            (ShortComplex.HomologyData.right (X.homologyDataIdId f n₀ n₁ (n₁ + 1) ⋯ ⋯))) =
    (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)
⊢ X.pOpcycles f (𝟙 i₁) n₁ ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).hom = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)

Tactic:
dsimp [opcyclesIsoH]

Premises used: CategoryTheory.Abelian.SpectralObject.opcyclesIsoH
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
simp : (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)
⊢ X.pOpcycles f (𝟙 i₁) n₁ ≫
      (X.opcyclesIso (𝟙 i₀) f (𝟙 i₁) n₀ n₁ (n₁ + 1) hn₁ ⋯).inv ≫
        Iso.hom
          (ShortComplex.RightHomologyData.opcyclesIso
            (ShortComplex.HomologyData.right (X.homologyDataIdId f n₀ n₁ (n₁ + 1) ⋯ ⋯))) =
    (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)

Tactic:
simp only [p_opcyclesIso_inv_assoc, homologyDataIdId_right_p, ← Functor.map_id,
    ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom]

Premises used: CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_p, CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom, CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv_assoc, CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
e_a : 𝟙 (mk₁ f) = twoδ₂Toδ₁ f (𝟙 i₁) f ⋯
⊢ (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : autoParam (n₀ + 1 = n₁) opcyclesIsoH_hom_inv_id._auto_1
⊢ f ≫ 𝟙 i₁ = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.fromOpcycles f (𝟙 i₁) f ⋯ n₁ ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv = 𝟙 (X.opcycles f (𝟙 i₁) n₁)

Tactic:
simpa using (X.opcyclesIsoH f n₀ n₁ hn₁).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : autoParam (n₀ + 1 = n₁) opcyclesIsoH_inv_hom_id._auto_1
⊢ f ≫ 𝟙 i₁ = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.opcyclesIsoH f n₀ n₁ hn₁).inv ≫ X.fromOpcycles f (𝟙 i₁) f ⋯ n₁ = 𝟙 ((X.H n₁).obj (mk₁ f))

Tactic:
simpa using (X.opcyclesIsoH f n₀ n₁ hn₁).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ 𝟙 i ≫ f = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
rw : h.i = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)
⊢ Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv

Tactic:
rw [← cancel_mono (X.cyclesIso ..).hom,
      Category.assoc, Iso.inv_hom_id, Category.comp_id,
      ← cancel_mono (X.iCycles ..), Category.assoc, cyclesIso_hom_i ..,
      h.cyclesIso_inv_comp_iCycles, toCycles_i]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i, CategoryTheory.Abelian.SpectralObject.cyclesIso, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom, CategoryTheory.Abelian.SpectralObject.toCycles_i, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles, CategoryTheory.Abelian.SpectralObject.iCycles
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
dsimp : 𝟙 ((X.H n₁).obj (mk₁ f)) = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)
⊢ h.i = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)

Tactic:
dsimp [h]
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
rw : (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)
⊢ 𝟙 ((X.H n₁).obj (mk₁ f)) = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)

Tactic:
rw [← Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
e_a : 𝟙 (mk₁ f) = twoδ₁Toδ₀ (𝟙 i) f f ⋯
⊢ (X.H n₁).map (𝟙 (mk₁ f)) = (X.H n₁).map (twoδ₁Toδ₀ (𝟙 i) f f ⋯)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
⊢ Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv

Tactic:
have : h.cyclesIso.inv =
      X.toCycles (𝟙 i) f f (by simp) n₁ ≫
        (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv := by
    rw [← cancel_mono (X.cyclesIso ..).hom,
      Category.assoc, Iso.inv_hom_id, Category.comp_id,
      ← cancel_mono (X.iCycles ..), Category.assoc, cyclesIso_hom_i ..,
      h.cyclesIso_inv_comp_iCycles, toCycles_i]
    dsimp [h]
    rw [← Functor.map_id]
    congr 1
    cat_disch
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
this : Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv
⊢ n₀ = n₁ - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).LeftHomologyData := (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left
this : Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv
obtain :
  ∀ (hn₁ : n₁ - 1 + 1 = n₁),
    let h := (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left;
    ∀ (this : Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv),
      (X.cyclesIsoH f n₁ n₂ hn₂).hom ≫ (X.EIsoH f (n₁ - 1) n₁ n₂ hn₁ hn₂).inv =
        X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
⊢ (X.cyclesIsoH f n₁ n₂ hn₂).hom ≫ (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).inv = X.πE (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂

Tactic:
obtain rfl : n₀ = n₁ - 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.Page
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : Iso.inv h.cyclesIso = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
rw : (X.EIsoH f (n₁ - 1) n₁ n₂ hn₁ hn₂).inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
⊢ (X.cyclesIsoH f n₁ n₂ hn₂).hom ≫ (X.EIsoH f (n₁ - 1) n₁ n₂ hn₁ hn₂).inv = X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂

Tactic:
rw [← cancel_epi (X.cyclesIsoH f n₁ n₂ hn₂).inv,
    cyclesIsoH_inv .., cyclesIsoH_inv_hom_id_assoc ..]

Premises used: CategoryTheory.Abelian.SpectralObject.cyclesIsoH, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv, CategoryTheory.Iso.inv