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
K : LieSubalgebra R L
⊢ K = ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
rw [_root_.eq_bot_iff]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K ≤ ⊥ ↔ ∀ x ∈ K, x = 0
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mpr
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'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
x y : L'
z : L
hz : f z = y
w : L
hw : ⁅x, f z⁆ = f w
⊢ ∃ y_1, f y_1 = ⁅x, y⁆

Tactic:
use w

Goal state after:
case h
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'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
x y : L'
z : L
hz : f z = y
w : L
hw : ⁅x, f z⁆ = f w
⊢ f w = ⁅x, y⁆
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case h
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'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
x y : L'
z : L
hz : f z = y
w : L
hw : ⁅x, f z⁆ = f w
⊢ f w = ⁅x, y⁆

Tactic:
← hw,

Goal state after:
case h
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'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
x y : L'
z : L
hz : f z = y
w : L
hw : ⁅x, f z⁆ = f w
⊢ ⁅x, f z⁆ = ⁅x, y⁆
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N✝ N'✝ N N' : LieSubmodule R L M
⊢ ∀ {x : L} {m : M}, m ∈ (↑N ⊔ ↑N').carrier → ⁅x, m⁆ ∈ (↑N ⊔ ↑N').carrier

Tactic:
rintro x m (hm : m ∈ (N : Submodule R M) ⊔ (N' : Submodule R M))

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'✝ N N' : LieSubmodule R L M
x : L
m : M
hm : m ∈ ↑N ⊔ ↑N'
⊢ ⁅x, m⁆ ∈ (↑N ⊔ ↑N').carrier
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 J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N_1 → m ∈ N_1
⊢ m ∈ ⁅J, N'⁆

Tactic:
rw [lieIdeal_oper_eq_span, mem_lieSpan]

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 J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N_1 → m ∈ N_1
⊢ ∀ (N : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N → m ∈ N
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
x : M
⊢ x ∈ lieSpan R L s ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

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

Goal state after:
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
inst✝ : LieModule R L M
⊢ IsFaithful R L M ↔ LieModule.ker R L M = ⊥

Tactic:
rw [isFaithful_iff', LieSubmodule.ext_iff]

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
inst✝ : LieModule R L M
⊢ (∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0) ↔ ∀ (m : L), m ∈ LieModule.ker R L M ↔ m ∈ ⊥
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
hsup

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
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : lieSpan R L {m} ≤ sSup s
⊢ ∃ x ∈ s, lieSpan R L {m} ≤ x
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
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : (Polynomial.aeval x) (X + C ((minpoly A x).coeff 0)) = 0
⊢ x ∈ (algebraMap A B).range

Tactic:
aeval_add,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : (Polynomial.aeval x) X + (Polynomial.aeval x) (C ((minpoly A x).coeff 0)) = 0
⊢ x ∈ (algebraMap A B).range
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
⊢ ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆

Tactic:
by
  have h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆ := by
    rw [sup_le_iff]; constructor <;>
    apply mono_lie_left <;> [exact le_sup_left; exact le_sup_right]
  suffices ⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆ by exact le_antisymm this h
  rw [lieIdeal_oper_eq_span, lieSpan_le]
  rintro m ⟨⟨x, hx⟩, n, h⟩
  simp only [SetLike.mem_coe]
  rw [LieSubmodule.mem_sup] at hx ⊢
  rcases hx with ⟨x₁, hx₁, x₂, hx₂, hx'⟩
  use ⁅((⟨x₁, hx₁⟩ : I) : L), (n : N)⁆; constructor; · apply lie_coe_mem_lie
  use ⁅((⟨x₂, hx₂⟩ : J) : L), (n : N)⁆; constructor; · apply lie_coe_mem_lie
  simp [← h, ← hx']

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 a✝ b✝ : ↥R[x]
ha✝ : a✝ ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
hb✝ : b✝ ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x) a = ↑a✝
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x) b = ↑b✝
⊢ (aeval x) (a + b) = ↑(a✝ + b✝)

Tactic:
simp [ha', hb']

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

Goal state before:
pp: case mp.smul
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y a b : ↥R[x]
hb✝ : b ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x) b' = ↑b
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a • b)

Tactic:
have ⟨p, hp⟩ := adjoin_eq_exists_aeval R x a

Goal state after:
case mp.smul
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y a b : ↥R[x]
hb✝ : b ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
b' : R[X]
hb : ∀ (i : ℕ), b'.coeff i ∈ I
hb' : (aeval x) b' = ↑b
p : R[X]
hp : (aeval x) p = ↑a
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑(a • b)
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ norm R = MonoidHom.id R

Tactic:
ext
  simp [norm_apply]

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ root (X ^ 1 - C 0) = 0

Tactic:
pow_one,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ root (X - C 0) = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
⊢ IsUnit y

Tactic:
rcases h.isUnit_or_isUnit hz with (hu | hu)

Goal state after:
case inl
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit y
⊢ IsUnit y

case inr
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit (y * z)
⊢ IsUnit y
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✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ LinearMap.det f = 1

Tactic:
← f.det_toMatrix b

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ ((toMatrix b b) f).det = 1
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →* S
x : R
⊢ f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x)

Tactic:
apply_fun (frobeniusEquiv S p)
  simp [← MonoidHom.map_frobenius]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
⊢ g.natDegree < N.succ

Tactic:
rw [← mul_one g.natDegree, ← hg1]

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
⊢ g.natDegree * 1 < g.natDegree * p
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p ^ 1 - C y).roots = p ^ 1 • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}

Tactic:
pow_one,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p - C y).roots = p • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
H : ((X ^ p ^ 1 - C y) ^ m).roots = (m * p ^ 1) • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}

Tactic:
pow_one,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
H : ((X ^ p - C y) ^ m).roots = (m * p) • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f g : S[X]
hfg : f = g
⊢ (algEquivOfEq R f g hfg) (root f) = root g

Tactic:
rw [coe_algEquivOfEq, algHomOfDvd_root]

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 ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ (b.map f).det v = b.det (⇑f.symm ∘ v)

Tactic:
rw [det_apply, toMatrix_map, det_apply]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
⊢ (aeval (root f)) q = 0 → (f * C f.leadingCoeff⁻¹).degree ≤ q.degree

Tactic:
q_aeval

Goal state after:
case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
⊢ (f * C f.leadingCoeff⁻¹).degree ≤ q.degree
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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ (aeval f) X = 0

Tactic:
rw [← aeval_X_pow (R := R) f] at h0

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : (aeval f) (X ^ n) = 0
⊢ (aeval f) X = 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
μ : R
⊢ (f - (algebraMap R (End R M)) μ).IsSemisimple ↔ f.IsSemisimple

Tactic:
by
  suffices ∀ p : Submodule R M, p ≤ p.comap (f - algebraMap R (Module.End R M) μ) ↔ p ≤ p.comap f by
    simp [mem_invtSubmodule, isSemisimple_iff, this]
  refine fun p ↦ ⟨fun h x hx ↦ ?_, fun h x hx ↦ p.sub_mem (h hx) (p.smul_mem μ hx)⟩
  simpa using p.add_mem (h hx) (p.smul_mem μ hx)

Goal state after:
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:
by
      simp only [LinearMap.sub_apply, coeFn_coe, apply_lie_eq_sub, lie_sub, sub_sub_sub_comm]

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

Goal state before:
pp: R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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 N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x y : L
t : M ⊗[R] N
⊢ (hasBracketAux (x + y)) t = (hasBracketAux x) t + (hasBracketAux y) t

Tactic:
simp only [hasBracketAux, LinearMap.lTensor_add, LinearMap.rTensor_add, map_add,
      LinearMap.add_apply]
    abel

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

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
N : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N

Tactic:
exact fun x => N.lie_mem hm

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

Goal state before:
pp: case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ (↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆ =
    ⁅(↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹), (↑f).quotKerEquivRange (Submodule.Quotient.mk z✝)⁆

Tactic:
rw [← SetLike.coe_eq_coe, LieSubalgebra.coe_bracket f.range]

Goal state after:
case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ ↑((↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆) =
    ⁅↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹)), ↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝))⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ ↑((↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆) =
    ⁅↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹)), ↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝))⁆

Tactic:
simp only [← LieSubmodule.Quotient.mk_bracket, LinearMap.quotKerEquivRange_apply_mk,
        coe_toLinearMap, map_lie]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
⊢ ∀ {x y : L ⧸ f.ker}, (↑f).quotKerEquivRange ⁅x, y⁆ = ⁅(↑f).quotKerEquivRange x, (↑f).quotKerEquivRange y⁆

Tactic:
by
      intro x y
      induction x using Submodule.Quotient.induction_on
      induction y using Submodule.Quotient.induction_on
      rw [← SetLike.coe_eq_coe, LieSubalgebra.coe_bracket f.range]
      simp only [← LieSubmodule.Quotient.mk_bracket, LinearMap.quotKerEquivRange_apply_mk,
        coe_toLinearMap, map_lie]

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:
by
  obtain ⟨k, hk⟩ := (isNilpotent_quotient_iff R L M N).mp h
  exact iInf_le_of_le k hk

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
k : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : lowerCentralSeries ℤ L M k₁ = ⊥
⊢ k₂ ∈ s

Tactic:
exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries ℤ L M h₁₂)

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

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 : ℕ
ih : ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)
⊢ ↑(lowerCentralSeries R (↥I) (↥I) (k + 1)) ≤ ↑(lowerCentralSeries R L (↥I) (k + 1))

Tactic:
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
    apply Submodule.span_mono
    rintro x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
    exact ⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩

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₃
h : Normal F E
x : ↥(toAlgHom F E K₁).range
⊢ ϕ ↑x ∈ (toAlgHom F E K₂).range

Tactic:
by
      suffices (toAlgHom F E K₁).range.map ϕ ≤ _ by exact this ⟨x, Subtype.mem x, rfl⟩
      rintro x ⟨y, ⟨z, hy⟩, hx⟩
      rw [← hx, ← hy]
      apply minpoly.mem_range_of_degree_eq_one E
      refine ((h.splits z).of_dvd (map_ne_zero (minpoly.ne_zero (h.isIntegral z)))
        (minpoly.dvd E _ (by simp [aeval_algHom_apply]))).degree_eq_one_of_irreducible
        (minpoly.irreducible ?_)
      simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
      suffices IsIntegral F _ by exact this.tower_top
      exact ((h.isIntegral z).map <| toAlgHom F E K₁).map ϕ

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ ∏ g, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)) ∣ Polynomial.map (subfield G F).subtype f

Tactic:
refine
    Fintype.prod_dvd_of_coprime
      (Polynomial.pairwise_coprime_X_sub_C <| MulAction.injective_ofQuotientStabilizer G x) fun y =>
      QuotientGroup.induction_on y fun g => ?_

Goal state after:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
y : G ⧸ stabilizer G x
g : G
⊢ Polynomial.X - Polynomial.C (ofQuotientStabilizer G x ↑g) ∣ Polynomial.map (subfield G F).subtype f
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
⊢ (∏ g, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g))).Splits

Tactic:
exact Polynomial.Splits.prod fun _ _ => Polynomial.Splits.X_sub_C _

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

Goal state before:
pp: F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
⊢ (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)

Tactic:
classical
    refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
    · rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
    rw [forall_mem_insert] at H
    rcases H with ⟨⟨H1, H2⟩, H3⟩
    obtain ⟨f⟩ := ih H3
    choose H3 _ using H3
    rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
    set Ks := Algebra.adjoin F (s : Set K)
    have : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
    let := fieldOfFiniteDimensional F Ks
    let := (f : Ks →+* L).toAlgebra
    have H5 : IsIntegral Ks a := H1.tower_top
    have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
    obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
    rw [eval_map] at hy
    exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩

Goal state after: