mathlib-initiative/mathlib-tactics huggingface dataset:
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₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x y : L
⊢ (↑f).rangeRestrict.toFun ⁅x, y⁆ = ⁅(↑f).rangeRestrict.toFun x, (↑f).rangeRestrict.toFun y⁆

Tactic:
apply Subtype.ext
      exact f.map_lie x y

Goal state after:
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
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
this : ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆
⊢ ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆

Tactic:
exact le_antisymm this h

Goal state after:
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
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑(⁅I, N⁆ ⊔ ⁅I, N'⁆)

Tactic:
rintro m ⟨x, ⟨n, hn⟩, h⟩

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
inst✝ : LieAlgebra R L
I : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅↑x, ↑⟨n, hn⟩⁆ = m
⊢ m ∈ ↑(⁅I, N⁆ ⊔ ⁅I, N'⁆)
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 : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
this : ⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆
⊢ ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆

Tactic:
exact le_antisymm this h

Goal state after:
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
p : A[X]
hp : (Polynomial.aeval x) p = 0
⊢ minpoly A x ∣ p

Tactic:
by_cases hp0 : p = 0

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : p = 0
⊢ minpoly A x ∣ p

case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
⊢ minpoly A x ∣ p
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case inr
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ 0
h : 0 < (minpoly A x).degree
⊢ minpoly A x = 1

Tactic:
exact (this.not_gt h).elim

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

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

Tactic:
mul_comm a b

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) =
    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
p : A[X]
ne_zero : p ≠ 0
root : (aeval pb.gen) p = 0
⊢ pb.dim ≤ p.natDegree

Tactic:
refine le_of_not_gt fun hlt => ne_zero ?_

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
root : (aeval pb.gen) p = 0
hlt : p.natDegree < pb.dim
⊢ p = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ (pb.equivOfRoot (pb.map e) h₁ h₂) ((aeval pb.gen) f) = e ((aeval pb.gen) f)

Tactic:
simp [aeval_algEquiv]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
c : R
hc : d = a * c
⊢ d ∣ y

Tactic:
hc,

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : a * c * (a * c) = a * b
hc : d = a * c
⊢ d ∣ y
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ b = d * c

Tactic:
hc,

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ b = a * c * c
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑(cons a s ha)).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree (∏ i ∈ cons a s ha, f i)

Tactic:
rw [Finset.prod_cons, squarefree_mul_iff]
    rw [Finset.coe_cons, Set.pairwise_insert] at hs
    refine ⟨.prod_right fun i hi ↦ ?_, hs' a (by simp), ?_⟩
    · exact (hs.right i (by simp [hi]) fun h ↦ ha (h ▸ hi)).left
    · exact ih hs.left fun i hi ↦ hs' i <| Finset.mem_cons_of_mem hi

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
⊢ LinearMap.det 0 = 0

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
val✝ : Fintype ι
⊢ LinearMap.det 0 = 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁ + 0 ∧ (expand F (p ^ 0)) g₂ = g₂

Tactic:
rw [add_zero, pow_zero, expand_one]

Goal state after:
case inr
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁ ∧ g₂ = g₂
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
⊢ f = 0

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
val✝ : Fintype ι
⊢ f = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ LinearMap.det f.dualMap = LinearMap.det f

Tactic:
set b := Module.Free.chooseBasis R M
  have : Fintype (Module.Free.ChooseBasisIndex R M) :=
    Module.Free.ChooseBasisIndex.fintype R M
  rw [← LinearMap.det_toMatrix b, ← LinearMap.det_toMatrix b.dualBasis]
  simp [LinearMap.dualMap_def, LinearMap.toMatrix_transpose]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ ∑ k ∈ range k, ((↑k !)⁻¹ • a ^ k) • m + ∑ k ∈ Ico k (nilpotencyClass a), ((↑k !)⁻¹ • a ^ k) • m =
    ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
suffices ∑ i ∈ Ico k (nilpotencyClass a), ((i.factorial : ℚ)⁻¹ • (a ^ i)) • m = 0 by
    simp_rw [this, add_zero, smul_assoc]

Goal state after:
case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ ∑ i ∈ Ico k (nilpotencyClass a), ((↑i !)⁻¹ • a ^ i) • m = 0
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : End R M
inst✝ : Module.Finite R M
hf : f.IsFinitelySemisimple
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq₁ : q ∈ f.invtSubmodule
hq₂ : Disjoint p q
hq₃ : p ⊔ q = ⊤
⊢ ∃ q ∈ f.invtSubmodule, IsCompl p q

Tactic:
exact ⟨q, hq₁, hq₂, codisjoint_iff.mpr hq₃⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case refine_4
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁵ : Module.Finite K R
this✝⁴ : Module.Finite R S
this✝³ : Module.Finite K S
this✝² : IsArtinianRing R
this✝¹ : IsReduced R
this✝ : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
⊢ a.IsSemisimple

Tactic:
obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp (this ha)

Goal state after:
case refine_4
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁵ : Module.Finite K R
this✝⁴ : Module.Finite R S
this✝³ : Module.Finite K S
this✝² : IsArtinianRing R
this✝¹ : IsReduced R
this✝ : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : φ p ∈ K[f, g]
⊢ (φ p).IsSemisimple
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
a b : K[X]
h : a * P ^ k + b * P' = 1
⊢ IsUnit ((aeval ff) P')

Tactic:
replace h : (aeval f b) * (aeval f P') = 1 := by
      simpa only [map_add, map_mul, map_one, minpoly.dvd_iff.mp nil, mul_zero, zero_add]
        using (aeval f).congr_arg h

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
a b : K[X]
h : (aeval f) b * (aeval f) P' = 1
⊢ IsUnit ((aeval ff) P')
Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
⊢ (ad K (Module.End K V)) n ∈ K[(ad K (Module.End K V)) (n + s)]

Tactic:
by
  have : ad K _ n = ad K _ (n + s) - ad K _ s := by simp [map_add]
  rw [this]
  exact sub_mem (Algebra.self_mem_adjoin_singleton K _) (ad_mem_adjoin_of_isSemisimple hc hn hs)

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (derivative (map (algebraMap R S) P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
⊢ IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))

Tactic:
have : IsUnit (aeval r₁ (derivative P)) :=
      isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' hr₁

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (derivative (map (algebraMap R S) P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P))
⊢ IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : SMul M R
inst✝¹ : Semigroup R
inst✝ : SMulCommClass M R R
x y : R
m : M
h : x ∣ y
k : R
hk : y = x * k
⊢ m • y = x * m • k

Tactic:
by rw [mul_smul_comm, ← hk]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
let D₁ : LieIdeal R L →o LieIdeal R L :=
    { toFun := fun I => ⁅I, I⁆
      monotone' := fun I J h => LieSubmodule.mono_lie h h }

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I ↦ ⁅I, I⁆, monotone' := ⋯ }
⊢ D (k + l) (I + J) ≤ D k I + D l J
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x ⊗ₜ[R] y)) z) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))) z +
        ((bracket' R A L M) (x ⊗ₜ[R] y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

Tactic:
intro a₂ l₂
      refine z.induction_on ?_ ?_ ?_
      · simp only [map_zero, add_zero]
      · intro a₃ l₃; simp only [bracket'_tmul]
        rw [mul_left_comm a₂ a₁ a₃, mul_assoc, leibniz_lie, TensorProduct.tmul_add]
      · grind

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedLengthOfIdeal R L I = k + 1 ↔ IsLieAbelian ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥

Tactic:
by
  rw [abelian_iff_derived_succ_eq_bot]
  let s := { k | derivedSeriesOfIdeal R L k I = ⊥ }
  change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
  have hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := by
    intro k₁ k₂ h₁₂ h₁
    suffices derivedSeriesOfIdeal R L k₂ I ≤ ⊥ by exact eq_bot_iff.mpr this
    change derivedSeriesOfIdeal R L k₁ I = ⊥ at h₁; rw [← h₁]
    exact derivedSeriesOfIdeal_antitone I h₁₂
  exact Nat.sInf_upward_closed_eq_succ_iff hs k

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

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
⊢ IsNilpotent L M ↔ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
by
  simp [isNilpotent_iff_int, SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
⊢ ∃ K', IsEngelian R ↥K' ∧ K < K'

Tactic:
by
  obtain ⟨x, hx₁, hx₂⟩ := SetLike.exists_of_lt hK₂
  let K' : LieSubalgebra R L :=
    { (R ∙ x) ⊔ (K : Submodule R L) with
      lie_mem' := fun {y z} => LieSubalgebra.lie_mem_sup_of_mem_normalizer hx₁ }
  have hxK' : x ∈ K' := Submodule.mem_sup_left (Submodule.subset_span (Set.mem_singleton _))
  have hKK' : K ≤ K' := (LieSubalgebra.toSubmodule_le_toSubmodule K K').mp le_sup_right
  have hK' : K' ≤ K.normalizer := by
    rw [← LieSubalgebra.toSubmodule_le_toSubmodule]
    exact sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) hK₂.le
  refine ⟨K', ?_, lt_iff_le_and_ne.mpr ⟨hKK', fun contra => hx₂ (contra.symm ▸ hxK')⟩⟩
  intro M _i1 _i2 _i3 _i4 h
  obtain ⟨I, hI₁ : (I : LieSubalgebra R K') = LieSubalgebra.ofLe hKK'⟩ :=
    LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer hKK' hK'
  have hI₂ : R ∙ (⟨x, hxK'⟩ : K') ⊔ LieSubmodule.toSubmodule I = ⊤ := by
    rw [← LieIdeal.toLieSubalgebra_toSubmodule R K' I, hI₁]
    apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype
    simp only [LieSubalgebra.coe_ofLe, Submodule.map_sup, Submodule.map_subtype_range_inclusion,
      Submodule.map_top, Submodule.range_subtype]
    rw [Submodule.map_subtype_span_singleton]
  have e : K ≃ₗ⁅R⁆ I :=
    (LieSubalgebra.equivOfLe hKK').trans
      (LieEquiv.ofEq _ _ ((LieSubalgebra.coe_set_eq _ _).mpr hI₁.symm))
  have hI₃ : LieAlgebra.IsEngelian R I := e.isEngelian_iff.mp hK₁
  exact LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop hI₂ (h _) (hI₃ _ fun x => h x)

Goal state after:
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := ⋯
⊢ (Basis.ofVectorSpaceIndex K V).Finite → IsNoetherian K V

Tactic:
intro hbfinite

Goal state after:
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ IsNoetherian K V
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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✝ : IsNoetherian R M
⊢ IsNilpotent (↥(toEnd R L M).range) M ↔ ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)

Tactic:
LieModule.isNilpotent_iff_forall (R := R)

Goal state after:
R : Type u₁
L : Type u₂
M : Type u₄
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✝ : IsNoetherian R M
⊢ (∀ (x : ↥(toEnd R L M).range), _root_.IsNilpotent ((toEnd R (↥(toEnd R L M).range) M) x)) ↔
    ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)
Module: Mathlib.Algebra.Lie.Nilpotent

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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝¹ : LieModule R L₂ M₂
hf_surj : Surjective ⇑f
hg_surj : Surjective ⇑g
inst✝ : LieModule.IsNilpotent L M
⊢ LieModule.IsNilpotent L₂ M₂

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M
  rw [isNilpotent_iff R]
  use k
  rw [← LieSubmodule.toSubmodule_inj] at hk ⊢
  simp [← hf_surj.lieModule_lcs_map_eq hfg hg_surj k, hk]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ IsNilpotent (A ⊗[R] L) (A ⊗[R] M)

Tactic:
rw [isNilpotent_iff A]

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ ∃ k, lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = ⊥
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
⊢ restrictNormalHom K = MonoidHom.id Gal(K/F)

Tactic:
ext f x
  dsimp only [restrictNormalHom, MonoidHom.mk'_apply, MonoidHom.id_apply]
  apply (algebraMap K K).injective
  rw [AlgEquiv.restrictNormal_commutes]
  simp only [Algebra.algebraMap_self, RingHom.id_apply]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
⊢ ⊤.FG

Tactic:
by
  rwa [fg_top_iff]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ Function.Bijective ⇑(Minpoly.toAdjoin F x)

Tactic:
by
    refine ⟨(injective_iff_map_eq_zero _).2 fun P₁ hP₁ ↦ ?_, Minpoly.toAdjoin.surjective F x⟩
    obtain ⟨P, rfl⟩ := mk_surjective P₁
    refine AdjoinRoot.mk_eq_zero.mpr (minpoly.dvd F x ?_)
    simpa [← Subalgebra.coe_eq_zero, ← aeval_def] using hP₁

Goal state after: