awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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)
⊢ finrank.{u_1, u_2} K ↥(orthogonal Φ hΦ_inv J ⊓ I) < finrank.{u_1, u_2} K ↥I
have hst₁ : ¬I ≤ J'
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')
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ finrank.{u_1, u_2} K ↥(orthogonal Φ hΦ_inv J ⊓ I) < finrank.{u_1, u_2} K ↥I
have hst₃ : ∀ (hIJ' : I ≤ J'), J = ⊥
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')
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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 = ⊥
⊢ finrank.{u_1, u_2} K ↥(orthogonal Φ hΦ_inv J ⊓ I) < finrank.{u_1, u_2} K ↥I
have hst₄ : ∀ (hIJ' : I ≤ J'), J ≤ ⊥
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')
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
have refine_1 : Eq.{u_2 + 1} (α := LieIdeal K L) (sSup {I : LieIdeal K L | IsAtom I}) ⊤
Tactic: refine ⟨?_, ?_, hL⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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}) ⊤
⊢ IsSemisimple K L
have refine_2 : sSupIndep.{u_2} (α := LieIdeal K L) {I : LieIdeal K L | IsAtom I}
Tactic: refine ⟨?_, ?_, hL⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ Disjoint I (sSup ({I : LieIdeal K L | IsAtom I} \ {I}))
have refine_2 : sSup ({I : LieIdeal K L | IsAtom I} \ {I}) ≤ orthogonal Φ hΦ_inv I
Tactic: apply (orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI).mono_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ sSup ({I : LieIdeal K L | IsAtom I} \ {I}) ≤ orthogonal Φ hΦ_inv I
have 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
Tactic: apply sSup_le
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ ∀ (b : LieIdeal K L),
    Membership.mem (γ := Set (LieIdeal K L)) ({I : LieIdeal K L | IsAtom I} \ {I}) b → b ≤ orthogonal Φ hΦ_inv I
have refine_2 : ∀ (b : LieIdeal K L), IsAtom b → ¬b = I → b ≤ orthogonal Φ hΦ_inv I
Tactic: simp only [Set.mem_diff, Set.mem_setOf_eq, Set.mem_singleton_iff, and_imp]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ J ≤ orthogonal Φ hΦ_inv I
have refine_2 : {x : L | ∃ (x_1 : ↥J) (n : ↥J), ⁅(↑x_1 : L), (↑n : L)⁆ = x} ⊆ (↑(orthogonal Φ hΦ_inv I) : Set L)
Tactic: rw [← lie_eq_self_of_isAtom_of_nonabelian J hJ (hL J hJ), lieIdeal_oper_eq_span, lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ Eq.{u_1 + 1} (α := K) ((((Φ : (a : L) → L →ₗ[K] K) z : L →ₗ[K] K) : (a : L) → K) ⁅(↑x : L), (↑y : L)⁆ : K) (0 : K)
have 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)
Tactic: rw [← neg_eq_zero, ← hΦ_inv]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
⊢ Eq.{u_1 + 1} (α := K) ((((Φ : (a : L) → L →ₗ[K] K) ⁅(↑x : L), z⁆ : L →ₗ[K] K) : (a : L) → K) (↑y : L) : K) (0 : K)
have refine_2 : ⁅(↑x : L), z⁆ = 0
Tactic: suffices ⁅(x : L), z⁆ = 0 by simp only [this, map_zero, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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⁆ = 0
have refine_2 : ⁅(↑x : L), z⁆ ∈ J ⊓ I
Tactic: rw [← LieSubmodule.mem_bot (R := K) (L := L), ← (hJ.disjoint_of_ne hI hJI).eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.InvariantForm (goal)
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
have refine_2 : ⁅(↑x : L), z⁆ ∈ ⁅J, I⁆
Tactic: apply lie_le_inf
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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)
have refine : LinearMap.SeparatingLeft (LieModule.traceForm R L L)
Tactic: refine (LieModule.traceForm_isSymm R L L).isRefl.nondegenerate_iff_separatingLeft.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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 = ⊥
have rw : I ≤ LieIdeal.killingCompl R L ⊤
Tactic: rw [eq_bot_iff, ← killingCompl_top_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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
⊢ IsSemisimple K L
have hΦ_nondeg : LinearMap.BilinForm.Nondegenerate (killingForm K L)
Tactic: apply InvariantForm.isSemisimple_of_nondegenerate (Φ := killingForm K L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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)
⊢ IsSemisimple K L
have hΦ_inv : LinearMap.BilinForm.lieInvariant L (killingForm K L)
Tactic: apply InvariantForm.isSemisimple_of_nondegenerate (Φ := killingForm K L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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)
⊢ IsSemisimple K L
have hΦ_refl : LinearMap.BilinForm.IsRefl (killingForm K L)
Tactic: apply InvariantForm.isSemisimple_of_nondegenerate (Φ := killingForm K L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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)
⊢ IsSemisimple K L
have hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian.{u_3} ↥I
Tactic: apply InvariantForm.isSemisimple_of_nondegenerate (Φ := killingForm K L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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
⊢ IsLieAbelian L ↔ Subsingleton L
have mp : IsLieAbelian L → Subsingleton L
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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
⊢ IsLieAbelian L ↔ Subsingleton L
have mpr : Subsingleton L → IsLieAbelian L
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (hypothesis)
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
⊢ Subsingleton L
have h₁ : Eq (α := LieIdeal R L) (center R L) ⊤
Tactic: rw [isLieAbelian_iff_center_eq_top R] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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) ⊤ ⊥
have rw : Eq (α := LieIdeal R L) ⊤ (center R L)
Tactic: rw [← center_eq_bot R L, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
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)
⊢ Eq.{u_3 + 1} (α := LieIdeal R L) ⊤ ⊥
have rw₁ : Eq.{u_3 + 1} (α := LieIdeal R L) ⊤ ⊤
Tactic: rw [← center_eq_bot R L, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (hypothesis)
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) ⊤
⊢ Subsingleton L
have hc : Eq.{u_3 + 1} (α := LieIdeal R L) ⊤ ⊥
Tactic: have hc : (⊤ : LieIdeal R L) = ⊥ := by rw [← center_eq_bot R L, h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x y : L
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L' : (a : L') → L' →ₗ[R] R) ((e : (a : L) → L') x) : L' →ₗ[R] R) : (a : L') → R)
        ((e : (a : L) → L') y : L') :
      R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
have simp_rw : Eq.{u_1 + 1} (α := R)
  ((LinearMap.trace R L' : (a : L' →ₗ[R] L') → R)
      ((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') ∘ₗ
        (ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') y : L')) :
    R)
  ((LinearMap.trace R L : (a : L →ₗ[R] L) → R)
      ((ad R L : (a : L) → Module.End R L) x ∘ₗ (ad R L : (a : L) → Module.End R L) y) :
    R)
Tactic: simp_rw [killingForm_apply_apply, ← LieAlgebra.conj_ad_apply, ← LinearEquiv.conj_comp,
    LinearMap.trace_conj']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x y : L
simp_rw :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R L' : (a : L' →ₗ[R] L') → R)
        ((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') ∘ₗ
          (ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') y : L')) :
      R)
    ((LinearMap.trace R L : (a : L →ₗ[R] L) → R)
        ((ad R L : (a : L) → Module.End R L) x ∘ₗ (ad R L : (a : L) → Module.End R L) y) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L' : (a : L') → L' →ₗ[R] R) ((e : (a : L) → L') x) : L' →ₗ[R] R) : (a : L') → R)
        ((e : (a : L) → L') y : L') :
      R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
have simp_rw₁ : Eq.{u_1 + 1} (α := R)
  ((LinearMap.trace R L' : (a : L' →ₗ[R] L') → R)
      ((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) ∘ₗ
        (e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) y)) :
    R)
  ((LinearMap.trace R L : (a : L →ₗ[R] L) → R)
      ((ad R L : (a : L) → Module.End R L) x ∘ₗ (ad R L : (a : L) → Module.End R L) y) :
    R)
Tactic: simp_rw [killingForm_apply_apply, ← LieAlgebra.conj_ad_apply, ← LinearEquiv.conj_comp,
    LinearMap.trace_conj']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x y : L
simp_rw :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R L' : (a : L' →ₗ[R] L') → R)
        ((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') ∘ₗ
          (ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') y : L')) :
      R)
    ((LinearMap.trace R L : (a : L →ₗ[R] L) → R)
        ((ad R L : (a : L) → Module.End R L) x ∘ₗ (ad R L : (a : L) → Module.End R L) y) :
      R)
simp_rw₁ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R L' : (a : L' →ₗ[R] L') → R)
        ((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) ∘ₗ
          (e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) y)) :
      R)
    ((LinearMap.trace R L : (a : L →ₗ[R] L) → R)
        ((ad R L : (a : L) → Module.End R L) x ∘ₗ (ad R L : (a : L) → Module.End R L) y) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L' : (a : L') → L' →ₗ[R] R) ((e : (a : L) → L') x) : L' →ₗ[R] R) : (a : L') → R)
        ((e : (a : L) → L') y : L') :
      R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
have simp_rw₂ : Eq.{u_1 + 1} (α := R)
  ((LinearMap.trace R L' : (a : L' →ₗ[R] L') → R)
      ((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L')
          ((ad R L : (a : L) → Module.End R L) x ∘ₗ (ad R L : (a : L) → Module.End R L) y) :
        Module.End R L') :
    R)
  ((LinearMap.trace R L : (a : L →ₗ[R] L) → R)
      ((ad R L : (a : L) → Module.End R L) x ∘ₗ (ad R L : (a : L) → Module.End R L) y) :
    R)
Tactic: simp_rw [killingForm_apply_apply, ← LieAlgebra.conj_ad_apply, ← LinearEquiv.conj_comp,
    LinearMap.trace_conj']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
⊢ IsKilling R L'
have killingCompl_top_eq_bot : Eq (α := LieIdeal R L') (LieIdeal.killingCompl R L' ⊤) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
⊢ Eq (α := LieIdeal R L') (LieIdeal.killingCompl R L' ⊤) ⊥
have killingCompl_top_eq_bot : ∀ (x' : L'),
  Membership.mem (γ := LieSubmodule R L' L') (LieIdeal.killingCompl R L' ⊤) x' ↔
    Membership.mem (γ := LieSubmodule R L' L') ⊥ x'
Tactic: ext x'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ Membership.mem (γ := LieSubmodule R L' L') (LieIdeal.killingCompl R L' ⊤) x' ↔
    Membership.mem (γ := LieSubmodule R L' L') ⊥ x'
have killingCompl_top_eq_bot : (∀ (y : L'),
    Membership.mem (γ := LieIdeal R L') ⊤ y →
      Eq.{u_1 + 1} (α := R)
        ((((LieModule.traceForm R L' L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y : R) (0 : R)) ↔
  Membership.mem (γ := LieSubmodule R L' L') ⊥ x'
Tactic: simp_rw [LieIdeal.mem_killingCompl, LieModule.traceForm_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
⊢ (∀ (y : L'),
      Membership.mem (γ := LieIdeal R L') ⊤ y →
        Eq.{u_1 + 1} (α := R)
          ((((LieModule.traceForm R L' L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y : R) (0 : R)) ↔
    Membership.mem (γ := LieSubmodule R L' L') ⊥ x'
have killingCompl_top_eq_bot : ∀
  (hx' :
    ∀ (y : L'),
      Membership.mem (γ := LieIdeal R L') ⊤ y →
        Eq.{u_1 + 1} (α := R)
          ((((LieModule.traceForm R L' L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y : R) (0 : R)),
  Membership.mem (γ := LieSubmodule R L' L') ⊥ x'
Tactic: refine ⟨fun hx' ↦ ?_, fun hx y _ ↦ hx ▸ LinearMap.map_zero₂ (killingForm R L') y⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (hypothesis)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' :
  ∀ (y : L'),
    Membership.mem (γ := LieIdeal R L') ⊤ y →
      Eq.{u_1 + 1} (α := R)
        ((((LieModule.traceForm R L' L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y : R) (0 : R)
this : Membership.mem (α := L) (γ := Submodule R L) (LinearMap.ker (killingForm R L)) ((e.symm : (a : L') → L) x' : L)
⊢ Membership.mem (γ := LieSubmodule R L' L') ⊥ x'
have this₁ : Membership.mem.{u_3, u_3} (α := L) (γ := Submodule R L) ⊥ ((e.symm : (a : L') → L) x' : L)
Tactic: rw [IsKilling.ker_killingForm_eq_bot] at this
Cleared hypotheses: this