mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (aeval ⟨x, ⋯⟩) (minpoly R x) = 0

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (aeval ⟨x, ⋯⟩) (minpoly R x) = 0
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
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
x✝ : AdjoinRoot g
x : R[X]
⊢ (pb.lift (root g) h₁) ((aeval pb.gen) x) = (mk g) x

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
x✝ : AdjoinRoot g
x : R[X]
⊢ (pb.lift (root g) h₁) ((aeval pb.gen) x) = (mk g) x
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:
;

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.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
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun i ↦ (f ^ i) x
x✝ : M
⊢ x✝ ∈ {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1} ↔ x✝ ∈ g '' Iic k

Tactic:
;

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
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun i ↦ (f ^ i) x
x✝ : M
⊢ x✝ ∈ {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1} ↔ x✝ ∈ g '' Iic k
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
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
hp₁ : p ∈ f.invtSubmodule
g : ℕ → M := fun i ↦ (f ^ i) x
hg : {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1} = g '' Iic k
⊢ Module.Finite R ↥p

Tactic:
exact Module.Finite.span_of_finite _ <| hg ▸ toFinite (g '' Iic k)

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

Tactic:
let e : q ≃ₗ[R] q.map p.subtype := p.equivSubtypeMap q

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
this : Submodule.map p.subtype q ∈ f.invtSubmodule
e : ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q) := p.equivSubtypeMap q
⊢ IsSemisimple ((LinearMap.restrict f hp).restrict hq₁)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotMapOfEquivQuotMapCMapMk I f).symm
      ((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
        ((quotEquivOfEq ⋯).symm
          ((Polynomial.quotQuotEquivComm I f).symm.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:
RingEquiv.symm_symm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotMapOfEquivQuotMapCMapMk I f).symm
      ((quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
        ((quotEquivOfEq ⋯).symm
          ((Polynomial.quotQuotEquivComm I f)
            ((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)
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case inr
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
this :
  ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : End K M}
    (t : K), f.IsSemisimple → t ≠ 0 → (t • f).IsSemisimple
ht : ¬t ≠ 0
⊢ (t • f).IsSemisimple

pp: M✝ : Type u_2
inst✝⁵ : AddCommGroup M✝
K✝ : Type u_3
inst✝⁴ : Field K✝
inst✝³ : Module K✝ M✝
f✝ : End K✝ M✝
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
ht : t ≠ 0
⊢ (t • f).IsSemisimple

Tactic:
;

Goal state after:
case inr
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
this :
  ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : End K M}
    (t : K), f.IsSemisimple → t ≠ 0 → (t • f).IsSemisimple
ht : ¬t ≠ 0
⊢ (t • f).IsSemisimple

M✝ : Type u_2
inst✝⁵ : AddCommGroup M✝
K✝ : Type u_3
inst✝⁴ : Field K✝
inst✝³ : Module K✝ M✝
f✝ : End K✝ M✝
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
ht : t ≠ 0
⊢ (t • f).IsSemisimple
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
⊢ (annihilator K[X] (AEval' f)).IsRadical

Tactic:
;

Goal state after:
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
⊢ (annihilator K[X] (AEval' f)).IsRadical
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 ∈ (aeval f).range
⊢ a.IsSemisimple

Tactic:
;

Goal state after:
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 ∈ (aeval f).range
⊢ a.IsSemisimple
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]
⊢ ((aeval f).toRingHom p).IsSemisimple

Tactic:
;

Goal state after:
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]
⊢ ((aeval f).toRingHom p).IsSemisimple
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:
AdjoinRoot.quotEquivQuotMap_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
I : Ideal R
⊢ (quotAdjoinRootEquivQuotPolynomialQuot I f) ((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)
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case mk
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
D2 : LieDerivation R L M
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h : (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ } = (fun D ↦ D.toFun) D2
⊢ { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ } = D2

Tactic:
;

Goal state after:
case mk
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
D2 : LieDerivation R L M
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h : (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ } = (fun D ↦ D.toFun) D2
⊢ { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ } = D2
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case mk.mk
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
toLinearMap✝¹ : L →ₗ[R] M
leibniz'✝¹ : ∀ (a b : L), toLinearMap✝¹ ⁅a, b⁆ = ⁅a, toLinearMap✝¹ b⁆ - ⁅b, toLinearMap✝¹ a⁆
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
⊢ { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } = { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }

Tactic:
;

Goal state after:
case mk.mk
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
toLinearMap✝¹ : L →ₗ[R] M
leibniz'✝¹ : ∀ (a b : L), toLinearMap✝¹ ⁅a, b⁆ = ⁅a, toLinearMap✝¹ b⁆ - ⁅b, toLinearMap✝¹ a⁆
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
⊢ { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } = { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case mk.mk
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
toLinearMap✝¹ : L →ₗ[R] M
leibniz'✝¹ : ∀ (a b : L), toLinearMap✝¹ ⁅a, b⁆ = ⁅a, toLinearMap✝¹ b⁆ - ⁅b, toLinearMap✝¹ a⁆
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝

Tactic:
;

Goal state after:
case mk.mk
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
toLinearMap✝¹ : L →ₗ[R] M
leibniz'✝¹ : ∀ (a b : L), toLinearMap✝¹ ⁅a, b⁆ = ⁅a, toLinearMap✝¹ b⁆ - ⁅b, toLinearMap✝¹ a⁆
toLinearMap✝ : L →ₗ[R] M
leibniz'✝ : ∀ (a b : L), toLinearMap✝ ⁅a, b⁆ = ⁅a, toLinearMap✝ b⁆ - ⁅b, toLinearMap✝ a⁆
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, leibniz' := leibniz'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case refine_1
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 : K[X]
⊢ a ∈ RingHom.ker (aeval f) → (aeval f) a = 0

Tactic:
;

Goal state after:
case refine_1
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 : K[X]
⊢ a ∈ RingHom.ker (aeval f) → (aeval f) a = 0
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
a : L
⊢ ⁅d + e, f⁆ a = (⁅d, f⁆ + ⁅e, f⁆) a

Tactic:
;

Goal state after:
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
a : L
⊢ ⁅d + e, f⁆ a = (⁅d, f⁆ + ⁅e, f⁆) a
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
a : L
⊢ d (f a) + e (f a) - (f (d a) + f (e a)) = d (f a) - f (d a) + (e (f a) - f (e a))

Tactic:
;

Goal state after:
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
a : L
⊢ d (f a) + e (f a) - (f (d a) + f (e a)) = d (f a) - f (d a) + (e (f a) - f (e a))
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
a : L
⊢ ⁅d, e + f⁆ a = (⁅d, e⁆ + ⁅d, f⁆) a

Tactic:
;

Goal state after:
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
a : L
⊢ ⁅d, e + f⁆ a = (⁅d, e⁆ + ⁅d, f⁆) a
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
a : L
⊢ d (e a) + d (f a) - (e (d a) + f (d a)) = d (e a) - e (d a) + (d (f a) - f (d a))

Tactic:
;

Goal state after:
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
a : L
⊢ d (e a) + d (f a) - (e (d a) + f (d a)) = d (e a) - e (d a) + (d (f a) - f (d a))
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
a : L
⊢ ⁅d, d⁆ a = 0 a

Tactic:
;

Goal state after:
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
a : L
⊢ ⁅d, d⁆ a = 0 a
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
a : L
⊢ d (d a) - d (d a) = 0

Tactic:
;

Goal state after:
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
a : L
⊢ d (d a) - d (d a) = 0
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
a : L
⊢ ⁅d, ⁅e, f⁆⁆ a = (⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆) a

Tactic:
;

Goal state after:
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
a : L
⊢ ⁅d, ⁅e, f⁆⁆ a = (⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆) a
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
a : L
⊢ d (e (f a)) - d (f (e a)) - (e (f (d a)) - f (e (d a))) =
    d (e (f a)) - e (d (f a)) - (f (d (e a)) - f (e (d a))) + (e (d (f a)) - e (f (d a)) - (d (f (e a)) - f (d (e a))))

Tactic:
;

Goal state after:
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
a : L
⊢ d (e (f a)) - d (f (e a)) - (e (f (d a)) - f (e (d a))) =
    d (e (f a)) - e (d (f a)) - (f (d (e a)) - f (e (d a))) + (e (d (f a)) - e (f (d a)) - (d (f (e a)) - f (d (e a))))
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
a : L
⊢ ⁅d, r • e⁆ a = (r • ⁅d, e⁆) a

Tactic:
;

Goal state after:
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
a : L
⊢ ⁅d, r • e⁆ a = (r • ⁅d, e⁆) a
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
⊢ ↑(D1 + D2) = ↑D1 + ↑D2

Tactic:
;

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 : LieDerivation R L L
⊢ ↑(D1 + D2) = ↑D1 + ↑D2
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 : R
D2 : LieDerivation R L L
⊢ ↑(D1 • D2) = (RingHom.id R) D1 • ↑D2

Tactic:
;

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 : R
D2 : LieDerivation R L L
⊢ ↑(D1 • D2) = (RingHom.id R) D1 • ↑D2
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:
;

Goal state after:
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
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
⊢ ↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆

Tactic:
;

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 : LieDerivation R L L
⊢ ↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆
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
a✝ : L
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (m + n);
      { toLinearMap := __spread.0, leibniz' := ⋯ })
      a✝ =
    ((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' := ⋯ })
      a✝

Tactic:
;

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

Tactic:
;

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

Tactic:
;

Goal state after:
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✝ : L
⊢ ⁅x, ↑D⁆ x✝ = ↑⁅x, D⁆ x✝