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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
⊢ ∃ yc ∈ H, ∃ yl ∈ lieSpan R L (range b.f), ∃ yu ∈ lieSpan R L (range b.e), yc + yl + yu = ⁅v, z⁆

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible f.factor

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
a : α
s : List α
x✝ : { v // ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst }
v : ToType ⟦s⟧ ≃ (map f ⟦s⟧).ToType
hv : ∀ (a : ToType ⟦s⟧), (v a).fst = f a.fst
x : ToType ⟦a :: s⟧
⊢ ((((consEquiv.trans v.optionCongr).trans consEquiv.symm).trans (cast ⋯).symm) x).fst = f x.fst

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
⊢ f.factor ∣ f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
⊢ ∀ (s : Finset (LieIdeal R L)), ↑s ⊆ {I | IsAtom I} → ∀ I ≤ s.sup id, ∃ t ⊆ s, I = t.sup id

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f g : K[X]
⊢ IsCoprime f g ↔
    ∀ {A : Type v} [inst : CommRing A] [IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
⊢ (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
⊢ f.removeFactor.natDegree = f.natDegree - 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
n : ℕ
hfn : f.natDegree = n + 1
⊢ f.removeFactor.natDegree = n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
⊢ HasTrivialRadical R L

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ (map (algebraMap K (SplittingFieldAux n.succ f)) f).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
⊢ IsSemisimple R L

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
h : IsLieAbelian L
⊢ Subsingleton L

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
⊢ IsLieAbelian ↥(radical R L)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
⊢ f.natDegree ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
⊢ IsLieAbelian ↥(radical R L) ↔ ∀ (I : LieIdeal R L), IsSolvable ↥I → IsLieAbelian ↥I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
⊢ (ad R L).ker = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
⊢ f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
⊢ Algebra.adjoin K (f.rootSet (SplittingFieldAux n.succ f)) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f✝ f : K[X]
x : SplittingFieldAux f.natDegree f
⊢ (MvPolynomial.aeval id) (MvPolynomial.X x) = x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : f.SplittingField ≃ₐ[K] SplittingFieldAux f.natDegree f := algEquivSplittingFieldAux f
⊢ e.symm (e 0)⁻¹ = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : f.SplittingField ≃ₐ[K] SplittingFieldAux f.natDegree f := algEquivSplittingFieldAux f
a : f.SplittingField
ha : a ≠ 0
⊢ e (a * e.symm (e a)⁻¹) = e 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ≥0
x : f.SplittingField
p : MvPolynomial (SplittingFieldAux f.natDegree f) K
⊢ (fun x ↦ q • x) p = (fun x1 x2 ↦ x1 * x2) ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K)) ↑q) p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
q : ℚ
x : f.SplittingField
p : MvPolynomial (SplittingFieldAux f.natDegree f) K
⊢ (fun x ↦ q • x) p = (fun x1 x2 ↦ x1 * x2) ((algebraMap K (MvPolynomial (SplittingFieldAux f.natDegree f) K)) ↑q) p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')
B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f
i : ι
hi : B i i ≠ 0
⊢ i ∈ Set.range ⇑snf.f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')
B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f
aux : ∀ (i : ι), B i i ≠ 0 → i ∈ Set.range ⇑snf.f
⊢ ∀ x ∈ Finset.univ, B x x ≠ 0 → x ∈ Set.range ⇑snf.f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
⊢ (trace R ↥p) (f.restrict hf') = (trace R M) f

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝² : Field k
K : Type ?u.6
inst✝¹ : Field K
inst✝ : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i ↑f).Splits
⊢ (map i ↑f).roots.toEnumFinset.card = (↑f).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
hf : f ∈ s
⊢ (∏ x ∈ s, map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑x).Splits

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (toSplittingField s) ((subProdXSubC f).coeff n) = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
⊢ spanCoeffs k ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ≥0
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
⊢ (fun x ↦ q • x) p = (fun x1 x2 ↦ x1 * x2) ((algebraMap k (MvPolynomial (Vars k) k)) ↑q) p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ
x : AlgebraicClosure k
p : MvPolynomial (Vars k) k
⊢ (fun x ↦ q • x) p = (fun x1 x2 ↦ x1 * x2) ((algebraMap k (MvPolynomial (Vars k) k)) ↑q) p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : AddCommMonoid M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid N₁
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Algebra R A
inst✝⁹ : Module R M₁
inst✝⁸ : Module A M₁
inst✝⁷ : Module R N₁
inst✝⁶ : Module A N₁
inst✝⁵ : SMulCommClass R A M₁
inst✝⁴ : IsScalarTower R A M₁
inst✝³ : SMulCommClass R A N₁
inst✝² : IsScalarTower R A N₁
inst✝¹ : Module R M₂
inst✝ : Module R N₂
B₁ : BilinMap A M₁ N₁
B₂ : BilinMap R M₂ N₂
hB₁ : ∀ (x y : M₁), (B₁ x) y = (B₁ y) x
hB₂ : ∀ (x y : M₂), (B₂ x) y = (B₂ y) x
x y : M₁ ⊗[R] M₂
⊢ ((B₁.tmul B₂) x) y = ((B₁.tmul B₂) y) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ IsSymm (B₁.tmul B₂)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : Monics k
⊢ map (algebraMap k (AlgebraicClosure k)) ↑f = ∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : AddCommMonoid M₂
inst✝¹ : Algebra R A
inst✝ : Module R M₂
⊢ BilinForm.baseChange A 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M₂
inst✝² : Algebra R A
inst✝¹ : Module R M₂
inst✝ : FaithfulSMul R A
B : BilinForm R M₂
h : B = 0
⊢ BilinForm.baseChange A B = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M₂
inst✝² : Algebra R A
inst✝¹ : Module R M₂
inst✝ : FaithfulSMul R A
B : BilinForm R M₂
⊢ BilinForm.baseChange A B = 0 ↔ B = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module.Free R M₁
inst✝² : Module.Finite R M₁
inst✝¹ : Module.Free R M₂
inst✝ : Module.Finite R M₂
⊢ ↑(tensorDistribEquiv R) = tensorDistrib R R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsKilling R L
⊢ LinearMap.ker (killingForm R L) = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsKilling R L
⊢ (killingForm R L).Nondegenerate

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : IsKilling R L
inst✝⁴ : Module.Free R L
inst✝³ : Module.Finite R L
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
I : LieIdeal R L
inst✝ : IsLieAbelian ↥I
⊢ I = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : LieAlgebra K L
inst✝² : IsKilling R L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
⊢ IsSemisimple K L

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : IsKilling R L
inst✝³ : Module.Free R L
inst✝² : Module.Finite R L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
h : center R L = ⊤
⊢ ⊤ = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : IsKilling R L
inst✝³ : Module.Free R L
inst✝² : Module.Finite R L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ IsLieAbelian L ↔ Subsingleton L

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L' : Type u_4
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x y : L
⊢ ((killingForm R L') (e x)) (e y) = ((killingForm R L) x) y

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
z : AlgebraicClosure k
⊢ IsIntegral k z

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ (∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0) ↔ x' ∈ ⊥

Tactic:
refine ⟨fun hx' ↦ ?_, fun hx y _ ↦ hx ▸ LinearMap.map_zero₂ (killingForm R L') y⟩

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
⊢ x' ∈ ⊥
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : k[X]
hf : f.Monic
x✝ : Irreducible f
⊢ (map (algebraMap k (AlgebraicClosure k)) f).Splits

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
this : e.symm x' ∈ LinearMap.ker (killingForm R L)
⊢ x' ∈ ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
⊢ (killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule = killingForm R ↥(ad R L).range

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
hD : D ∈ ((killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule).carrier
⊢ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule =
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (ad R L).idealRange)).toSubmodule

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
y : L
⊢ ∀ (y' : L'), ((killingForm R L') x') y' = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ {x : L} {m : LieDerivation R L L},
    m ∈ ((killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule).carrier →
      ⁅x, m⁆ ∈ ((killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule).carrier

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
⊢ IsKilling R L'

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
⊢ IsCompl I (killingCompl K L I)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : Field R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : IsLieAbelian ↥(I ⊓ killingCompl K L I)
⊢ Disjoint I (killingCompl K L I)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ ↑(ad R L).range.toSubmodule

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : Field R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Module.Finite R L
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ Submodule.map (ad R L).range.subtype (LinearMap.ker (killingForm R ↥(ad R L).range))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : x = 0
⊢ (ad R L) x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
⊢ (ad R L) x = 0 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ LieAlgebra.center R L = ⊥

Tactic:
by

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : LieRing L
inst✝² : LieAlgebra K L
inst✝¹ : IsKilling K L
inst✝ : Module.Finite K L
I : LieIdeal K L
this : ∀ (x y z : L), x ∈ killingCompl K L I → y ∈ I → ((LieModule.traceForm K L L) ⁅x, y⁆) z = 0
⊢ IsLieAbelian ↥(I ⊓ killingCompl K L I)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ ((killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule).Nondegenerate

Tactic:
by

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ (ad R L).range = ⊤

Tactic:
by

Goal state after: