mathlib-initiative/mathlib-tactics huggingface dataset:
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
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
⊢ ∀ [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : LieRingModule (↥K') M] [inst_3 : LieModule R (↥K') M],
    (∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)) → LieModule.IsNilpotent (↥K') M

Tactic:
_i1

Goal state after:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
⊢ ∀ [inst : Module R M] [inst_1 : LieRingModule (↥K') M] [inst_2 : LieModule R (↥K') M],
    (∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)) → LieModule.IsNilpotent (↥K') M
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✝ : IsNoetherian R 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✝ : IsNoetherian R 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.FieldTheory.Finiteness

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsNoetherian K V
⊢ Set.range ⇑(Basis.ofVectorSpace K V) = Basis.ofVectorSpaceIndex K V

Tactic:
Basis.range_ofVectorSpace

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsNoetherian K V
⊢ Basis.ofVectorSpaceIndex K V = Basis.ofVectorSpaceIndex K V
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N

Tactic:
by
  rw [eq_top_iff, ← lcs_le_iff]; rfl

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ (∃ k, ucs k ⊥ = ⊤) ↔ ∃ k, N ≤ ucs k ⊥

Tactic:
← ucs_comap_incl,

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ (∃ k, comap N.incl (ucs k ⊥) = ⊤) ↔ ∃ k, N ≤ ucs k ⊥
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
inst✝⁵ : Field F
E : Type u_3
inst✝⁴ : Field E
inst✝³ : Algebra F E
M : Type u_5
N : Type u_6
inst✝² : Field N
inst✝¹ : Field M
inst✝ : Algebra M N
h : ∀ (x : E), IsIntegral F x ∧ (map (algebraMap F E) (minpoly F x)).Splits
f : F ≃+* M
g : E ≃+* N
hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)
this : Normal F E
x : N
⊢ IsIntegral M x ∧ (map (algebraMap M N) (minpoly M x)).Splits

Tactic:
rw [← g.apply_symm_apply x]

Goal state after:
F : Type u_1
inst✝⁵ : Field F
E : Type u_3
inst✝⁴ : Field E
inst✝³ : Algebra F E
M : Type u_5
N : Type u_6
inst✝² : Field N
inst✝¹ : Field M
inst✝ : Algebra M N
h : ∀ (x : E), IsIntegral F x ∧ (map (algebraMap F E) (minpoly F x)).Splits
f : F ≃+* M
g : E ≃+* N
hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)
this : Normal F E
x : N
⊢ IsIntegral M (g (g.symm x)) ∧ (map (algebraMap M N) (minpoly M (g (g.symm x)))).Splits
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
x : F
⊢ IsIntegral (↥(subfield G F)) x

Tactic:
cases nonempty_fintype G

Goal state after:
case intro
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsIntegral (↥(subfield G F)) x
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
⊢ (Polynomial.map (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x)).Splits

Tactic:
cases nonempty_fintype G

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ (Polynomial.map (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x)).Splits
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
⊢ IsSeparable (↥(subfield G F)) x

Tactic:
cases nonempty_fintype G

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsSeparable (↥(subfield G F)) x
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
⊢ FiniteDimensional (↥(subfield G F)) F

Tactic:
cases nonempty_fintype G

Goal state after:
case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
val✝ : Fintype G
⊢ FiniteDimensional (↥(subfield G F)) F
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
⊢ Function.Bijective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Tactic:
cases nonempty_fintype G

Goal state after:
case intro
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Bijective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
μ' : K
hμ' : μ' ∈ m.support
hμμ' : μ' = μ
⊢ g (m μ') = g (m μ)

Tactic:
hμμ'

Goal state after:
case pos
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
μ' : K
hμ' : μ' ∈ m.support
hμμ' : μ' = μ
⊢ g (m μ) = g (m μ)
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case e'_5
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
s : E
hs : s ∈ S
this✝ : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower L (↥L') E
e_3✝ : CommRing.toCommSemiring.toSemiring = Field.toSemifield.toDivisionSemiring.toSemiring
x✝ : L
⊢ (f'.comp (algebraMap L ↥L')) x✝ = f.toRingHom x✝

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
    AlgHom.coe_comp, Function.comp_apply, f']

Goal state after:
case e'_5
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Field K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra F K
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
s : E
hs : s ∈ S
this✝ : Algebra L ↥L' := (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower L (↥L') E
e_3✝ : CommRing.toCommSemiring.toSemiring = Field.toSemifield.toDivisionSemiring.toSemiring
x✝ : L
⊢ f (↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm ((algebraMap L ↥L') x✝)) = f x✝
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hi : Irreducible f
hs : (Polynomial.map (algebraMap K L) f).Splits
⊢ f.natDegree ∣ finrank K L

Tactic:
have := hi.degree_pos.ne'
  rw [← f.degree_map (algebraMap K L)] at this
  obtain ⟨x, hx⟩ := hs.exists_eval_eq_zero this
  rw [eval_map_algebraMap] at hx
  have key := minpoly.Irreducible.eq_minpoly hi hx
  replace hi := hi.ne_zero
  rw [key, natDegree_C_mul (leadingCoeff_ne_zero.mpr hi)]
  apply minpoly.degree_dvd
  rw [← minpoly.ne_zero_iff]
  contrapose hi
  rwa [hi, mul_zero] at key

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
pb : PowerBasis K L
⊢ pb.equivAdjoinSimple.symm pb.gen = AdjoinSimple.gen K pb.gen

Tactic:
rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
⊢ H ≤ zeroRootSubalgebra R L H

Tactic:
rw [← LieSubalgebra.toSubmodule_le_toSubmodule, ← H.coe_toLieSubmodule,
    coe_zeroRootSubalgebra, LieSubmodule.toSubmodule_le_toSubmodule]
  exact toLieSubmodule_le_rootSpace_zero R L H

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

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (B x) y = (B x) y * 2⁻¹ * 2

Tactic:
mul_assoc,

Goal state after:
M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (B x) y = (B x) y * (2⁻¹ * 2)
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
sym : B.IsSymm
b : Basis ι K V
i j : ι
⊢ (B ((B.dualBasis hB b) j)) (b i) = if i = j then 1 else 0

Tactic:
apply_dualBasis_left

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
sym : B.IsSymm
b : Basis ι K V
i j : ι
⊢ (if i = j then 1 else 0) = if i = j then 1 else 0
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h : ⇑(B.dualBasis hB b) = v
x✝¹ x✝ : ι
⊢ (B ((B.dualBasis hB b) x✝¹)) (b x✝) = if x✝ = x✝¹ then 1 else 0

Tactic:
apply_dualBasis_left

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h : ⇑(B.dualBasis hB b) = v
x✝¹ x✝ : ι
⊢ (if x✝ = x✝¹ then 1 else 0) = if x✝ = x✝¹ then 1 else 0
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case smul
ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅b.e i, t • u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
rw [lie_smul]

Goal state after:
case smul
ι : 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 z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x : L
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.f)
hu : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ t • ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
x : L
y : M
⊢ y ∈ (Φ.orthogonal ↑N).carrier → ⁅x, y⁆ ∈ (Φ.orthogonal ↑N).carrier

Tactic:
by
    suffices (∀ n ∈ N, Φ n y = 0) → ∀ n ∈ N, Φ n ⁅x, y⁆ = 0 by
      simpa only [
        AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
        LinearMap.BilinForm.mem_orthogonal_iff, LieSubmodule.mem_toSubmodule]
    intro H a ha
    rw [← neg_eq_zero, ← hΦ_inv]
    exact H _ <| N.lie_mem ha

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl I (orthogonal Φ hΦ_inv I)

Tactic:
rw [← LieSubmodule.isCompl_toSubmodule]
  exact orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
R : 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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
x y : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ))
        ((toEnd R L ↥(genWeightSpace M χ)) x * (toEnd R L ↥(genWeightSpace M χ)) y) -
      (LinearMap.trace R ↥(genWeightSpace M χ))
        ((toEnd R L ↥(genWeightSpace M χ)) y * (toEnd R L ↥(genWeightSpace M χ)) x) =
    0

Tactic:
LinearMap.trace_mul_comm,

Goal state after:
k : Type u_1
R : 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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
x y : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ))
        ((toEnd R L ↥(genWeightSpace M χ)) y * (toEnd R L ↥(genWeightSpace M χ)) x) -
      (LinearMap.trace R ↥(genWeightSpace M χ))
        ((toEnd R L ↥(genWeightSpace M χ)) y * (toEnd R L ↥(genWeightSpace M χ)) x) =
    0
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:
rw [hasTrivialRadical_iff_no_abelian_ideals]
  intro I hI
  apply (eq_bot_or_exists_atom_le I).resolve_right
  rintro ⟨J, hJ, hJ'⟩
  apply IsSemisimple.non_abelian_of_isAtom J hJ
  constructor
  intro x y
  ext
  simp only [LieIdeal.coe_bracket_of_module, LieSubmodule.coe_bracket, ZeroMemClass.coe_zero]
  have : (⁅(⟨x, hJ' x.2⟩ : I), ⟨y, hJ' y.2⟩⁆ : I) = 0 := trivial_lie_zero _ _ _ _
  apply_fun Subtype.val at this
  exact this

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
  apply InvariantForm.isSemisimple_of_nondegenerate (Φ := killingForm K L)
  · exact IsKilling.killingForm_nondegenerate _ _
  · exact LieModule.traceForm_lieInvariant _ _ _
  · exact (LieModule.traceForm_isSymm K L L).isRefl
  · intro I h₁ h₂
    exact h₁.1 <| IsKilling.ideal_eq_bot_of_isLieAbelian I

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
⊢ (map (↑e.flip.symm) p).dualAnnihilator = map (↑e) p.dualCoannihilator

Tactic:
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
  rw [← map_dualCoannihilator_linearEquiv_flip, ← LinearEquiv.coe_toLinearMap_flip,
    LinearEquiv.flip_flip]

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : corootSpace ⇑α ≠ ⊥
⊢ (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule ≠ ⊥

Tactic:
rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at hα

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).degree = ↑(↑n + 1).natAbs
ih2 : (T R ↑n).degree = ↑(↑n).natAbs
⊢ (2 * X * T R (↑n + 1)).degree = ↑(n + 2)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).degree = ↑(↑n + 1).natAbs
ih2 : (T R ↑n).degree = ↑(↑n).natAbs
⊢ (2 * (X * T R (↑n + 1))).degree = ↑(n + 2)
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: case add_two
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).leadingCoeff = 2 ^ ((↑n + 1).natAbs - 1)
ih2 : (T R ↑n).leadingCoeff = 2 ^ ((↑n).natAbs - 1)
this : leadingCoeff 2 = 2
⊢ (T R ↑n).degree < (2 * X * T R (↑n + 1)).degree

Tactic:
mul_assoc,

Goal state after:
case add_two
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (T R (↑n + 1)).leadingCoeff = 2 ^ ((↑n + 1).natAbs - 1)
ih2 : (T R ↑n).leadingCoeff = 2 ^ ((↑n).natAbs - 1)
this : leadingCoeff 2 = 2
⊢ (T R ↑n).degree < (2 * (X * T R (↑n + 1))).degree
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
this : ⁅⁅e, f'⁆, e⁆ = α h • e
⊢ (2 * (α h)⁻¹ * α h) • e = 2 • e

Tactic:
mul_assoc,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
e : L
heα : e ∈ rootSpace H ⇑α
he₀ : e ≠ 0
f' : L
hfα : f' ∈ rootSpace H (-⇑α)
hf : ((killingForm K L) e) f' ≠ 0
hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
h : ↥H := ⟨⁅e, f'⁆, ⋯⟩
hh : α h ≠ 0
f : L := (2 * (α h)⁻¹) • f'
this : ⁅⁅e, f'⁆, e⁆ = α h • e
⊢ (2 * ((α h)⁻¹ * α h)) • e = 2 • e
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
⊢ (2 * X * U R (↑n + 1)).degree = ↑(n + 2)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NeZero 2
n : ℕ
ih1 : (U R ↑n).degree = ↑n
ih2 : (U R (↑n + 1)).degree = ↑n + 1
⊢ (2 * (X * U R (↑n + 1))).degree = ↑(n + 2)