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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
int : IsIntegral A x
⊢ 2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range

Tactic:
rw [iff_not_comm, ← natDegree_eq_one_iff, not_le]

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
int : IsIntegral A x
⊢ (minpoly A x).natDegree = 1 ↔ (minpoly A x).natDegree < 2
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : ∀ (x : ↑(range ⇑(Module.finBasis F E))), rootsOfMinPolyPiType F E K f x = rootsOfMinPolyPiType F E K g x
⊢ ↑f = ↑g

Tactic:
exact LinearMap.ext_on (Module.finBasis F E).span_eq fun e he =>
    Subtype.ext_iff.mp (h ⟨e, he⟩)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
a : R
ha : a ∈ ↑I
i : ℕ
⊢ (if i = 0 then a else 0) ∈ I

Tactic:
aesop

Goal state after:
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
x y : S
d : ℕ
n : S
⊢ (∃ y, x ^ ↑y = n) ↔ n ∈ (fun i ↦ x ^ i) '' ↑(Finset.range d)

Tactic:
Set.mem_image,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
n : S
⊢ (∃ y, x ^ ↑y = n) ↔ ∃ x_1 ∈ ↑(Finset.range d), x ^ x_1 = n
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
inst✝ : Nontrivial S
pb : PowerBasis R S
y : S
⊢ y ∈ Submodule.span R (Set.range fun i ↦ pb.gen ^ ↑i)

Tactic:
simpa using pb.basis.mem_span y

Goal state after:
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
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f g : A[X]
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f * (aeval pb.gen) g) =
    ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f) * ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) g)

Tactic:
simp only [← aeval_mul, pb.constr_pow_aeval hy]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

Tactic:
exact linearIndependent_empty_type

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
⊢ b ^ m ≠ a

Tactic:
have hn : n ≠ 0 := fun e ↦ not_irreducible_C
    (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
hn : n ≠ 0
⊢ b ^ m ≠ a
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + b * derivative p = 1
⊢ Polynomial.map f a * Polynomial.map f p + Polynomial.map f b * Polynomial.map f (derivative p) = 1

Tactic:
← Polynomial.map_mul,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + b * derivative p = 1
⊢ Polynomial.map f (a * p) + Polynomial.map f b * Polynomial.map f (derivative p) = 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + b * derivative p = 1
⊢ Polynomial.map f (a * p) + Polynomial.map f b * Polynomial.map f (derivative p) = 1

Tactic:
← Polynomial.map_mul,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + b * derivative p = 1
⊢ Polynomial.map f (a * p) + Polynomial.map f (b * derivative p) = 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
⊢ ∃ s, map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)

Tactic:
obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp

Goal state after:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h : map i f = C (map i f).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ ∃ s, map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h : map i f = C (map i f).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ map i f = C (i f.leadingCoeff) * ∏ a ∈ s.toFinset, (X - C a)

Tactic:
rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]

Goal state after:
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h : map i f = C (map i f).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ s.Nodup
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case monomial
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S[X]
n : ℕ
a : R
a✝ : (aeval (root f)) (C a * X ^ n) = (mk f) (Polynomial.map (algebraMap R S) (C a * X ^ n))
⊢ (aeval (root f)) (C a * X ^ (n + 1)) = (mk f) (Polynomial.map (algebraMap R S) (C a * X ^ (n + 1)))

Tactic:
| monomial n a _ =>

Goal state after:
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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ ((e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j)).det = 0

Tactic:
apply det_zero_of_row_eq hij

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) j
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S →ₐ[R] T
g : T →ₐ[R] U
p : S[X]
q : T[X]
r : U[X]
hf : q ∣ Polynomial.map (↑f) p
hg : r ∣ Polynomial.map (↑g) q
⊢ (mapAlgHom g q r hg).comp (mapAlgHom f p q hf) = mapAlgHom (g.comp f) p r ⋯

Tactic:
aesop

Goal state after:
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_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
i : ι
⊢ (LinearEquiv.ofIsUnitDet h) (e i) = v i

Tactic:
LinearEquiv.ofIsUnitDet_apply,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
i : ι
⊢ ((e.constr ℕ) v) (e i) = v i
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
⊢ ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i

Tactic:
rw [h₁, this, add_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case refine_2.mk
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
a✝ : R
p : K[X]
⊢ Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) p))
    g

Tactic:
exact p.induction_on (fun k ↦ by simp [R, commute_algebraMap_left])
      (fun p q hp hq ↦ by simpa [R] using! hp.add_left hq)
      fun n k ↦ by simpa [R, pow_succ, ← mul_assoc _ _ X] using! (·.mul_left comm)

Goal state after:
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
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : n₀ ∈ K[n₁ + s₁]
s₀ : End K V
hs₀ : s₀ ∈ K[n₁ + s₁]
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
hnil : IsNilpotent (s - s₀)
⊢ s = s₀

Tactic:
have hss : (s - s₀).IsSemisimple :=
    hs.sub_of_commute (commute_of_mem_adjoin_singleton_of_commute hs₀ hsf) hs₀_ss

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : n₀ ∈ K[n₁ + s₁]
s₀ : End K V
hs₀ : s₀ ∈ K[n₁ + s₁]
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
hnil : IsNilpotent (s - s₀)
hss : (s - s₀).IsSemisimple
⊢ s = s₀
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrder R
x y : R
⊢ Associated y x ↔ Associated x y

Tactic:
Associated.comm

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrder R
x y : R
⊢ Associated x y ↔ Associated x y
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
z : L
⊢ z ∈ Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ⊤, ⁅x_1, n⁆ = x} ↔ z ∈ Submodule.span R {x | ∃ x_1 y, ⁅x_1, y⁆ = x}

Tactic:
aesop

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

Goal state before:
pp: case succ
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ⇑f
k : ℕ
ih : map f (derivedSeries R L' k) = derivedSeries R L k
⊢ map f (derivedSeries R L' (k + 1)) = derivedSeries R L (k + 1)

Tactic:
simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hx : x ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}
hy : y ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}
m : M
⊢ ⁅x + y, m⁆ ∈ N

Tactic:
add_lie

Goal state after:
R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hx : x ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}
hy : y ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}
m : M
⊢ ⁅x, m⁆ + ⁅y, m⁆ ∈ N
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : IsLieAbelian ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ IsLieAbelian
    ↥(match k + 1 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Tactic:
exact h.1

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
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s = 0 ↔ I = ⊥

Tactic:
have hne : s.Nonempty :=
    have ⟨k, hk⟩ := IsSolvable.solvable R I
    ⟨k, by rwa [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk⟩

Goal state after:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
hne : s.Nonempty
⊢ sInf s = 0 ↔ I = ⊥
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case 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
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
y z : A ⊗[R] L
hy : ⁅y, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
hz : ⁅z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
⊢ ⁅y + z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N

Tactic:
add_lie

Goal state after:
case 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
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
y z : A ⊗[R] L
hy : ⁅y, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
hz : ⁅z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
⊢ ⁅y, (Finsupp.linearCombination A Subtype.val) c⁆ + ⁅z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈
    Submodule.baseChange A ↑N
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
⊢ LieAlgebra.IsEngelian R L₂

Tactic:
intro M _i1 _i2 _i3 _i4 h'

Goal state after:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
⊢ LieModule.IsNilpotent L₂ M
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this✝¹ : LieRingModule L M := ⋯
this✝ : LieModule R L M := ⋯
hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
surj_id : Surjective ⇑LinearMap.id
this : LieModule.IsNilpotent L M
⊢ ∀ (x : L) (m : M), ⁅f x, LinearMap.id m⁆ = LinearMap.id ⁅x, m⁆

Tactic:
aesop

Goal state after:
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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ lowerCentralSeries R L M k ≤ N

Tactic:
← LieSubmodule.Quotient.map_mk'_eq_bot_le,

Goal state after:
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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k) = ⊥
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
k : ℕ
⊢ lowerCentralSeries R L (M ⧸ N) k = ⊥ ↔ lowerCentralSeries R L M k ≤ N

Tactic:
← LieSubmodule.Quotient.map_mk'_eq_bot_le,

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
k : ℕ
⊢ lowerCentralSeries R L (M ⧸ N) k = ⊥ ↔ LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k) = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
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
k : ℕ
h : ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥
⊢ ⁅⊤,
      match k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k⁆ =
    ⊥

Tactic:
exact h.1

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

Goal state before:
pp: case mpr
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₂
inst✝ : LieModule R L₂ M₂
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
h : LieModule.IsNilpotent L₂ M₂
hg : Surjective ⇑↑g.symm
x : L₂
m : M₂
⊢ ⁅f.symm.toLieHom x, ↑g.symm m⁆ = ↑g.symm ⁅x, m⁆

Tactic:
rw [LinearEquiv.coe_coe, LieEquiv.coe_toLieHom, ← g.symm_apply_apply ⁅f.symm x, g.symm m⁆, ←
      hfg, f.apply_symm_apply, g.apply_symm_apply]

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
M₁ M₂ : LieSubmodule R L M
h₁ : M₁ ≤ M₂
inst✝ : IsNilpotent L ↥M₂
f : L →ₗ⁅R⁆ L := LieHom.id
g : ↥M₁ →ₗ[R] ↥M₂ := Submodule.inclusion h₁
⊢ ∀ (x : L) (m : ↥M₁), ⁅f x, g m⁆ = g ⁅x, m⁆

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
inst✝ : LieModule.IsNilpotent L ↥I
f : ↥I →ₗ⁅R⁆ L := I.incl
g : ↥I →ₗ⁅R⁆ ↥I := LieHom.id
⊢ ∀ (x m : ↥I), ⁅f x, g m⁆ = g ⁅x, m⁆

Tactic:
aesop

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 = ⊥
⊢ ∃ k, lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = ⊥

Tactic:
exact ⟨k, by simp [hk]⟩

Goal state after:
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹⁷ : Field F
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra E K₁
inst✝⁵ : Algebra E K₂
inst✝⁴ : Algebra E K₃
inst✝³ : IsScalarTower F E K₁
inst✝² : IsScalarTower F E K₂
inst✝¹ : IsScalarTower F E K₃
inst✝ : Normal F E
σ : Gal(E/F)
a✝ : E
⊢ ((fun σ ↦ σ.restrictNormal' E) ((fun σ ↦ (toAlgHom F E K₁).comp ↑σ) σ)) a✝ = σ a✝

Tactic:
simp only [AlgHom.restrictNormal', AlgEquiv.coe_ofBijective]

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹⁷ : Field F
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra E K₁
inst✝⁵ : Algebra E K₂
inst✝⁴ : Algebra E K₃
inst✝³ : IsScalarTower F E K₁
inst✝² : IsScalarTower F E K₂
inst✝¹ : IsScalarTower F E K₃
inst✝ : Normal F E
σ : Gal(E/F)
a✝ : E
⊢ (((toAlgHom F E K₁).comp ↑σ).restrictNormal E) a✝ = σ a✝
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

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

Tactic:
· intro _
    use Algebra.EssFiniteType.finset F E
    refine top_le_iff.mp fun x _ ↦ ?_
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (Algebra.EssFiniteType.submonoid F E) x
    have hs : s.1.1 ≠ 0 := (IsLocalization.map_units E s).ne_zero
    have H : IsLocalization.mk' E x s = x / s := by
      simp [IsLocalization.mk'_eq_iff_eq_mul, hs]
    rw [H]
    exact div_mem (IntermediateField.algebra_adjoin_le_adjoin _ _ x.2)
      (IntermediateField.algebra_adjoin_le_adjoin _ _ s.1.2)

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
S : Set E
⊢ restrictScalars F (adjoin (↥K) S) = K ⊔ adjoin F S

Tactic:
rw [restrictScalars_adjoin, adjoin_union, adjoin_self]

Goal state after: