awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e

Tactic:
lie_eq_smul_of_mem_rootSpace heα

Premises used: LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e

Tactic:
exact lie_eq_smul_of_mem_rootSpace heα

Premises used: LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
refine_1 :
  LE.le (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
refine_2 :
  LE.le (α := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
⊢ Eq (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
e : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
f : L
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
rw :
  ∃ (a : K),
    HSMul.hSMul (β := L) a (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
        (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)
⊢ ⁅e, f⁆ ∈ (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)

Tactic:
rw [lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα, SetLike.mem_coe,
        Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, SetLike.mem_coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
e : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
f : L
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ ∃ (a : K),
    HSMul.hSMul (β := L) a (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
        (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)

Tactic:
⟨killingForm K L e f, rfl⟩

Premises used: killingForm, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
e : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
f : L
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ ∃ (a : K),
    HSMul.hSMul (β := L) a (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := L)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
        (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)

Tactic:
exact ⟨killingForm K L e f, rfl⟩
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
⊢ {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x} ⊆
    (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)

Tactic:
have : {⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} ⊆
        K ∙ ((cartanEquivDual H).symm α : L) := by
      rintro - ⟨e, heα, f, hfα, rfl⟩
      rw [lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα, SetLike.mem_coe,
        Submodule.mem_span_singleton]
      exact ⟨killingForm K L e f, rfl⟩
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
this :
  {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x} ⊆
    (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)
⊢ Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x

Tactic:
simp only [LieSubmodule.mem_toSubmodule, mem_corootSpace] at hx'

Premises used: LieSubmodule.mem_toSubmodule, LieAlgebra.mem_corootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
this :
  {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x} ⊆
    (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
⊢ Membership.mem (γ := Submodule K L)
    (span K (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)) x

Tactic:
replace this := Submodule.span_mono this hx'
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
this :
  Membership.mem (γ := Submodule K L)
    (span K (↑(K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) : Set L)) x
⊢ Membership.mem (γ := Submodule K L)
    (K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) x

Tactic:
rw [Submodule.span_span] at this

Premises used: Submodule.span_span
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
this :
  Membership.mem (γ := Submodule K L)
    (K ∙ (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)) x
refine_1 :
  ∀
    (this :
      ∃ (a : K),
        HSMul.hSMul (β := L) a (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) =
          x),
    ∃ (a : K),
      HSMul.hSMul (β := ↥H) a (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) =
        Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx
⊢ Membership.mem (γ := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)

Tactic:
rw [Submodule.mem_span_singleton] at this ⊢

Premises used: Submodule.mem_span_singleton
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x}) x
this :
  ∃ (a : K),
    HSMul.hSMul (β := L) a (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) = x
refine_1 :
  ∀ (t : K)
    (hx :
      HSMul.hSMul (β := L) t (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) ∈
        H)
    (hx' :
      Membership.mem (γ := Submodule K L)
        (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x})
        (HSMul.hSMul (β := L) t
          (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L))),
    ∃ (a : K),
      HSMul.hSMul (β := ↥H) a (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) =
        Subtype.mk (p := fun (x : L) ↦ x ∈ H)
          (HSMul.hSMul (β := L) t
            (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L))
          hx
⊢ ∃ (a : K),
    HSMul.hSMul (β := ↥H) a (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) =
      Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx

Tactic:
obtain ⟨t, rfl⟩ := this

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
t : K
hx : HSMul.hSMul (β := L) t (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L) ∈ H
hx' :
  Membership.mem (γ := Submodule K L)
    (span K {x : L | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = x})
    (HSMul.hSMul (β := L) t (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L))
⊢ ∃ (a : K),
    HSMul.hSMul (β := ↥H) a (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) =
      Subtype.mk (p := fun (x : L) ↦ x ∈ H)
        (HSMul.hSMul (β := L) t (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L))
        hx

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
refine_2 :
  Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieSubmodule K ↥H ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
⊢ LE.le (α := Submodule K ↥H)
    (span K (singleton (α := ↥H) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)))
    (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)

Tactic:
simp only [Submodule.span_singleton_le_iff_mem, LieSubmodule.mem_toSubmodule]

Premises used: LieSubmodule.mem_toSubmodule, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieSubmodule K ↥H ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)

Tactic:
cartanEquivDual_symm_apply_mem_corootSpace α

Premises used: Set.Mem, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : PerfectField K
α : Weight K (↥H) L
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieSubmodule K ↥H ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)

Tactic:
exact cartanEquivDual_symm_apply_mem_corootSpace α

Premises used: LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
inl : ∀ (hαx : Eq.{u_2 + 1} (α := K) (0 x) 0) (hx : Membership.mem (γ := LieIdeal K ↥H) (corootSpace 0) x), x = 0
inr : ∀ (hα : α ≠ 0), x = 0
⊢ x = 0

Tactic:
rcases eq_or_ne α 0 with rfl | hα

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
x : ↥H
hαx : Eq.{u_2 + 1} (α := K) (0 x) 0
hx : Membership.mem (γ := LieIdeal K ↥H) (corootSpace 0) x
⊢ x = 0

Tactic:
simpa using hx
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
⊢ Membership.mem (γ := Submodule K ↥H) (⨅ (β : Weight K (↥H) L), Weight.ker (M := L) (χ := β)) x

Tactic:
(Submodule.mem_iInf _).mpr fun β ↦ ?_

Premises used: Iff.mpr, Submodule.mem_iInf
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
refine : ∀ (β : Weight K (↥H) L), Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := β)) x
⊢ Membership.mem (γ := Submodule K ↥H) (⨅ (β : Weight K (↥H) L), Weight.ker (M := L) (χ := β)) x

Tactic:
refine (Submodule.mem_iInf _).mpr fun β ↦ ?_

Premises used: Iff.mpr, Submodule.mem_iInf
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
β : Weight K (↥H) L
obtain :
  ∀ (a b : ℤ) (hb : 0 < b) (hab : ∀ x ∈ corootSpace α, (a • α + HSMul.hSMul (β := ↥H → K) b (⇑β : (a : ↥H) → K)) x = 0),
    Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := β)) x
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := β)) x

Tactic:
obtain ⟨a, b, hb, hab⟩ :=
      exists_forall_mem_corootSpace_smul_add_eq_zero L α β hα β.genWeightSpace_ne_bot

Premises used: LieModule.exists_forall_mem_corootSpace_smul_add_eq_zero, LieModule.Weight.genWeightSpace_ne_bot, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
β : Weight K (↥H) L
a b : ℤ
hb : 0 < b
hab : ∀ x ∈ corootSpace α, (a • α + HSMul.hSMul (β := ↥H → K) b (⇑β : (a : ↥H) → K)) x = 0
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := β)) x

Tactic:
simpa [hαx, hb.ne'] using hab _ hx

Premises used: LT.lt.ne'
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hx : x ∈ corootSpace α
hα : α ≠ 0
⊢ Membership.mem (γ := Submodule K ↥H) (⨅ (β : Weight K (↥H) L), Weight.ker (M := L) (χ := β)) x

Tactic:
replace hx : x ∈ ⨅ β : Weight K H L, β.ker := by
    refine (Submodule.mem_iInf _).mpr fun β ↦ ?_
    obtain ⟨a, b, hb, hab⟩ :=
      exists_forall_mem_corootSpace_smul_add_eq_zero L α β hα β.genWeightSpace_ne_bot
    simpa [hαx, hb.ne'] using hab _ hx
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
x : ↥H
α : ↥H → K
hαx : α x = 0
hα : α ≠ 0
hx : Membership.mem (γ := Submodule K ↥H) (⨅ (β : Weight K (↥H) L), Weight.ker (M := L) (χ := β)) x
⊢ x = 0

Tactic:
simpa using hx
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
rw :
  Eq.{u_3 + 1} (α := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    ⊥
⊢ Disjoint.{u_3} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α))
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))

Tactic:
rw [disjoint_iff]

Premises used: disjoint_iff
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    ⊥

Tactic:
(Submodule.eq_bot_iff _).mpr fun x ⟨hαx, hx⟩ ↦ ?_

Premises used: Iff.mpr, _private.0.LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace.match_1, Submodule.eq_bot_iff, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
refine :
  ∀ (x : ↥H),
    Membership.mem (γ := Submodule K ↥H)
        (Weight.ker (M := L) (χ := α) ⊓
          LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
        x →
      ∀ (hαx : x ∈ (↑(Weight.ker (M := L) (χ := α)) : Set ↥H))
        (hx :
          x ∈
            (↑(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) :
              Set ↥H)),
        x = 0
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H)
    (Weight.ker (M := L) (χ := α) ⊓
      LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K))))
    ⊥

Tactic:
refine (Submodule.eq_bot_iff _).mpr fun x ⟨hαx, hx⟩ ↦ ?_