mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
x y : ↥L₁''
⊢ (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun ⁅x, y⁆ =
    ⁅(↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun x,
      (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun y⁆

Tactic:
apply SetCoe.ext

Goal state after:
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
x y : ↥L₁''
⊢ ↑((↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun ⁅x, y⁆) =
    ↑⁅(↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun x,
        (↑(e.toLinearEquiv.submoduleMap L₁''.toSubmodule)).toFun y⁆
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieRing L₂
inst✝¹ : LieAlgebra R L₁
inst✝ : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
x y : ↥L₁'
⊢ (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun ⁅x, y⁆ =
    ⁅(↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun x,
      (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun y⁆

Tactic:
apply SetCoe.ext

Goal state after:
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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
x y : ↥L₁'
⊢ ↑((↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun ⁅x, y⁆) =
    ↑⁅(↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun x,
        (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯)).toFun 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' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
t : R
x : L
y : ↥N
⊢ ⁅t • x, y⁆ = t • ⁅x, y⁆

Tactic:
apply SetCoe.ext

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
inst✝ : LieModule R L M
t : R
x : L
y : ↥N
⊢ ↑⁅t • x, y⁆ = ↑(t • ⁅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' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
t : R
x : L
y : ↥N
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
apply SetCoe.ext

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
inst✝ : LieModule R L M
t : R
x : L
y : ↥N
⊢ ↑⁅x, t • y⁆ = ↑(t • ⁅x, y⁆)
Module: Mathlib.Algebra.Lie.Ideal

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

Tactic:
rw [← f.ker_eq_bot, LieHom.ker] at h₁

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : map f I = ⊥
⊢ I = ⊥
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case refine_4
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
t : R
m'' : M
hx✝ : m'' ∈ Submodule.span R s
hm'' : ⁅y, m''⁆ ∈ Submodule.span R s
⊢ ⁅y, t • m''⁆ ∈ Submodule.span R s

Tactic:
rw [lie_smul]

Goal state after:
case refine_4
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
t : R
m'' : M
hx✝ : m'' ∈ Submodule.span R s
hm'' : ⁅y, m''⁆ ∈ Submodule.span R s
⊢ t • ⁅y, m''⁆ ∈ Submodule.span R s
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
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ (minpoly A x).coeff 0 = 1

Tactic:
simpa only [ndeg_eq_zero.symm] using! (monic hx).leadingCoeff

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
inst✝ : Nontrivial B
p : A[X]
hi : Irreducible p
hx : (Polynomial.aeval x) p = 0
⊢ p = p * C p.leadingCoeff⁻¹ * C p.leadingCoeff

Tactic:
mul_assoc,

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hi : Irreducible p
hx : (Polynomial.aeval x) p = 0
⊢ p = p * (C p.leadingCoeff⁻¹ * C p.leadingCoeff)
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : ↑(minpoly A x).natDegree ≤ ↑(q.natDegree * (X + C a).natDegree)
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree

Tactic:
natDegree_X_add_C,

Goal state after:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : ↑(minpoly A x).natDegree ≤ ↑(q.natDegree * 1)
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
⊢ Submodule.Quotient.mk b = Submodule.Quotient.mk ((algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩))

Tactic:
← add_zero (algebraMap _ _ _),

Goal state after:
case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
⊢ Submodule.Quotient.mk b = Submodule.Quotient.mk ((algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) + 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
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ pb.minpolyGen.degree = ↑pb.dim

Tactic:
degree_minpolyGen

Goal state after:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ ↑pb.dim = ↑pb.dim
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 R
x : S
hx : IsIntegral R x
f : R[X]
⊢ (aeval x) f ∈ Submodule.span R (Set.range fun i ↦ x ^ ↑i)

Tactic:
apply mem_span_pow'.mpr _

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ ∃ f_1, f_1.degree < ↑(minpoly R x).natDegree ∧ (aeval x) f = (aeval x) f_1
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : z * z * w ∣ 1 * (z * w)
⊢ IsUnit z

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ IsUnit z
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z * (z * w) ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0
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 : a * c * (a * c) = a * b
hc : d = a * c
⊢ d ∣ y

Tactic:
mul_assoc,

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: case pos
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
rcases h a with (h | h)

Goal state after:
case pos.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1

case pos.inr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : IsUnit a
⊢ Multiset.count a (normalizedFactors x) ≤ 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
ι : Type u_1
inst✝ : Fintype ι
f : ι → F
⊢ (∀ (x : ι), True → ∀ (y : ι), True → f x = f y → x = y) ↔ Function.Injective f

Tactic:
true_imp_iff,

Goal state after:
F : Type u
inst✝¹ : Field F
ι : Type u_1
inst✝ : Fintype ι
f : ι → F
⊢ (∀ (x y : ι), f x = f y → x = y) ↔ Function.Injective f
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.zero
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
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn

Goal state after:
case h.inr.zero
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
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = C (f.coeff 0)
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: M : Type u_1
p : ℕ
inst✝¹ : CommMonoid M
inst✝ : PerfectRing M p
n✝ n : ℕ
ih : powMulEquiv M (p ^ n) = powMulEquiv M p ^ n
⊢ powMulEquiv M (p ^ n.succ) = powMulEquiv M p ^ n.succ

Tactic:
pow_succ (powMulEquiv M p),

Goal state after:
M : Type u_1
p : ℕ
inst✝¹ : CommMonoid M
inst✝ : PerfectRing M p
n✝ n : ℕ
ih : powMulEquiv M (p ^ n) = powMulEquiv M p ^ n
⊢ powMulEquiv M (p ^ n.succ) = powMulEquiv M p ^ n * powMulEquiv M p
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case mpr
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 : f.ker ≠ ⊥
⊢ LinearMap.det f = 0

Tactic:
· let b := Module.finBasis R M
    obtain ⟨v, ⟨_, hv_ne_zero⟩⟩ := (ker f).ne_bot_iff.mp h
    rw [← det_toMatrix b, ← Matrix.exists_mulVec_eq_zero_iff]
    refine ⟨fun i => b.repr v i, by simpa, by simpa [toMatrix_mulVec_repr]⟩

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ i x ∈ (map i h).roots

Tactic:
mem_roots (show h.map i ≠ 0 from map_ne_zero h_ne_zero)

Goal state after:
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ (map i h).IsRoot (i x)
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✝
𝕜 : Type u_5
inst✝³ : Field 𝕜
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 0
⊢ IsUnit (LinearMap.det f)

Tactic:
exact isUnit_iff_ne_zero.2 hf

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 (update v i (v j))).det = 0

Tactic:
← det_transpose,

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 (update v i (v j)))ᵀ.det = 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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ f = 0

Tactic:
← aeval_X (R := R) f

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 : f ^ n = 0
⊢ (aeval f) X = 0
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

Tactic:
simp_rw [exp_eq_sum (pow_eq_zero_of_le h₀ (pow_nilpotencyClass hn)), sum_smul, smul_assoc]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂ (↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p)))))
      (1 ⊗ₜ[R] root p) q =
    0

Tactic:
simp only [← h, AlgHom.toRingHom_eq_coe]

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂ (↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p)))))
      (1 ⊗ₜ[R] root p) (Polynomial.map (↑includeRight) p) =
    0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: K : Type u_6
L : Type u_7
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
h2 : IsIntegral K (AdjoinRoot.root f)
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g

Tactic:
have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)

Goal state after:
K : Type u_6
L : Type u_7
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
h2 : IsIntegral K (AdjoinRoot.root f)
h3 : f * C f.leadingCoeff⁻¹ ∣ Polynomial.map (algebraMap K L) (minpoly K (AdjoinRoot.root f))
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p a b c d x y : R
h1 : p ∣ a * x + b * y
h2 : p ∣ c * x + d * y
⊢ p ∣ (a * d - b * c) * x

Tactic:
obtain ⟨k1, hk1⟩ := h1
  obtain ⟨k2, hk2⟩ := h2
  refine ⟨d * k1 - b * k2, ?_⟩
  grind

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

Tactic:
rw [lie_smul]

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
t : R
m : M
hm : m ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
x : L
⊢ t • ⁅x, m⁆ ∈ N
Module: Mathlib.Algebra.Lie.Normalizer

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
x y : L
⊢ ⁅x, y⁆ ∈ I ↔ ⁅y, x⁆ ∈ I

Tactic:
simp only [← lie_skew x y, neg_mem_iff]

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

Goal state before:
pp: case smul_mem
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
y : L
hy : y ∈ S
⊢ c • y ∈ Submodule.span R₂ S

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      refine Submodule.subset_span ⟨c • a, ?_, b, hb, rfl⟩
      rw [← ih] at ha ⊢
      exact Submodule.smul_mem _ _ ha

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₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂

Tactic:
by
  induction k with
  | zero => simp
  | succ k ih => simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]

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

Goal state before:
pp: case refine_2.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
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆

Tactic:
mul_assoc,

Goal state after:
case refine_2.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
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆
Module: Mathlib.Algebra.Lie.BaseChange

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
N : LieSubmodule R L M
x : A ⊗[R] L
m : A ⊗[R] M
hm : m ∈ Submodule.baseChange A ↑N
⊢ ⁅x, m⁆ ∈ Submodule.baseChange A ↑N

Tactic:
rw [Submodule.baseChange_eq_span] at hm

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
N : LieSubmodule R L M
x : A ⊗[R] L
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ⁅x, m⁆ ∈ Submodule.baseChange A ↑N
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✝ : Subsingleton L
M : Type u_1
⊢ ∀ [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : LieRingModule L M] [inst_3 : LieModule R L M],
    (∀ (x : L), IsNilpotent ((toEnd R L M) x)) → LieModule.IsNilpotent L M

Tactic:
_i1

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
⊢ ∀ [inst : Module R M] [inst_1 : LieRingModule L M] [inst_2 : LieModule R L M],
    (∀ (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₄
⊢ ∀ [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : LieRingModule L₂ M] [inst_3 : LieModule R L₂ M],
    (∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)) → LieModule.IsNilpotent L₂ M

Tactic:
_i1

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
⊢ ∀ [inst : Module R M] [inst_1 : LieRingModule L₂ M] [inst_2 : LieModule R L₂ M],
    (∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)) → LieModule.IsNilpotent L₂ M