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
⊢ Pretriangulated.Triangle.mk
      ((composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        ((ComposableArrows.mapFunctorArrows (CochainComplex C ℤ) 0 1 0 2 2 SpectralObject._proof_6
              SpectralObject._proof_8 SpectralObject._proof_10 SpectralObject._proof_2 SpectralObject._proof_4).app
          D))
      ((composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        ((ComposableArrows.mapFunctorArrows (CochainComplex C ℤ) 0 2 1 2 2 SpectralObject._proof_8
              SpectralObject._proof_2 SpectralObject._proof_6 SpectralObject._proof_4 SpectralObject._proof_4).app
          D))
      ({
            app := fun D ↦
              ((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₃,
            naturality := ⋯ }.app
        D) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles

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✝
⊢ Pretriangulated.Triangle.mk
      ((composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        ((ComposableArrows.mapFunctorArrows (CochainComplex C ℤ) 0 1 0 2 2 SpectralObject._proof_6
              SpectralObject._proof_8 SpectralObject._proof_10 SpectralObject._proof_2 SpectralObject._proof_4).app
          (ComposableArrows.mk₂ f g)))
      ((composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        ((ComposableArrows.mapFunctorArrows (CochainComplex C ℤ) 0 2 1 2 2 SpectralObject._proof_8
              SpectralObject._proof_2 SpectralObject._proof_6 SpectralObject._proof_4 SpectralObject._proof_4).app
          (ComposableArrows.mk₂ f g)))
      ({
            app := fun D ↦
              ((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₃,
            naturality := ⋯ }.app
        (ComposableArrows.mk₂ f g)) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Homotopy (ProjectiveResolution.lift (f ≫ g) (projectiveResolution X✝) (projectiveResolution Z✝))
    (ProjectiveResolution.lift f (projectiveResolution X✝) (projectiveResolution Y✝) ≫
      ProjectiveResolution.lift g (projectiveResolution Y✝) (projectiveResolution Z✝))

Tactic:
apply ProjectiveResolution.liftCompHomotopy

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ QuasiIsoAt (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩) 0

Tactic:
rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros']

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ { X₁ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).X₁,
        X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).X₂,
        X₃ :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj
              ((ChainComplex.single₀ C).obj Z)).X₂,
        f := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).f,
        g :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map
              (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩)).τ₂,
        zero := ⋯ }.Exact ∧
    Epi
      ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map
          (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩)).τ₂

case zero.hg₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).g = 0

case zero.hf₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj ((ChainComplex.single₀ C).obj Z)).f = 0

case zero.hg₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj ((ChainComplex.single₀ C).obj Z)).g = 0
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

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✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D✝ : Type u_3
inst✝⁶ : Category.{v_3, u_3} D✝
inst✝⁵ : HasZeroObject D✝
inst✝⁴ : HasShift D✝ ℤ
inst✝³ : Preadditive D✝
inst✝² : ∀ (n : ℤ), (shiftFunctor D✝ n).Additive
inst✝¹ : Pretriangulated D✝
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
D : ComposableArrows ι' 2
⊢ Triangle.mk
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        ((mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app D))
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        ((mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app D))
      ({
            app := fun D ↦
              X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                X.δ'.app ((F.mapComposableArrows 2).obj D) ≫
                  (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
            naturality := ⋯ }.app
        D) ∈
    distinguishedTriangles

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

Goal state after:
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
⊢ Triangle.mk
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        ((mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4).app (mk₂ f g)))
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        ((mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4).app (mk₂ f g)))
      ({
            app := fun D ↦
              X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                X.δ'.app ((F.mapComposableArrows 2).obj D) ≫
                  (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
            naturality := ⋯ }.app
        (mk₂ f g)) ∈
    distinguishedTriangles
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
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝³ : X₃.HasTensor X₄
inst✝² : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
h'' : i₂ + i₃ + i₄ = i₂₃₄
hj : i₁ + i₂ + i₃ + i₄ = j
⊢ X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g

Tactic:
simpa only [assoc, ιTensorObj₄_eq X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j hj i₂₃₄ h''] using h i₁ i₂ i₃ i₄ hj

Goal state after:
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₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    X.δ f₁₂ f₃₄ n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃

Tactic:
subst h₁₂ h₃₄
  simp only [d, δ_toCycles_assoc, toCycles_πE_descE]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯

Tactic:
X.map_ιE f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄)
    (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄) n₁ n₂ n₃

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂'✝ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, 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 : ℤ
hn : n = data.deg pq
⊢ data.i₁ pq = data.i₀ r₀ pq ⋯

Tactic:
← data.hi₀₁

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, 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 : ℤ
hn : n = data.deg pq
⊢ data.i₀ r₀ pq ⋯ = data.i₀ r₀ pq ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, 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₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_3
⊢ data.i₁ pq = data.i₀ r₀ pq ⋯

Tactic:
← data.hi₀₁

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, 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₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_3
⊢ data.i₀ r₀ pq ⋯ = data.i₀ r₀ pq ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.FirstPage

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, 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₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_3
⊢ data.i₁ pq = data.i₀ r₀ pq ⋯

Tactic:
← data.hi₀₁

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, 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₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_3
⊢ data.i₀ r₀ pq ⋯ = data.i₀ r₀ pq ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq : κ
hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq
n : ℤ
hn : n = data.deg pq - 1
i₃ i₃' : ι
hi₃ : i₃ = data.i₃ r pq ⋯
hi₃' : i₃' = data.i₃ r' pq ⋯
⊢ i₃ ≤ i₃'

Tactic:
simpa only [hi₃, hi₃'] using data.i₃_le r r' pq

Goal state after:
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: case refine_1
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m

pp: case refine_2
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n

Tactic:
· exact (h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm

Goal state after:
case refine_2
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n
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 r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
h : ¬(c r).Rel pq' pq''
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂)

Tactic:
apply X.isIso_map_fourδ₁Toδ₀_of_isZero ..

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 r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
h : ¬(c r).Rel pq' pq''
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsZero ((X.H n₂).obj (mk₁ (homOfLE ⋯)))
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ IsUnit x ↔ IsRightRegular x

Tactic:
rw [IsRightRegular, IsUnit.isUnit_iff_mulRight_bijective, Bijective, and_iff_left_of_imp]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ (Injective fun x_1 ↦ x_1 * x) → Surjective fun x_1 ↦ x_1 * x
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n✝ : ℕ
hn✝¹ :
  ∀ (m : ℕ), n✝ ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n✝ = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn✝ : Jac * Jac ^ n✝ = Jac ^ n✝
ne✝ : ¬Ring.jacobson R ^ n✝ = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
n : ℕ
hn : Jac ^ n * N = N
⊢ Jac ^ n * Jac * N = N

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n✝ : ℕ
hn✝¹ :
  ∀ (m : ℕ), n✝ ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n✝ = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn✝ : Jac * Jac ^ n✝ = Jac ^ n✝
ne✝ : ¬Ring.jacobson R ^ n✝ = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
n : ℕ
hn : Jac ^ n * N = N
⊢ Jac ^ n * (Jac * N) = N
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)

Tactic:
mul_assoc,

Goal state after:
A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * (a * (a * b)) = a * (a * a * b)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : ↥L'
⊢ ⟨⁅↑(x✝ + y✝), ↑z✝⁆, ⋯⟩ = ⟨⁅↑x✝, ↑z✝⁆, ⋯⟩ + ⟨⁅↑y✝, ↑z✝⁆, ⋯⟩

Tactic:
apply SetCoe.ext

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : ↥L'
⊢ ↑⟨⁅↑(x✝ + y✝), ↑z✝⁆, ⋯⟩ = ↑(⟨⁅↑x✝, ↑z✝⁆, ⋯⟩ + ⟨⁅↑y✝, ↑z✝⁆, ⋯⟩)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : ↥L'
⊢ ⟨⁅↑x✝, ↑(y✝ + z✝)⁆, ⋯⟩ = ⟨⁅↑x✝, ↑y✝⁆, ⋯⟩ + ⟨⁅↑x✝, ↑z✝⁆, ⋯⟩

Tactic:
apply SetCoe.ext

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : ↥L'
⊢ ↑⟨⁅↑x✝, ↑(y✝ + z✝)⁆, ⋯⟩ = ↑(⟨⁅↑x✝, ↑y✝⁆, ⋯⟩ + ⟨⁅↑x✝, ↑z✝⁆, ⋯⟩)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ : ↥L'
⊢ ⟨⁅↑x✝, ↑x✝⁆, ⋯⟩ = 0

Tactic:
apply SetCoe.ext

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ : ↥L'
⊢ ↑⟨⁅↑x✝, ↑x✝⁆, ⋯⟩ = ↑0
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : ↥L'
⊢ ⟨⁅↑x✝, ↑⟨⁅↑y✝, ↑z✝⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅↑⟨⁅↑x✝, ↑y✝⁆, ⋯⟩, ↑z✝⁆, ⋯⟩ + ⟨⁅↑y✝, ↑⟨⁅↑x✝, ↑z✝⁆, ⋯⟩⁆, ⋯⟩

Tactic:
apply SetCoe.ext

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
x✝ y✝ z✝ : ↥L'
⊢ ↑⟨⁅↑x✝, ↑⟨⁅↑y✝, ↑z✝⁆, ⋯⟩⁆, ⋯⟩ = ↑(⟨⁅↑⟨⁅↑x✝, ↑y✝⁆, ⋯⟩, ↑z✝⁆, ⋯⟩ + ⟨⁅↑y✝, ↑⟨⁅↑x✝, ↑z✝⁆, ⋯⟩⁆, ⋯⟩)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
t✝ : R
x✝ y✝ : ↥L'
⊢ ⁅x✝, t✝ • y✝⁆ = t✝ • ⁅x✝, y✝⁆

Tactic:
apply SetCoe.ext

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
t✝ : R
x✝ y✝ : ↥L'
⊢ ↑⁅x✝, t✝ • y✝⁆ = ↑(t✝ • ⁅x✝, y✝⁆)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
by
  rw [← SetLike.mem_coe, lieSpan, coe_sInf]
  exact Set.mem_iInter₂

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
⊢ e ⁅x, e.toLinearEquiv.symm y'⁆ = ⁅e x, y'⁆

Tactic:
map_lie,

Goal state after:
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
⊢ ⁅e x, e (e.toLinearEquiv.symm y')⁆ = ⁅e x, y'⁆
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x y : L
m : ↥N
⊢ ⟨⁅x + y, ↑m⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑m⁆, ⋯⟩

Tactic:
apply SetCoe.ext

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x y : L
m : ↥N
⊢ ↑⟨⁅x + y, ↑m⁆, ⋯⟩ = ↑(⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑m⁆, ⋯⟩)
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : L
m n : ↥N
⊢ ⟨⁅x, ↑(m + n)⁆, ⋯⟩ = ⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅x, ↑n⁆, ⋯⟩

Tactic:
apply SetCoe.ext

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : L
m n : ↥N
⊢ ↑⟨⁅x, ↑(m + n)⁆, ⋯⟩ = ↑(⟨⁅x, ↑m⁆, ⋯⟩ + ⟨⁅x, ↑n⁆, ⋯⟩)
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x y : L
m : ↥N
⊢ ⟨⁅x, ↑⟨⁅y, ↑m⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅⁅x, y⁆, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑⟨⁅x, ↑m⁆, ⋯⟩⁆, ⋯⟩

Tactic:
apply SetCoe.ext

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x y : L
m : ↥N
⊢ ↑⟨⁅x, ↑⟨⁅y, ↑m⁆, ⋯⟩⁆, ⋯⟩ = ↑(⟨⁅⁅x, y⁆, ↑m⁆, ⋯⟩ + ⟨⁅y, ↑⟨⁅x, ↑m⁆, ⋯⟩⁆, ⋯⟩)