mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
⊢ N + 1 + (N + 1) ≤ 2 * N + 1 + 1

Tactic:
by

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
I : Ideal R
f : R[X]
⊢ Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f}) = span {(Ideal.Quotient.mk (Ideal.map C I)) f}

Tactic:
by

Goal state after:
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
this : ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
⊢ (f - (algebraMap R (End R M)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

Tactic:
by

Goal state after:
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)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

Tactic:
by

Goal state after:
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
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
⊢ Module.Finite R ↥q → IsSemisimple ((LinearMap.restrict f hp).restrict hq₁)

Tactic:
hq₂

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
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
hq₁ : q ∈ invtSubmodule (LinearMap.restrict f hp)
hq₂ : Module.Finite R ↥q
⊢ IsSemisimple ((LinearMap.restrict f hp).restrict hq₁)
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
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
⊢ IsFinitelySemisimple (LinearMap.restrict f hp)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
ht : t ≠ 0
⊢ (t • f).IsSemisimple ↔ f.IsSemisimple

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
t : K
h : f.IsSemisimple
⊢ (t • f).IsSemisimple

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : (aeval f) p = 0
⊢ f.IsSemisimple

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotAdjoinRootEquivQuotPolynomialQuot I f).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ IsRadical (minpoly K f)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
a : K[X]
h : a ∈ Ideal.span {minpoly K f}
⊢ (aeval f) a = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
⊢ (aeval ((aeval f) p)) (minpoly K ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
a : End K M
ha : a ∈ K[f]
⊢ a.IsSemisimple

Tactic:
by

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
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
⊢ (quotAdjoinRootEquivQuotPolynomialQuot I f) ((algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x) =
    (algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
I : Ideal R
⊢ (quotEquivQuotMap f I) ((Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)) =
    (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
I : Ideal R
⊢ (quotEquivQuotMap f I).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: 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
⊢ IsReduced S

Tactic:
by

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
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
⊢ q ∣ Polynomial.map (↑includeRight) p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
⊢ LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)

Tactic:
by

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
h : (fun D ↦ D.toFun) D1 = (fun D ↦ D.toFun) D2
⊢ D1 = D2

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
⊢ D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆

Tactic:
by

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
D1 D2 : LieDerivation R L M
s : Set L
h : Set.EqOn (⇑D1) (⇑D2) s
⊢ Set.EqOn ⇑D1 ⇑D2 ↑(LieSubalgebra.lieSpan R L s)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ (⇑D)^[n] ⁅a, b⁆ = ∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D)^[i] a, (⇑D)^[n - i] b⁆

Tactic:
by

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✝ a b : L
⊢ 0 ⁅a, b⁆ = ⁅a, 0 b⁆ - ⁅b, 0 a⁆

Tactic:
by

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

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
D : LieDerivation R L M
a b : L
⊢ (-↑D) ⁅a, b⁆ = ⁅a, (-↑D) b⁆ - ⁅b, (-↑D) a⁆

Tactic:
by

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

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
S : Type u_4
T : Type u_5
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulBracketCommClass S L M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulBracketCommClass T L M
r : S
D : LieDerivation R L M
a b : L
⊢ (r • ↑D) ⁅a, b⁆ = ⁅a, (r • ↑D) b⁆ - ⁅b, (r • ↑D) a⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 : LieDerivation R L L
a b : L
⊢ ⁅↑D1, ↑D2⁆ ⁅a, b⁆ = ⁅a, ⁅↑D1, ↑D2⁆ b⁆ - ⁅b, ⁅↑D1, ↑D2⁆ a⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
⊢ (↑i !)⁻¹ • (a ^ j * b ^ (i - j) * ↑(i.choose j)) = ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 d : LieDerivation R L L
⊢ ⁅d, d⁆ = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 d e f : LieDerivation R L L
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 : LieDerivation R L L
r : R
d e : LieDerivation R L L
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (x y : LieDerivation R L L), ↑(x + y) = ↑x + ↑y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (m : R) (x : LieDerivation R L L), ↑(m • x) = (RingHom.id R) m • ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ {x y : LieDerivation R L L}, ↑⁅x, y⁆ = ⁅↑x, ↑y⁆

Tactic:
by

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
m : M
⊢ ∀ (a b : L),
    ((↑(LieModule.toEnd R L M)).flip m) ⁅a, b⁆ =
      ⁅a, ((↑(LieModule.toEnd R L M)).flip m) b⁆ - ⁅b, ((↑(LieModule.toEnd R L M)).flip m) a⁆

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ ↑(j ! * (i - j)!) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: 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]
k : K
⊢ Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) (C k)))
    g

Tactic:
by

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
m n : M
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (m + n);
    { toLinearMap := __spread.0, leibniz' := ⋯ }) =
    (let __spread.0 := (↑(LieModule.toEnd R L M)).flip m;
      { toLinearMap := __spread.0, leibniz' := ⋯ }) +
      let __spread.0 := (↑(LieModule.toEnd R L M)).flip n;
      { toLinearMap := __spread.0, leibniz' := ⋯ }

Tactic:
by

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
t : R
m : M
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (t • m);
    { toLinearMap := __spread.0, leibniz' := ⋯ }) =
    (RingHom.id R) t •
      let __spread.0 := (↑(LieModule.toEnd R L M)).flip m;
      { toLinearMap := __spread.0, leibniz' := ⋯ }

Tactic:
by

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
x y : L
D : LieDerivation R L M
⊢ (inner R L M) (D (x + y)) = (inner R L M) (D x) + (inner R L M) (D y)

Tactic:
by

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
x : L
D₁ D₂ : LieDerivation R L M
⊢ (inner R L M) ((D₁ + D₂) x) = (inner R L M) (D₁ x) + (inner R L M) (D₂ x)

Tactic:
by

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
x y : L
D : LieDerivation R L M
⊢ (inner R L M) (((inner R L M) (D y)) x) = (inner R L M) (D ⁅x, y⁆) + (inner R L M) (((inner R L M) (D x)) y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

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

Tactic:
by

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
x : L
D : LieDerivation R L M
⊢ ⁅x, ↑D⁆ = ↑⁅x, D⁆

Tactic:
by

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
t : R
x : L
D : LieDerivation R L M
⊢ ⁅t • x, D⁆ = t • ⁅x, D⁆

Tactic:
by

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
t : R
x : L
D : LieDerivation R L M
⊢ ⁅x, t • D⁆ = t • ⁅x, D⁆

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: 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]
n : ℕ
k : K
⊢ Commute
      ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) (C k * X ^ n)))
      g →
    Commute
      ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) (C k * X ^ (n + 1))))
      g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D₁ D₂ : LieDerivation R L L
⊢ ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent ↑D
⊢ ∀ {x y : L}, (IsNilpotent.exp ↑D).toFun ⁅x, y⁆ = ⁅(IsNilpotent.exp ↑D).toFun x, (IsNilpotent.exp ↑D).toFun y⁆

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent ↑D
x : L
⊢ (fun x ↦ (IsNilpotent.exp (-↑D)) x) ((IsNilpotent.exp ↑D).toFun x) = x

Tactic:
by

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
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
⊢ T ⊗[R] AdjoinRoot p ≃ₐ[T] AdjoinRoot q

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent ↑D
x : L
⊢ (IsNilpotent.exp ↑D).toFun ((fun x ↦ (IsNilpotent.exp (-↑D)) x) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_6
S : Type u_7
T : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ (tensorAlgEquiv p q h) (1 ⊗ₜ[R] root p) = root q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_6
S : Type u_7
T : Type u_8
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
x : S
⊢ (tensorAlgEquiv p q h) (1 ⊗ₜ[R] (of p) x) = (of q) (1 ⊗ₜ[R] x)

Tactic:
by

Goal state after: