mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
D₂ : ComposableArrows (CochainComplex C ℤ) 2
w✝² w✝¹ w✝ : CochainComplex C ℤ
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
φ : ComposableArrows.mk₂ f g ⟶ D₂
⊢ (ComposableArrows.functorArrows (CochainComplex C ℤ) 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙
            composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        φ ≫
      ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            (D₂.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            (D₂.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))).mor₃ =
    ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            ((ComposableArrows.mk₂ f g).map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            ((ComposableArrows.mk₂ f g).map' 1 2 spectralObjectMappingCone._proof_2
              spectralObjectMappingCone._proof_3))).mor₃ ≫
      (ComposableArrows.functorArrows (CochainComplex C ℤ) 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
              shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        φ

Tactic:
obtain ⟨_, _, _, f', g', rfl⟩ := ComposableArrows.mk₂_surjective D₂

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
w✝⁵ w✝⁴ w✝³ : CochainComplex C ℤ
f : w✝⁵ ⟶ w✝⁴
g : w✝⁴ ⟶ w✝³
w✝² w✝¹ w✝ : CochainComplex C ℤ
f' : w✝² ⟶ w✝¹
g' : w✝¹ ⟶ w✝
φ : ComposableArrows.mk₂ f g ⟶ ComposableArrows.mk₂ f' g'
⊢ (ComposableArrows.functorArrows (CochainComplex C ℤ) 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙
            composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        φ ≫
      ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            ((ComposableArrows.mk₂ f' g').map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            ((ComposableArrows.mk₂ f' g').map' 1 2 spectralObjectMappingCone._proof_2
              spectralObjectMappingCone._proof_3))).mor₃ =
    ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            ((ComposableArrows.mk₂ f g).map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            ((ComposableArrows.mk₂ f g).map' 1 2 spectralObjectMappingCone._proof_2
              spectralObjectMappingCone._proof_3))).mor₃ ≫
      (ComposableArrows.functorArrows (CochainComplex C ℤ) 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
              shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        φ
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
X' : C
g : X ⟶ X'
⊢ ↑(toSingleMk (f ≫ g) h p' hp' ⋯) = ↑((toSingleMk f h p' hp' hf).postcomp ((singleFunctor C q).map g))

Tactic:
exact (Cochain.toSingleEquiv h).injective (by simp [Cochain.toSingleMk_postcomp])

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K ((singleFunctor C q).obj X) (n - 1)
g : K.X p'' ⟶ X
hα : δ (n - 1) n (Cochain.toSingleMk g ⋯) = Cochain.toSingleMk f h
hg : Cochain.toSingleMk g ⋯ = α
⊢ K.d p p'' ≫ (n.negOnePow • g) = f

Tactic:
Cochain.δ_toSingleMk _ _ _ _ h

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K ((singleFunctor C q).obj X) (n - 1)
g : K.X p'' ⟶ X
hα : n.negOnePow • Cochain.toSingleMk (K.d p p'' ≫ g) h = Cochain.toSingleMk f h
hg : Cochain.toSingleMk g ⋯ = α
⊢ K.d p p'' ≫ (n.negOnePow • g) = f
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app P =
    F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p

Tactic:
by
  rw [natTrans_eq]
  congr 2
  rw [← congr_app (((whiskeringLeft _ _ _).obj (toKaroubi _)).map_preimage τ) P.X]
  dsimp
  congr

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X : GradedObject J D
j : J
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ =
    (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)

Tactic:
simp [mapBifunctorRightUnitorCofan]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ : ℤ
⊢ (X.H n₀).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) = 0

Tactic:
subst h
  exact (X.exact₂' n₀ (mk₂ f g)).zero 0

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero ((X.H n₀).obj (mk₁ f))
h₂ : IsZero ((X.H n₁).obj (mk₁ f))
⊢ IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))

Tactic:
have := X.mono_H_map_twoδ₁Toδ₀ n₀ f g fg hfg h₁

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero ((X.H n₀).obj (mk₁ f))
h₂ : IsZero ((X.H n₁).obj (mk₁ f))
this : Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
⊢ IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ ≫ X.pOpcycles f g n₁ = 0

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

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₁ : ℤ
hn₁ : n₁ - 1 + 1 = n₁
⊢ X.δ f g (n₁ - 1) n₁ hn₁ ≫ X.pOpcycles f g n₁ = 0
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).Exact

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

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₁ : ℤ
hn₁ : n₁ - 1 + 1 = n₁
⊢ (X.cokernelSequenceOpcycles f g (n₁ - 1) n₁ hn₁).Exact
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
a₁✝ : ↑{i | i.1 + i.2.1 + i.2.2 = n}
⊢ ∀ ⦃a₂ : ↑{i | i.1 + i.2.1 + i.2.2 = n}⦄,
    (fun x ↦
            match x with
            | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩))
          a₁✝ =
        (fun x ↦
            match x with
            | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩))
          a₂ →
      a₁✝ = a₂

Tactic:
_

Goal state after:
I : Type u
inst✝² : AddMonoid I
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
n : ℕ
a₁✝ a₂✝ : ↑{i | i.1 + i.2.1 + i.2.2 = n}
⊢ (fun x ↦
          match x with
          | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩))
        a₁✝ =
      (fun x ↦
          match x with
          | ⟨(i₁, i₂, i₃), hi⟩ => (⟨i₁, ⋯⟩, ⟨i₂, ⋯⟩, ⟨i₃, ⋯⟩))
        a₂✝ →
    a₁✝ = a₂✝
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f₁ : i₀ ⟶ i₁
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₁ n₀ n₁ n₂ hn₁ hn₂).hom = (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom

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

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f₁ : i₀ ⟶ i₁
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ X.πE (𝟙 i₀) f₁ (𝟙 i₁) (n₁ - 1) n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₁ (n₁ - 1) n₁ n₂ hn₁ hn₂).hom =
    (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').hom =
    (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      (X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).hom

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

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').hom =
    (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).hom
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').inv =
    (X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).inv ≫
      (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).inv

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

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').inv =
    (X.EIsoH (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv ≫
      (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ (n₁ - 1) n₁ n₂ hn₁' ⋯ ⋯).inv
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq : κ
i₀ i₁ i₂ i₃ : ι
h₀ : i₀ = data.i₀ r pq ⋯
h₁ : i₁ = data.i₁ pq
h₂ : i₂ = data.i₂ pq
h₃ : i₃ = data.i₃ r pq ⋯
n₀ n₁ n₂ : ℤ
h : n₁ = data.deg pq
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ pageX X data r pq hr = X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂

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

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq : κ
i₀ i₁ i₂ i₃ : ι
h₀ : i₀ = data.i₀ r pq ⋯
h₁ : i₁ = data.i₁ pq
h₂ : i₂ = data.i₂ pq
h₃ : i₃ = data.i₃ r pq ⋯
n₁ n₂ : ℤ
h : n₁ = data.deg pq
hn₂ : n₁ + 1 = n₂
hn₁ : n₁ - 1 + 1 = n₁
⊢ pageX X data r pq hr = X.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (n₁ - 1) n₁ n₂ hn₁ hn₂
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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 : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ n₂ hn₁ hn₂).inv
⊢ (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

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject 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 : h.cyclesIso.inv = 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₂
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  h.right.opcyclesIso.hom = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).inv ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁ =
    X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁

Tactic:
opcyclesIsoH_inv_hom_id ..

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  h.right.opcyclesIso.hom = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ (X.EIsoH f n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ 𝟙 ((X.H n₁).obj (mk₁ f)) =
    X.ιE (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂ ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y z : L
m n : M
x : L
f g : M →ₗ[R] N
⊢ { toFun := fun m ↦ ⁅x, (f + g) m⁆ - (f + g) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m ↦ ⁅x, g m⁆ - g ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext n
    simp only [coe_mk, AddHom.coe_mk, lie_add, add_apply]
    abel

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ pageD X data r pq pq' ⋯ ≫
      (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
        X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ =
    0

Tactic:
rw [pageD_eq X data r hr pq pq' h (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
      (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃))
      (homOfLE (data.le₃₃' hrr' hr pq' hi₃ hi₃'))
      (homOfLE (by simpa only [hi₃', data.i₃_next r r' _ _ h] using data.le₂₃ r pq))
      hi₀ hi₁ (by rw [hi₂, data.hc₀₂ r _ _ h])
      (by rw [hi₃, data.hc₁₃ r _ _ h]) (by rw [hi₃', data.i₃_next r r' _ _ h]) rfl
      (n₀ - 1) n₀ n₁ n₂ (by have := data.hc r pq pq' h; lia) (by simp) hn₁ hn₂,
      Category.assoc, Category.assoc, Iso.inv_hom_id_assoc,
      d_map_fourδ₄Toδ₃ .., comp_zero]

Goal state after:
case pos
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ 0 = 0
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
α✝ : Type u_5
⊢ ∀ {β : Type u_5} (a : α✝ ≃ β),
    (∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R P} [∀ (i : β), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
_

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
⊢ ∀ (a : α✝ ≃ β✝),
    (∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : β✝ → Submodule R P} [∀ (i : β✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
⊢ ∀ {M : β✝ → Submodule R P} [∀ (i : β✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
_

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
⊢ ∀ [∀ (i : β✝), IsArtinian R ↥(M✝ i)], IsArtinian R ↥(⨆ i, M✝ i)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
⊢ ∀ [∀ (i : β✝), IsArtinian R ↥(M✝ i)], IsArtinian R ↥(⨆ i, M✝ i)

Tactic:
_

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ i, M✝ i)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
α✝ : Type u_5
⊢ ∀ [Fintype α✝],
    (∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : Option α✝ → Submodule R P} [∀ (i : Option α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
_

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ : Type u_5
inst✝ : Fintype α✝
⊢ (∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
    ∀ {M : Option α✝ → Submodule R P} [∀ (i : Option α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ : Type u_5
inst✝ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
⊢ ∀ {M : Option α✝ → Submodule R P} [∀ (i : Option α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
_

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ : Type u_5
inst✝ : Fintype α✝
ih : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : Option α✝ → Submodule R P
⊢ ∀ [∀ (i : Option α✝), IsArtinian R ↥(M✝ i)], IsArtinian R ↥(⨆ i, M✝ i)