awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
h :
  ∀ (y : LieIdeal K L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : LieIdeal K L) ↦ finrank.{u_1, u_2} K ↥x) y I →
      sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h_1 : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
⊢ J ≤ ⊥

Tactic:
orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL J hJ le_rfl (hJI.trans hIJ')

Premises used: LieAlgebra.InvariantForm.orthogonal_disjoint, le_rfl, LE.le.trans
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
h :
  ∀ (y : LieIdeal K L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : LieIdeal K L) ↦ finrank.{u_1, u_2} K ↥x) y I →
      sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h_1 : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
⊢ J ≤ ⊥

Tactic:
exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL J hJ le_rfl (hJI.trans hIJ')

Premises used: LieAlgebra.InvariantForm.orthogonal_disjoint, le_rfl, LE.le.trans
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
h :
  ∀ (y : LieIdeal K L),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2) (fun (x : LieIdeal K L) ↦ finrank.{u_1, u_2} K ↥x) y I →
      sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h_1 : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hst : (↑(orthogonal Φ hΦ_inv J ⊓ I) : Submodule K L) < (↑I : Submodule K L)
hst₁ : ¬I ≤ J'
hst₂ : ∀ (hIJ' : I ≤ J'), False
hst₃ : ∀ (hIJ' : I ≤ J'), J = ⊥
hst₄ : ∀ (hIJ' : I ≤ J'), J ≤ ⊥
⊢ finrank.{u_1, u_2} K ↥(orthogonal Φ hΦ_inv J ⊓ I) < finrank.{u_1, u_2} K ↥I

Tactic:
decreasing_by
  apply finrank_lt_finrank_of_lt
  suffices ¬I ≤ J' by simpa
  intro hIJ'
  apply hJ.1
  rw [eq_bot_iff]
  exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL J hJ le_rfl (hJI.trans hIJ')

Premises used: Submodule.finrank_lt_finrank_of_lt, And.left, eq_bot_iff
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
⊢ IsSemisimple K L

Tactic:
⟨?_, ?_, hL⟩

Premises used: LieAlgebra.IsSemisimple.mk
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
refine_1 : Eq.{u_2 + 1} (α := LieIdeal K L) (sSup {I : LieIdeal K L | IsAtom I}) ⊤
refine_2 : sSupIndep.{u_2} (α := LieIdeal K L) {I : LieIdeal K L | IsAtom I}
⊢ IsSemisimple K L

Tactic:
refine ⟨?_, ?_, hL⟩
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
⊢ Eq.{u_2 + 1} (α := LieIdeal K L) (sSup {I : LieIdeal K L | IsAtom I}) ⊤

Tactic:
simpa using atomistic Φ hΦ_nondeg hΦ_inv hΦ_refl hL ⊤

Premises used: Top.top, LieAlgebra.InvariantForm.atomistic
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
refine_2 : sSup ({I : LieIdeal K L | IsAtom I} \ {I}) ≤ orthogonal Φ hΦ_inv I
⊢ Disjoint I (sSup ({I : LieIdeal K L | IsAtom I} \ {I}))

Tactic:
apply (orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI).mono_right

Premises used: LieAlgebra.InvariantForm.orthogonal_disjoint, Disjoint.mono_right
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
refine_2 :
  ∀ (b : LieIdeal K L),
    Membership.mem (γ := Set (LieIdeal K L)) ({I : LieIdeal K L | IsAtom I} \ {I}) b → b ≤ orthogonal Φ hΦ_inv I
⊢ sSup ({I : LieIdeal K L | IsAtom I} \ {I}) ≤ orthogonal Φ hΦ_inv I

Tactic:
apply sSup_le

Premises used: sSup_le
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
refine_2 : ∀ (b : LieIdeal K L), IsAtom b → ¬b = I → b ≤ orthogonal Φ hΦ_inv I
⊢ ∀ (b : LieIdeal K L),
    Membership.mem (γ := Set (LieIdeal K L)) ({I : LieIdeal K L | IsAtom I} \ {I}) b → b ≤ orthogonal Φ hΦ_inv I

Tactic:
simp only [Set.mem_diff, Set.mem_setOf_eq, Set.mem_singleton_iff, and_imp]

Premises used: and_imp, Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
refine_2 : {x : L | ∃ (x_1 : ↥J) (n : ↥J), ⁅(↑x_1 : L), (↑n : L)⁆ = x} ⊆ (↑(orthogonal Φ hΦ_inv I) : Set L)
⊢ J ≤ orthogonal Φ hΦ_inv I

Tactic:
rw [← lie_eq_self_of_isAtom_of_nonabelian J hJ (hL J hJ), lieIdeal_oper_eq_span, lieSpan_le]

Premises used: lie_eq_self_of_isAtom_of_nonabelian, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
refine_2 :
  Eq.{u_1 + 1} (α := K) ((((Φ : (a : L) → L →ₗ[K] K) ⁅(↑x : L), z⁆ : L →ₗ[K] K) : (a : L) → K) (↑y : L) : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((((Φ : (a : L) → L →ₗ[K] K) z : L →ₗ[K] K) : (a : L) → K) ⁅(↑x : L), (↑y : L)⁆ : K) (0 : K)

Tactic:
rw [← neg_eq_zero, ← hΦ_inv]

Premises used: neg_eq_zero
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
this : ⁅(↑x : L), z⁆ = 0
⊢ Eq.{u_1 + 1} (α := K) ((((Φ : (a : L) → L →ₗ[K] K) ⁅(↑x : L), z⁆ : L →ₗ[K] K) : (a : L) → K) (↑y : L) : K) (0 : K)

Tactic:
simp only [this, map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, map_zero
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
refine_2 : ⁅(↑x : L), z⁆ = 0
⊢ Eq.{u_1 + 1} (α := K) ((((Φ : (a : L) → L →ₗ[K] K) ⁅(↑x : L), z⁆ : L →ₗ[K] K) : (a : L) → K) (↑y : L) : K) (0 : K)

Tactic:
suffices ⁅(x : L), z⁆ = 0 by simp only [this, map_zero, LinearMap.zero_apply]
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
refine_2 : ⁅(↑x : L), z⁆ ∈ J ⊓ I
⊢ ⁅(↑x : L), z⁆ = 0

Tactic:
rw [← LieSubmodule.mem_bot (R := K) (L := L), ← (hJ.disjoint_of_ne hI hJI).eq_bot]

Premises used: IsAtom.disjoint_of_ne, LieSubmodule.mem_bot, Disjoint.eq_bot
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
refine_2 : ⁅(↑x : L), z⁆ ∈ ⁅J, I⁆
⊢ ⁅(↑x : L), z⁆ ∈ J ⊓ I

Tactic:
apply lie_le_inf

Premises used: LieSubmodule.lie_le_inf
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
⊢ ⁅(↑x : L), z⁆ ∈ ⁅J, I⁆

Tactic:
lie_mem_lie x.2 hz

Premises used: Set.Mem, LieSubmodule.lie_mem_lie, Subtype.property
-- Module: Mathlib.Algebra.Lie.InvariantForm
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : 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.{u_2} ↥I
I : LieIdeal K L
hI : Membership.mem (γ := Set (LieIdeal K L)) {I : LieIdeal K L | IsAtom I} I
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
⊢ ⁅(↑x : L), z⁆ ∈ ⁅J, I⁆

Tactic:
exact lie_mem_lie x.2 hz

Premises used: LieSubmodule.lie_mem_lie, Subtype.property
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
⊢ Eq (α := Submodule R L) (LinearMap.ker (killingForm R L)) ⊥

Tactic:
simp [← LieIdeal.coe_killingCompl_top, killingCompl_top_eq_bot]

Premises used: LieIdeal.coe_killingCompl_top, LieAlgebra.IsKilling.killingCompl_top_eq_bot
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
⊢ LinearMap.BilinForm.Nondegenerate (killingForm R L)

Tactic:
(LieModule.traceForm_isSymm R L L).isRefl.nondegenerate_iff_separatingLeft.mpr ?_

Premises used: Iff.mpr, LieModule.traceForm_isSymm, LinearMap.IsSymm.isRefl, LinearMap.IsRefl.nondegenerate_iff_separatingLeft
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
refine : LinearMap.SeparatingLeft (LieModule.traceForm R L L)
⊢ LinearMap.BilinForm.Nondegenerate (killingForm R L)

Tactic:
refine (LieModule.traceForm_isSymm R L L).isRefl.nondegenerate_iff_separatingLeft.mpr ?_

Premises used: Iff.mpr, LieModule.traceForm_isSymm, LinearMap.IsSymm.isRefl, LinearMap.IsRefl.nondegenerate_iff_separatingLeft
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
⊢ LinearMap.SeparatingLeft (LieModule.traceForm R L L)

Tactic:
simp [LinearMap.separatingLeft_iff_ker_eq_bot]

Premises used: LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
I : LieIdeal R L
inst_8 : IsLieAbelian.{u_3} ↥I
rw : I ≤ LieIdeal.killingCompl R L ⊤
⊢ I = ⊥

Tactic:
rw [eq_bot_iff, ← killingCompl_top_eq_bot]

Premises used: LieAlgebra.IsKilling.killingCompl_top_eq_bot, eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
I : LieIdeal R L
inst_8 : IsLieAbelian.{u_3} ↥I
⊢ I ≤ LieIdeal.killingCompl R L ⊤

Tactic:
I.le_killingCompl_top_of_isLieAbelian

Premises used: LieIdeal.le_killingCompl_top_of_isLieAbelian
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
I : LieIdeal R L
inst_8 : IsLieAbelian.{u_3} ↥I
⊢ I ≤ LieIdeal.killingCompl R L ⊤

Tactic:
exact I.le_killingCompl_top_of_isLieAbelian

Premises used: LieIdeal.le_killingCompl_top_of_isLieAbelian
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
hΦ_nondeg : LinearMap.BilinForm.Nondegenerate (killingForm K L)
hΦ_inv : LinearMap.BilinForm.lieInvariant L (killingForm K L)
hΦ_refl : LinearMap.BilinForm.IsRefl (killingForm K L)
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_3} ↥I
⊢ IsSemisimple K L

Tactic:
apply InvariantForm.isSemisimple_of_nondegenerate (Φ := killingForm K L)

Premises used: killingForm, LieAlgebra.InvariantForm.isSemisimple_of_nondegenerate
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
⊢ LinearMap.BilinForm.Nondegenerate (killingForm K L)

Tactic:
IsKilling.killingForm_nondegenerate _ _

Premises used: LieAlgebra.IsKilling.killingForm_nondegenerate
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
⊢ LinearMap.BilinForm.Nondegenerate (killingForm K L)

Tactic:
exact IsKilling.killingForm_nondegenerate _ _

Premises used: LieAlgebra.IsKilling.killingForm_nondegenerate
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
⊢ LinearMap.BilinForm.lieInvariant L (killingForm K L)

Tactic:
LieModule.traceForm_lieInvariant _ _ _

Premises used: LieModule.traceForm_lieInvariant
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
⊢ LinearMap.BilinForm.lieInvariant L (killingForm K L)

Tactic:
exact LieModule.traceForm_lieInvariant _ _ _

Premises used: LieModule.traceForm_lieInvariant
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
⊢ LinearMap.BilinForm.IsRefl (killingForm K L)

Tactic:
(LieModule.traceForm_isSymm K L L).isRefl

Premises used: LieModule.traceForm_isSymm, LinearMap.IsSymm.isRefl, LinearMap.BilinForm.IsRefl
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
⊢ LinearMap.BilinForm.IsRefl (killingForm K L)

Tactic:
exact (LieModule.traceForm_isSymm K L L).isRefl

Premises used: LieModule.traceForm_isSymm, LinearMap.IsSymm.isRefl
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
I : LieIdeal K L
h₁ : IsAtom I
h₂ : IsLieAbelian.{u_3} ↥I
⊢ False

Tactic:
h₁.1 <| IsKilling.ideal_eq_bot_of_isLieAbelian I

Premises used: And.left, LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : IsKilling K L
inst_7 : Module.Finite K L
I : LieIdeal K L
h₁ : IsAtom I
h₂ : IsLieAbelian.{u_3} ↥I
⊢ False

Tactic:
exact h₁.1 <| IsKilling.ideal_eq_bot_of_isLieAbelian I

Premises used: And.left, LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : LieRing L
inst_3 : LieAlgebra R L
inst_4 : LieAlgebra K L
inst_5 : IsKilling R L
inst_6 : Module.Free R L
inst_7 : Module.Finite R L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
⊢ HasTrivialRadical R L

Tactic:
(hasTrivialRadical_iff_no_abelian_ideals R L).mpr IsKilling.ideal_eq_bot_of_isLieAbelian

Premises used: Iff.mpr, LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian, LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
mp : IsLieAbelian L → Subsingleton L
mpr : Subsingleton L → IsLieAbelian L
⊢ IsLieAbelian L ↔ Subsingleton L

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
h : IsLieAbelian L
⊢ Eq (α := LieIdeal R L) (center R L) ⊤

Tactic:
rw [isLieAbelian_iff_center_eq_top R] at h

Premises used: LieAlgebra.isLieAbelian_iff_center_eq_top
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
h : Eq (α := LieIdeal R L) (center R L) ⊤
rw : Eq (α := LieIdeal R L) ⊤ (center R L)
rw₁ rw₂ : Eq.{u_3 + 1} (α := LieIdeal R L) ⊤ ⊤
⊢ Eq.{u_3 + 1} (α := LieIdeal R L) ⊤ ⊥

Tactic:
rw [← center_eq_bot R L, h]

Premises used: LieAlgebra.center_eq_bot
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
h : Eq (α := LieIdeal R L) (center R L) ⊤
⊢ Eq.{u_3 + 1} (α := LieIdeal R L) ⊤ ⊥

Tactic:
have hc : (⊤ : LieIdeal R L) = ⊥ := by rw [← center_eq_bot R L, h]
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
h : Eq (α := LieIdeal R L) (center R L) ⊤
hc : Eq.{u_3 + 1} (α := LieIdeal R L) ⊤ ⊥
⊢ Subsingleton L

Tactic:
(LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_top_eq_bot hc)

Premises used: subsingleton_of_top_eq_bot, Iff.mp, LieSubmodule.subsingleton_iff
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
h : Eq (α := LieIdeal R L) (center R L) ⊤
hc : Eq.{u_3 + 1} (α := LieIdeal R L) ⊤ ⊥
⊢ Subsingleton L

Tactic:
exact (LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_top_eq_bot hc)

Premises used: subsingleton_of_top_eq_bot, Iff.mp, LieSubmodule.subsingleton_iff
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
⊢ Subsingleton L → IsLieAbelian L

Tactic:
fun _ => inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsKilling R L
inst_4 : Module.Free R L
inst_5 : Module.Finite R L
inst_6 : IsDomain R
inst_7 : IsPrincipalIdealRing R
⊢ Subsingleton L → IsLieAbelian L

Tactic:
exact fun _ => inferInstance