mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬(X ^ p - C a).degree = 0

Tactic:
degree_X_pow_sub_C hp.pos,

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬↑p = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case mp
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : LinearMap.det f = 0
⊢ f.ker ≠ ⊥

Tactic:
exact bot_lt_iff_ne_bot.mp (bot_lt_ker_of_det_eq_zero h)

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
a✝ : Nontrivial R
⊢ ∑ b, ((monomial ↑b) (x b)).coeff ↑i = x i

pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
a✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (x i)).degree < g.degree

Tactic:
· simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
a✝ : Nontrivial R
⊢ (∑ i, (monomial ↑i) (x i)).degree < g.degree
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ (basisFun R ι).det v = (of v).det

Tactic:
rw [Pi.basisFun_det]
  rfl

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ exp a = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i

Tactic:
dsimp [exp]

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inl
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₀ : nilpotencyClass a ≤ k
⊢ exp a • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

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
⊢ exp a • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
· simp_rw [exp_eq_sum (pow_eq_zero_of_le h₀ (pow_nilpotencyClass hn)), sum_smul, 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
⊢ exp a • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
D D1✝ D2✝ : LieDerivation R L M
a✝ b✝ : L
D1 D2 : LieDerivation R L M
a b : L
⊢ (↑D1 + ↑D2) ⁅a, b⁆ = ⁅a, (↑D1 + ↑D2) b⁆ - ⁅b, (↑D1 + ↑D2) a⁆

Tactic:
simp only [LinearMap.add_apply, coeFn_coe, apply_lie_eq_sub, lie_add, add_sub_add_comm]

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
this : (ad R L) (D x) = 0
⊢ D x = 0 x

Tactic:
rw [← LieHom.mem_ker, ad_ker_eq_center, h, LieSubmodule.mem_bot] at this

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)
x : L
this : D x = 0
⊢ D x = 0 x
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: case refine_3
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)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
hss : (aeval s) P = 0
⊢ s.IsSemisimple

Tactic:
exact isSemisimple_of_squarefree_aeval_eq_zero sep.squarefree hss

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 : ℕ
⊢ IsLieAbelian ↥(D k I) ↔ D (1 + k) I = ⊥

Tactic:
derivedSeriesOfIdeal_add I 1 k,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ IsLieAbelian ↥(D k I) ↔ D 1 (D k I) = ⊥
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
k l : ℕ
I J : LieIdeal R L
hI : derivedSeriesOfIdeal R L k I = ⊥
hJ : derivedSeriesOfIdeal R L l J = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) = ⊥

Tactic:
← le_bot_iff

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k l : ℕ
I J : LieIdeal R L
hI : derivedSeriesOfIdeal R L k I = ⊥
hJ : derivedSeriesOfIdeal R L l J = ⊥
⊢ derivedSeriesOfIdeal R L (k + l) (I + J) ≤ ⊥
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L), ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y) + ((bracket' R A L L) (x ⊗ₜ[R] y)) (a₁ ⊗ₜ[R] l₁) = 0

pp: case refine_3.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x + ((bracket' R A L L) x) (a₁ ⊗ₜ[R] l₁) = 0 →
      ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y + ((bracket' R A L L) y) (a₁ ⊗ₜ[R] l₁) = 0 →
        ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y) + ((bracket' R A L L) (x + y)) (a₁ ⊗ₜ[R] l₁) = 0

Tactic:
· intro a₂ l₂
        simp only [← lie_skew l₂ l₁, mul_comm a₁ a₂, TensorProduct.tmul_neg, bracket'_tmul,
          add_neg_cancel]

Goal state after:
case refine_3.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x + ((bracket' R A L L) x) (a₁ ⊗ₜ[R] l₁) = 0 →
      ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y + ((bracket' R A L L) y) (a₁ ⊗ₜ[R] l₁) = 0 →
        ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y) + ((bracket' R A L L) (x + y)) (a₁ ⊗ₜ[R] l₁) = 0
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
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
⊢ derivedSeries R L 1 < ⊤

Tactic:
obtain ⟨n, hn⟩ := IsSolvable.solvable (R := R) (L := L)

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
⊢ derivedSeries R L 1 < ⊤
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
N : LieSubmodule R L M
k : ℕ
⊢ lowerCentralSeries R L (↥N) k = ⊥ ↔ LieSubmodule.lcs k N = ⊥

Tactic:
rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot,
    inf_eq_right.mpr (N.lcs_le_self 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
k✝ : ℕ
N : LieSubmodule R L M
M₂✝ : Type w₁
inst✝⁶ : AddCommGroup M₂✝
inst✝⁵ : Module R M₂✝
inst✝⁴ : LieRingModule L M₂✝
inst✝³ : LieModule R L M₂✝
inst✝² : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst✝¹ : IsNilpotent L ↥M₁
inst✝ : IsNilpotent L ↥M₂
k : ℕ
hk : lowerCentralSeries R L (↥M₁) k = ⊥
l : ℕ
hl : lowerCentralSeries R L (↥M₂) l = ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M),
  m ≤ n → lowerCentralSeries R L (↥N) m = ⊥ → lowerCentralSeries R L (↥N) n = ⊥ :=
  fun {m n} N le hn ↦
    Eq.mp (Eq.trans (congrArg (LE.le (lowerCentralSeries R L (↥N) n)) hn) le_bot_iff._simp_1)
      (antitone_lowerCentralSeries R L (↥N) le)
h₁ : lowerCentralSeries R L (↥M₁) (max k l) = ⊥
h₂ : lowerCentralSeries R L (↥M₂) (max k l) = ⊥
⊢ IsNilpotent L ↥(M₁ ⊔ M₂)

Tactic:
refine (isNilpotent_iff R L (M₁ + M₂)).mpr ⟨k ⊔ l, ?_⟩

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
k✝ : ℕ
N : LieSubmodule R L M
M₂✝ : Type w₁
inst✝⁶ : AddCommGroup M₂✝
inst✝⁵ : Module R M₂✝
inst✝⁴ : LieRingModule L M₂✝
inst✝³ : LieModule R L M₂✝
inst✝² : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst✝¹ : IsNilpotent L ↥M₁
inst✝ : IsNilpotent L ↥M₂
k : ℕ
hk : lowerCentralSeries R L (↥M₁) k = ⊥
l : ℕ
hl : lowerCentralSeries R L (↥M₂) l = ⊥
lcs_eq_bot : ∀ {m n : ℕ} (N : LieSubmodule R L M),
  m ≤ n → lowerCentralSeries R L (↥N) m = ⊥ → lowerCentralSeries R L (↥N) n = ⊥ :=
  fun {m n} N le hn ↦
    Eq.mp (Eq.trans (congrArg (LE.le (lowerCentralSeries R L (↥N) n)) hn) le_bot_iff._simp_1)
      (antitone_lowerCentralSeries R L (↥N) le)
h₁ : lowerCentralSeries R L (↥M₁) (max k l) = ⊥
h₂ : lowerCentralSeries R L (↥M₂) (max k l) = ⊥
⊢ lowerCentralSeries R L (↥(M₁ + M₂)) (max k l) = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
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✝ : IsNilpotent L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k

Tactic:
exact iterate_toEnd_mem_lowerCentralSeries R L M x m k

Goal state after:
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✝⁷ : 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
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
x✝ y✝ : A ⊗[R] L
z✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hz✝ : z✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝¹ : ⁅x✝, z✝⁆ ∈ Submodule.span A s
a✝ : ⁅y✝, z✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝ + y✝, z✝⁆ ∈ Submodule.span A s

Tactic:
simp [add_mem, Submodule.smul_mem, *]

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

Goal state before:
pp: case refine_2.refine_3
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
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
x✝ : A ⊗[R] L
y✝ z✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
hz✝ : z✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝¹ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
a✝ : ⁅x✝, z✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝, y✝ + z✝⁆ ∈ Submodule.span A s

Tactic:
simp [add_mem, Submodule.smul_mem, *]

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

Goal state before:
pp: case refine_2.refine_4
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
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
r✝ : A
x✝ : A ⊗[R] L
y✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
⊢ ⁅r✝ • x✝, y✝⁆ ∈ Submodule.span A s

Tactic:
simp [add_mem, Submodule.smul_mem, *]

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
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : IsNilpotent L (M ⧸ N)
⊢ ⨅ k, lowerCentralSeries R L M k ≤ N

Tactic:
obtain ⟨k, hk⟩ := (isNilpotent_quotient_iff R L M N).mp h

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
inst✝ : LieModule R L M
h : IsNilpotent L (M ⧸ N)
k : ℕ
hk : lowerCentralSeries R L M k ≤ N
⊢ ⨅ k, lowerCentralSeries R L M k ≤ N
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_5
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
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
r✝ : A
x✝ : A ⊗[R] L
y✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝, r✝ • y✝⁆ ∈ Submodule.span A s

Tactic:
simp [add_mem, Submodule.smul_mem, *]

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
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ Function.Surjective ⇑↑(toEnd R L M).rangeRestrict

Tactic:
exact LieHom.surjective_rangeRestrict (toEnd 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
inst✝ : IsNoetherian R L
⊢ IsEngelian R L

Tactic:
intro M _i1 _i2 _i3 _i4 h
  rw [← isNilpotent_range_toEnd_iff R]
  let L' := (toEnd R L M).range
  replace h : ∀ y : L', IsNilpotent (y : Module.End R M) := by
    rintro ⟨-, ⟨y, rfl⟩⟩
    simp [h]
  change LieModule.IsNilpotent L' M
  let s := {K : LieSubalgebra R L' | LieAlgebra.IsEngelian R K}
  have hs : s.Nonempty := ⟨⊥, LieAlgebra.isEngelian_of_subsingleton⟩
  suffices ⊤ ∈ s by
    rw [← isNilpotent_of_top_iff (R := R)]
    apply this M
    simp [LieSubalgebra.toEnd_eq, h]
  have : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K' := by
    rintro K (hK₁ : LieAlgebra.IsEngelian R K) hK₂
    apply LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer hK₁
    apply lt_of_le_of_ne K.le_normalizer
    rw [Ne, eq_comm, K.normalizer_eq_self_iff, ← Ne, ←
      LieSubmodule.nontrivial_iff_ne_bot R K]
    have : Nontrivial (L' ⧸ K.toLieSubmodule) := Submodule.Quotient.nontrivial_iff.2 <| by simpa
    have : LieModule.IsNilpotent K (L' ⧸ K.toLieSubmodule) := by
      refine hK₁ _ fun x => ?_
      have hx := LieAlgebra.isNilpotent_ad_of_isNilpotent (h x)
      apply Module.End.IsNilpotent.mapQ ?_ hx
      intro X HX
      simp only [LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.mem_toSubmodule] at HX
      simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply,
        LieSubalgebra.mem_toSubmodule]
      exact LieSubalgebra.lie_mem K x.prop HX
    exact nontrivial_max_triv_of_isNilpotent R K (L' ⧸ K.toLieSubmodule)
  have _i5 : IsNoetherian R L' := by
    refine isNoetherian_of_surjective (LieHom.rangeRestrict (toEnd R L M)).toLinearMap ?_
    simp only [LinearMap.range_eq_top]
    exact LieHom.surjective_rangeRestrict (toEnd R L M)
  obtain ⟨K, hK₁, hK₂⟩ := (LieSubalgebra.wellFoundedGT_of_noetherian R L').wf.has_min s hs
  obtain rfl : K = ⊤ := by grind
  exact hK₁

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

Goal state before:
pp: case h
L : Type v
inst✝ : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : LieModule.lowerCentralSeries ℤ L L k = ⊥
⊢ derivedSeries ℤ L k = ⊥

Tactic:
← le_bot_iff

Goal state after:
case h
L : Type v
inst✝ : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : LieModule.lowerCentralSeries ℤ L L k ≤ ⊥
⊢ derivedSeries ℤ L k ≤ ⊥
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (Polynomial.map (subfield G F).subtype ((prodXSubSMul G F x).toSubring (subfield G F).toSubring ⋯)).Separable

Tactic:
Polynomial.map_toSubring _ (subfield G F).toSubring

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (prodXSubSMul G F x).Separable
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ f.fieldRange = IntermediateField.adjoin F s

Tactic:
by
  apply IntermediateField.toSubfield_injective
  simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]
  refine ringHom_fieldRange_eq_of_comp_eq_of_range_eq h ?_
  rw [← Algebra.adjoin_eq_ring_closure, ← hs]; rfl

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
⊢ Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B

Tactic:
by
  obtain ⟨ιA, bA⟩ := Free.exists_basis (R := R) (M := A)
  obtain ⟨ιB, bB⟩ := Free.exists_basis (R := R) (M := B)
  have h := Algebra.adjoin_union_coe_submodule R (A : Set S) (B : Set S)
  rw [A.adjoin_eq_span_basis R bA, B.adjoin_eq_span_basis R bB, ← Algebra.sup_def,
    Submodule.span_mul_span] at h
  change Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ _
  rw [h, ← bA.mk_eq_rank'', ← bB.mk_eq_rank'']
  refine (rank_span_le _).trans Cardinal.mk_mul_le |>.trans ?_
  gcongr <;> exact Cardinal.mk_range_le

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ lift ⊤ = K

Tactic:
lift,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ map K.val ⊤ = K
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
hcomm : Commute ((aeval a) (C k - X)) ((aeval a) (-(q / (X - C k))))
⊢ ¬IsUnit ((aeval a) (C k - X) * (aeval a) (-(q / (X - C k))))

Tactic:
apply mt fun h => (hcomm.isUnit_mul_iff.mp h).1

Goal state after:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := ⋯
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
hcomm : Commute ((aeval a) (C k - X)) ((aeval a) (-(q / (X - C k))))
⊢ ¬IsUnit ((aeval a) (C k - X))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ⨆ i ∈ s, F⟮↑i⟯ ≤ adjoin F (Subtype.val '' ↑s)

Tactic:
iSup_le_iff,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∀ i ∈ s, F⟮↑i⟯ ≤ adjoin F (Subtype.val '' ↑s)