mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case e'_3
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₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ (shiftFunctor C 1).map
      (X.ω₁.map
        ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
          (F.mapComposableArrows 1).map (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
            (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom)) =
    (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))

Tactic:
congr 2

Goal state after:
case e'_3
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₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
      (F.mapComposableArrows 1).map (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
        (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom =
    homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

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

Tactic:
· rw [quasiIsoAt_iff_exactAt']
      · apply ofComplex_exactAt_succ
      · apply ChainComplex.exactAt_succ_single_obj

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (P.complex.d 1 0) ≫ F.map (P.π.f 0) = 0

Tactic:
← F.map_comp,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (P.complex.d 1 0 ≫ P.π.f 0) = 0
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i : I
⊢ (GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0) ▷ K.X i ≫
      GradedObject.Monoidal.ιTensorObj (tensorUnit C c).X K.X 0 i i ⋯ =
    (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫ (tensorUnit C c).ιTensorObj K 0 i i ⋯

Tactic:
congr 2

Goal state after:
case e_a
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i : I
⊢ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 = (singleObjXSelf c 0 (𝟙_ C)).inv
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ K.X i ◁ (GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0) ≫
      GradedObject.Monoidal.ιTensorObj K.X (tensorUnit C c).X i 0 i ⋯ =
    K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) i 0 i ⋯

Tactic:
congr 2

Goal state after:
case e_a
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 = (singleObjXSelf c 0 (𝟙_ C)).inv
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 ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
    X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
      X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂

Tactic:
ext
  all_goals dsimp; rw [← Functor.map_comp]; congr 1; cat_disch

Goal state after:
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
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
by rw [hi₂, data.hi₂₃]

Goal state after:
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
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
by rw [hi₂, data.hi₂₃]

Goal state after:
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
⊢ i₂ = data.i₃ r₀ pq ⋯

Tactic:
by rw [hi₂, data.hi₂₃]

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' : κ
i₀' i₀ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
⊢ i₀' ≤ i₀

Tactic:
by
  rw [hi₀', hi₀]
  exact data.antitone_i₀ r r' pq'

Goal state after:
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 ⋯
⊢ IsZero ((X.H n).obj (mk₁ (homOfLE ⋯)))

Tactic:
subst hi₀' hi₀

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 ι
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
⊢ IsZero ((X.H n).obj (mk₁ (homOfLE ⋯)))
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 ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : β.app 0 = α.app 0
h₁ : β.app 1 = α.app 2
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map
        (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
          homMk₁ ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 1) ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 2)
            ⋯) ≫
      X.pOpcycles f₂' f₃' n₁ =
    (X.H n₁).map
        (homMk₁ (β.app 0) (β.app 1) ⋯ ≫
          homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯) ≫
      X.pOpcycles f₂' f₃' n₁

Tactic:
congr 2

Goal state after:
case e_a
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₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : β.app 0 = α.app 0
h₁ : β.app 1 = α.app 2
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
      homMk₁ ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 1) ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 2) ⋯ =
    homMk₁ (β.app 0) (β.app 1) ⋯ ≫
      homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x y : L
m : M
⊢ ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

Tactic:
rw [leibniz_lie, add_sub_cancel_right]

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

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : LieRing L₂
inst✝² : LieAlgebra R L₂
inst✝¹ : LieRing L₃
inst✝ : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x y : L₂
⊢ g ⁅x, y⁆ = g ⁅f (g x), f (g y)⁆

Tactic:
conv_lhs => rw [← h₂ x, ← h₂ y]

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

Goal state before:
pp: R : Type u
L : Type v
M : 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✝ : IsFaithful R L M
L' : LieSubalgebra R L
⊢ IsFaithful R (↥L') M

Tactic:
refine ⟨(?_ : Injective (toEnd R L M ∘ ((↑) : L' → L)))⟩
  exact IsFaithful.injective_toEnd.comp Subtype.val_injective

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) - (⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆) = 0

Tactic:
← sub_sub,

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) - ⁅L (a * a), L b⁆ - ⁅L (b * b), L a⁆ = 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
K : LieSubalgebra R L
⊢ K.incl.range = K

Tactic:
← toSubmodule_inj

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K.incl.range.toSubmodule = K.toSubmodule
Module: Mathlib.Algebra.Lie.IdealOperations

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
⊢ map N.incl (comap N.incl N') = N ⊓ N'

Tactic:
← toSubmodule_inj

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
⊢ ↑(map N.incl (comap N.incl N')) = ↑(N ⊓ N')
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
⊢ ↑(map f I) = Submodule.map ↑f ↑I

Tactic:
by
  let J : LieIdeal R L' :=
    { (I : Submodule R L).map (f : L →ₗ[R] L') with
      lie_mem := fun {x y} hy ↦ by
        have hy' : ∃ x : L, x ∈ I ∧ f x = y := by simpa [hy]
        obtain ⟨z₂, hz₂, rfl⟩ := hy'
        obtain ⟨z₁, rfl⟩ := h x
        simp only [LieHom.coe_toLinearMap, SetLike.mem_coe, Set.mem_image, Submodule.mem_carrier,
          Submodule.map_coe]
        use ⁅z₁, z₂⁆
        exact ⟨I.lie_mem hz₂, f.map_lie z₁ z₂⟩ }
  rw [map, toLieSubalgebra_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]
  exact ⟨J, rfl⟩

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

Goal state before:
pp: case mp
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 : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
m : M
⊢ (∃ x n, ⁅↑x, ↑n⁆ = m) → ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m

Tactic:
rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩

Goal state after:
case mp
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 : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ∃ x_1 ∈ I, ∃ n_1 ∈ N, ⁅x_1, n_1⁆ = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆
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
m : M
s : Set (LieSubmodule R L M)
⊢ s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
hne

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
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥

Tactic:
trivial_lie_zero

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : 0 = m
⊢ m ∈ ↑⊥
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
⊢ p * C p.leadingCoeff⁻¹ = minpoly A x

Tactic:
by
  have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero
  apply eq_of_irreducible_of_monic
  · exact Associated.irreducible ⟨⟨C p.leadingCoeff⁻¹, C p.leadingCoeff,
      by rwa [← C_mul, inv_mul_cancel₀, C_1], by rwa [← C_mul, mul_inv_cancel₀, C_1]⟩, rfl⟩ hp1
  · rw [aeval_mul, hp2, zero_mul]
  · rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
y : ↥R[x]
hy : y ∈ Ideal.map (algebraMap R ↥R[x]) I
z : ↥R[x]
hz : z ∈ Ideal.span {⟨x, ⋯⟩}
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
hw : z = ⟨x, ⋯⟩ * w
q : R[X]
hq : (aeval x) q = ↑w
⊢ ∃ p, p.leadingCoeff - 1 ∈ I ∧ (aeval ⅟x) p = 0

Tactic:
use (1 - p - X * q).reverse

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
y : ↥R[x]
hy : y ∈ Ideal.map (algebraMap R ↥R[x]) I
z : ↥R[x]
hz : z ∈ Ideal.span {⟨x, ⋯⟩}
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
hw : z = ⟨x, ⋯⟩ * w
q : R[X]
hq : (aeval x) q = ↑w
⊢ (1 - p - X * q).reverse.leadingCoeff - 1 ∈ I ∧ (aeval ⅟x) (1 - p - X * q).reverse = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : f✝ pb.gen = g pb.gen
f : R[X]
⊢ f✝ ((aeval pb.gen) f) = g ((aeval pb.gen) f)

Tactic:
← Polynomial.aeval_algHom_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : f✝ pb.gen = g pb.gen
f : R[X]
⊢ (aeval (f✝ pb.gen)) f = g ((aeval pb.gen) f)
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : f✝ pb.gen = g pb.gen
f : R[X]
⊢ (aeval (f✝ pb.gen)) f = g ((aeval pb.gen) f)

Tactic:
← Polynomial.aeval_algHom_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : f✝ pb.gen = g pb.gen
f : R[X]
⊢ (aeval (f✝ pb.gen)) f = (aeval (g pb.gen)) f
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {C x, X - C y} = Ideal.span {X - C y} ⊔ Ideal.span {C x}

Tactic:
by
      rw [Ideal.span_insert, sup_comm]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {↑(quotientSpanXSubCAlgEquiv y) ((Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (C x))} = Ideal.span {x}

Tactic:
congr 2

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ ↑(quotientSpanXSubCAlgEquiv y) ((Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (C x)) = x
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Tactic:
simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root : ∑ x, p.coeff ↑x • pb.basis x = 0
⊢ (monomial ↑i) (p.coeff ↑i) = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ ∑ x, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x + pb.gen ^ pb.dim = (aeval pb.gen) pb.minpolyGen

Tactic:
aeval_eq_sum_range,

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ ∑ x, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x + pb.gen ^ pb.dim =
    ∑ i ∈ Finset.range (pb.minpolyGen.natDegree + 1), pb.minpolyGen.coeff i • pb.gen ^ i
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p : MvPolynomial σ (R ⧸ I)) (n : σ),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
            (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X n)) =
        p * X n

Tactic:
· intro p i hp
    simp only [hp, coe_eval₂Hom, Ideal.Quotient.lift_mk, eval₂_mul, map_mul, eval₂_X]

Goal state after: