awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
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)
⊢ 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)

Tactic:
simp_rw [killingForm_apply_apply, ← LieAlgebra.conj_ad_apply, ← LinearEquiv.conj_comp,
    LinearMap.trace_conj']

Premises used: LinearEquiv.conj_comp, killingForm_apply_apply, LieAlgebra.conj_ad_apply, LinearMap.trace_conj'
-- 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
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
killingCompl_top_eq_bot : Eq (α := LieIdeal R L') (LieIdeal.killingCompl R L' ⊤) ⊥
⊢ IsKilling R 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
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
killingCompl_top_eq_bot :
  ∀ (x' : L'),
    Membership.mem (γ := LieSubmodule R L' L') (LieIdeal.killingCompl R L' ⊤) x' ↔
      Membership.mem (γ := LieSubmodule R L' L') ⊥ x'
⊢ Eq (α := LieIdeal R L') (LieIdeal.killingCompl R L' ⊤) ⊥

Tactic:
ext x'
-- 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
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
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'
⊢ Membership.mem (γ := LieSubmodule R L' L') (LieIdeal.killingCompl R L' ⊤) x' ↔
    Membership.mem (γ := LieSubmodule R L' L') ⊥ x'

Tactic:
simp_rw [LieIdeal.mem_killingCompl, LieModule.traceForm_comm]

Premises used: LieIdeal.mem_killingCompl, LieModule.traceForm_comm
-- 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
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'

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

Premises used: Eq.rec, killingForm, LinearMap.map_zero₂, Iff.intro, Eq.symm
-- 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
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
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'
⊢ (∀ (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⟩
-- 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
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.{u_3, u_3} (α := L) (γ := Submodule R L) ⊥ ((e.symm : (a : L') → L) x' : L)

Tactic:
rw [IsKilling.ker_killingForm_eq_bot] at this

Premises used: LieAlgebra.IsKilling.ker_killingForm_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
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.{u_3, u_3} (α := L) (γ := Submodule R L) ⊥ ((e.symm : (a : L') → L) x' : L)
⊢ Membership.mem (γ := LieSubmodule R L' L') ⊥ x'

Tactic:
simpa [map_zero] using (e : L ≃ₗ[R] L').congr_arg this

Premises used: map_zero, LinearEquiv.congr_arg
-- 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
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)
killingCompl_top_eq_bot :
  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'

Tactic:
suffices e.symm x' ∈ LinearMap.ker (killingForm R L) by
    rw [IsKilling.ker_killingForm_eq_bot] at this
    simpa [map_zero] using (e : L ≃ₗ[R] L').congr_arg this
-- 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
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)
killingCompl_top_eq_bot :
  ∀ (y : L),
    Eq.{u_1 + 1} (α := R)
      ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
      ((0 : (a : L) → R) y : R)
⊢ Membership.mem (α := L) (γ := Submodule R L) (LinearMap.ker (killingForm R L)) ((e.symm : (a : L') → L) x' : L)

Tactic:
ext y
-- 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
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)
y : L
⊢ ∀ (y' : L'),
    Eq.{u_1 + 1} (α := R) ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y' : R) (0 : R)

Tactic:
simpa using hx'
-- 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
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)
y : L
⊢ ∀ (y' : L'),
    Eq.{u_1 + 1} (α := R) ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y' : R) (0 : R)

Tactic:
replace hx' : ∀ y', killingForm R L' x' y' = 0 := by simpa using hx'
-- 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
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
hx' :
  ∀ (y' : L'),
    Eq.{u_1 + 1} (α := R) ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y' : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) ((e : (a : L) → L') y : L') : R)
    (0 : R)

Tactic:
specialize hx' (e y)

Premises used: DFunLike.coe
-- 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
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
hx' :
  Eq.{u_1 + 1} (α := R)
    ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) ((e : (a : L) → L') y : L') : R)
    (0 : R)
killingCompl_top_eq_bot :
  ∀
    (hx' :
      Eq.{u_1 + 1} (α := R)
        ((((killingForm R L' : (a : L') → L' →ₗ[R] R) ((e : (a : L) → L') ((e.symm : (a : L') → L) x' : L)) :
                L' →ₗ[R] R) :
              (a : L') → R)
            ((e : (a : L) → L') y : L') :
          R)
        (0 : R)),
    Eq.{u_1 + 1} (α := R)
      ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
      ((0 : (a : L) → R) y : R)
killingCompl_top_eq_bot₁ killingCompl_top_eq_bot₂ killingCompl_top_eq_bot₃ killingCompl_top_eq_bot₄ :
  ∀
    (hx' :
      Eq.{u_1 + 1} (α := R)
        ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
        (0 : R)),
    Eq.{u_1 + 1} (α := R)
      ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
      ((0 : (a : L) → R) y : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
    ((0 : (a : L) → R) y : R)

Tactic:
rwa [← e.apply_symm_apply x', killingForm_of_equiv_apply] at hx'

Premises used: LieEquiv.apply_symm_apply, LieAlgebra.killingForm_of_equiv_apply
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
rwa : IsCompl (↑I : Submodule K L) (↑(killingCompl K L I) : Submodule K L)
rwa₁ : IsCompl (↑I : Submodule K L) (LinearMap.BilinForm.orthogonal (killingForm K L) (↑I : Submodule K L))
rwa₂ : Disjoint (↑I : Submodule K L) (LinearMap.BilinForm.orthogonal (LieModule.traceForm K L L) (↑I : Submodule K L))
rwa₃ : Disjoint (↑I : Submodule K L) (↑(killingCompl K L I) : Submodule K L)
rwa₄ rwa₅ rwa₆ rwa₇ : Disjoint I (killingCompl K L I)
⊢ IsCompl I (killingCompl K L I)

Tactic:
rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]

Premises used: LieSubmodule.disjoint_toSubmodule, LieSubmodule.isCompl_toSubmodule, LieModule.traceForm_isSymm, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint, LinearMap.IsSymm.isRefl, LieIdeal.toSubmodule_killingCompl
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
suffices : Disjoint I (killingCompl K L I)
⊢ IsCompl I (killingCompl K L I)

Tactic:
suffices Disjoint I I.killingCompl by
    rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)
rw : I ⊓ killingCompl K L I = ⊥
⊢ Disjoint I (killingCompl K L I)

Tactic:
rw [disjoint_iff]

Premises used: disjoint_iff
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)
⊢ I ⊓ killingCompl K L I = ⊥

Tactic:
IsKilling.ideal_eq_bot_of_isLieAbelian _

Premises used: LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)
⊢ I ⊓ killingCompl K L I = ⊥

Tactic:
exact IsKilling.ideal_eq_bot_of_isLieAbelian _

Premises used: LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
suffices : IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)
⊢ Disjoint I (killingCompl K L I)

Tactic:
suffices IsLieAbelian (I ⊓ I.killingCompl : LieIdeal K L) by
    rw [disjoint_iff]
    exact IsKilling.ideal_eq_bot_of_isLieAbelian _
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this :
  ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
    Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, y⁆ : L →ₗ[K] K) : (a : L) → K) z : K)
      (0 : K)
rw : ∀ x ∈ I ⊓ killingCompl K L I, ∀ m ∈ I ⊓ killingCompl K L I, ⁅x, m⁆ = 0
⊢ IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)

Tactic:
rw [LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieSubmodule.lie_eq_bot_iff]

Premises used: LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieSubmodule.lie_eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this :
  ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
    Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, y⁆ : L →ₗ[K] K) : (a : L) → K) z : K)
      (0 : K)
x : L
hx : x ∈ (↑(↑(killingCompl K L I) : Submodule K L) : Set L)
y : L
hy : y ∈ (↑(↑I : Submodule K L) : Set L)
⊢ ⁅x, y⁆ = 0

Tactic:
(IsKilling.killingForm_nondegenerate K L).1 _ fun z ↦ this x y z hx hy

Premises used: LieAlgebra.IsKilling.killingForm_nondegenerate, And.left
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this :
  ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
    Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, y⁆ : L →ₗ[K] K) : (a : L) → K) z : K)
      (0 : K)
x : L
hx : x ∈ (↑(↑(killingCompl K L I) : Submodule K L) : Set L)
y : L
hy : y ∈ (↑(↑I : Submodule K L) : Set L)
⊢ ⁅x, y⁆ = 0

Tactic:
exact (IsKilling.killingForm_nondegenerate K L).1 _ fun z ↦ this x y z hx hy

Premises used: LieAlgebra.IsKilling.killingForm_nondegenerate, And.left
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
suffices :
  ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
    Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, y⁆ : L →ₗ[K] K) : (a : L) → K) z : K)
      (0 : K)
⊢ IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)

Tactic:
suffices ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
      LieModule.traceForm K L L ⁅x, y⁆ z = 0 by
    rw [LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieSubmodule.lie_eq_bot_iff]
    rintro x ⟨-, hx⟩ y ⟨hy, -⟩
    exact (IsKilling.killingForm_nondegenerate K L).1 _ fun z ↦ this x y z hx hy
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
x y z : L
hx : x ∈ killingCompl K L I
hy : y ∈ I
rw :
  Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅y, z⁆ : L →ₗ[K] K) : (a : L) → K) x : K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, y⁆ : L →ₗ[K] K) : (a : L) → K) z : K)
    (0 : K)

Tactic:
rw [LieModule.traceForm_apply_lie_apply K L L x y z, LieModule.traceForm_comm K L L]

Premises used: LieModule.traceForm_comm, LieModule.traceForm_apply_lie_apply
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
x y z : L
hx : x ∈ killingCompl K L I
hy : y ∈ I
⊢ Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅y, z⁆ : L →ₗ[K] K) : (a : L) → K) x : K)
    (0 : K)

Tactic:
I.mem_killingCompl.mp hx _ <| lie_mem_left K L I y z hy

Premises used: LieIdeal.mem_killingCompl, Iff.mp, lie_mem_left
-- Module: Mathlib.Algebra.Lie.Killing
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
x y z : L
hx : x ∈ killingCompl K L I
hy : y ∈ I
⊢ Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅y, z⁆ : L →ₗ[K] K) : (a : L) → K) x : K)
    (0 : K)

Tactic:
exact I.mem_killingCompl.mp hx _ <| lie_mem_left K L I y z hy

Premises used: LieIdeal.mem_killingCompl, Iff.mp, lie_mem_left
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : Membership.mem (γ := LieSubmodule R A V) (weightSpace V χ) v
rw : ∀ (hv : ∀ (x : A), ⁅x, v⁆ = χ x • v) (x : A), ⁅x, ⁅z, v⁆⁆ = χ x • ⁅z, v⁆
⊢ Membership.mem (γ := LieSubmodule R A V) (weightSpace V χ) ⁅z, v⁆

Tactic:
rw [mem_weightSpace] at hv ⊢

Premises used: LieModule.mem_weightSpace
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
inl : ∀ (hv : ∀ (x : A), ⁅x, 0⁆ = HSMul.hSMul (β := V) (χ x) 0), ⁅a, ⁅z, 0⁆⁆ = HSMul.hSMul (β := V) (χ a) ⁅z, 0⁆
inr : ∀ (hv' : v ≠ 0), ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆

Tactic:
rcases eq_or_ne v 0 with (rfl | hv')

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
a : A
hv : ∀ (x : A), ⁅x, 0⁆ = HSMul.hSMul (β := V) (χ x) 0
⊢ ⁅a, ⁅z, 0⁆⁆ = HSMul.hSMul (β := V) (χ a) ⁅z, 0⁆

Tactic:
simp only [lie_zero, smul_zero]

Premises used: smul_zero, lie_zero
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
rw₂ : ⁅⁅a, z⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₃ : -⁅⁅z, a⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₄ : -(χ ⁅z, a⁆ • v) + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₅ : -HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 v + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₆ : -0 + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₇ : 0 + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₈ rw₉ : χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆

Tactic:
rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]

Premises used: leibniz_lie, lie_smul, zero_add, zero_smul, neg_zero, lie_swap_lie
-- Module: Mathlib.Algebra.Lie.LieTheorem
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
inr : χ ⁅z, a⁆ = 0
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆

Tactic:
suffices χ ⁅z, a⁆ = 0 by
    rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]