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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
set :
  let α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α);
  ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑α' : L)
⊢ ⁅e, f⁆ =
    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:
set α' := (cartanEquivDual H).symm α

Premises used: LinearEquiv.symm, Membership.mem, Subtype, LieModule.Weight.toLinear, LieAlgebra.IsKilling.cartanEquivDual, 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
rw :
  Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K L))
    (⁅e, f⁆ -
      HSMul.hSMul.{u_2, u_3, u_3} (α := K)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L))
⊢ ⁅e, f⁆ =
    HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K)
      (↑α' : L)

Tactic:
rw [← sub_eq_zero, ← Submodule.mem_bot (R := K), ← ker_killingForm_eq_bot]

Premises used: sub_eq_zero, Submodule.mem_bot, LieAlgebra.IsKilling.ker_killingForm_eq_bot
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hx :
  ⁅e, f⁆ -
      HSMul.hSMul.{u_2, u_3, u_3} (α := K)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L) ∈
    rootSpace H 0
hx' :
  ∀ y ∈ rootSpace H (-0),
    Eq.{u_2 + 1} (α := K)
      ((((killingForm K L : (a : L) → L →ₗ[K] K)
                (⁅e, f⁆ -
                  HSMul.hSMul.{u_2, u_3, u_3} (α := K)
                    ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L)) :
              L →ₗ[K] K) :
            (a : L) → K)
          y :
        K)
      (0 : K)
⊢ Membership.mem (γ := Submodule K L) (LinearMap.ker (killingForm K L))
    (⁅e, f⁆ -
      HSMul.hSMul.{u_2, u_3, u_3} (α := K)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L))

Tactic:
apply mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg (α := (0 : H → K))

Premises used: LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hx :
  ⁅e, f⁆ -
      HSMul.hSMul.{u_2, u_3, u_3} (α := K)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L) ∈
    H
⊢ ⁅e, f⁆ -
      HSMul.hSMul.{u_2, u_3, u_3} (α := K)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L) ∈
    rootSpace H 0

Tactic:
simp only [rootSpace_zero_eq, LieSubalgebra.mem_toLieSubmodule]

Premises used: LieSubalgebra.mem_toLieSubmodule, LieAlgebra.rootSpace_zero_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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ -
      HSMul.hSMul.{u_2, u_3, u_3} (α := K)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L) ∈
    H

Tactic:
sub_mem ?_ (H.smul_mem _ α'.property)

Premises used: sub_mem, LieSubalgebra.smul_mem, Subtype.property
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
hx : ⁅e, f⁆ ∈ H
⊢ ⁅e, f⁆ -
      HSMul.hSMul.{u_2, u_3, u_3} (α := K)
        ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L) ∈
    H

Tactic:
refine sub_mem ?_ (H.smul_mem _ α'.property)

Premises used: sub_mem, LieSubalgebra.smul_mem, Subtype.property
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
⊢ ⁅e, f⁆ ∈ H

Tactic:
simpa using mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α (-α) heα hfα

Premises used: LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, DFunLike.coe, Neg.neg
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
z : L
hz : z ∈ rootSpace H (-0)
⊢ z ∈ H

Tactic:
simpa using hz
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
z : L
hz : z ∈ rootSpace H (-0)
⊢ z ∈ H

Tactic:
replace hz : z ∈ H := by simpa using hz
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
z : L
hz : z ∈ H
⊢ ⁅z, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : K) e

Tactic:
have he : ⁅z, e⁆ = α ⟨z, hz⟩ • e := aux ⟨z, hz⟩
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
z : L
hz : z ∈ H
he :
  ⁅z, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : K) e
⊢ Eq.{u_2 + 1} (α := K)
    ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑α' : L) : L →ₗ[K] K) : (a : L) → K)
        (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : L) :
      K)
    ((α : (a : ↥H) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : K)

Tactic:
have hαz : killingForm K L α' (⟨z, hz⟩ : H) = α ⟨z, hz⟩ :=
      LinearMap.BilinForm.apply_toDual_symm_apply (hB := traceForm_cartan_nondegenerate K L H) _ _
-- 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
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
aux : ∀ (h : ↥H), ⁅h, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
α' : ↥H := ((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)
z : L
hz : z ∈ H
he :
  ⁅z, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : K) e
hαz :
  Eq.{u_2 + 1} (α := K)
    ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑α' : L) : L →ₗ[K] K) : (a : L) → K)
        (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : L) :
      K)
    ((α : (a : ↥H) → K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz) : K)
⊢ Eq.{u_2 + 1} (α := K)
    ((((killingForm K L : (a : L) → L →ₗ[K] K)
              (⁅e, f⁆ -
                HSMul.hSMul.{u_2, u_3, u_3} (α := K)
                  ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (↑α' : L)) :
            L →ₗ[K] K) :
          (a : L) → K)
        z :
      K)
    (0 : K)

Tactic:
simp [traceForm_comm K L L ⁅e, f⁆, ← traceForm_apply_lie_apply, he, mul_comm _ (α ⟨z, hz⟩), hαz]

Premises used: Bracket.bracket, LieModule.traceForm_comm, Subtype.mk, mul_comm, LieModule.traceForm_apply_lie_apply, 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
α : Weight K (↥H) L
obtain :
  ∀ (e : L) (he₀ : e ≠ 0) (he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e),
    Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
      (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)

Tactic:
obtain ⟨e : L, he₀ : e ≠ 0, he : ∀ x, ⁅x, e⁆ = α x • e⟩ := exists_forall_lie_eq_smul K H L α

Premises used: Membership.mem, Subtype, LieModule.exists_forall_lie_eq_smul
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
x : ↥H
⊢ Eq (α := L)
    ((HPow.hPow (β := ℕ)
            (HSub.hSub (α := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) x : End K L)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := K) (β := End K L) ((α : (a : ↥H) → K) x : K) 1))
            1 :
          (a : L) → L)
        e :
      L)
    (0 : L)

Tactic:
simp [← he x]
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
⊢ e ∈ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
have heα : e ∈ rootSpace H α := (mem_genWeightSpace L α e).mpr fun x ↦ ⟨1, by simp [← he x]⟩
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
contrapose! :
  ∀
    (he₀ :
      ∀ (f : L) (_ : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
        Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)),
    e = 0
⊢ ∃ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)),
    Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)

Tactic:
contrapose! he₀
-- 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
α : Weight K (↥H) L
e : L
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
he₀ :
  ∀ (f : L) (_ : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
    Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
⊢ e = 0

Tactic:
simpa using mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H heα he₀

Premises used: LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
obtain :
  ∀ (f : L) (hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
    (hf :
      Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)),
    Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
      (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)

Tactic:
obtain ⟨f, hfα, hf⟩ : ∃ f ∈ rootSpace H (-α), killingForm K L e f ≠ 0 := by
    contrapose! he₀
    simpa using mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg K L H heα he₀

Premises used: LieAlgebra.rootSpace, DFunLike.coe, Neg.neg
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
f : L
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf : Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
this :
  ⁅e, f⁆ =
    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)
⊢ ⁅HSMul.hSMul.{u_2, u_3, u_3} (α := K)
        (((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f)⁻¹ : K) e,
      f⁆ =
    (↑(((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) : L)

Tactic:
simpa [inv_smul_eq_iff₀ hf]

Premises used: inv_smul_eq_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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
f : L
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf : Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
suffices :
  ⁅e, f⁆ =
    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)
⊢ Membership.mem.{u_3, u_3} (α := ↥H) (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K))
    (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H)

Tactic:
suffices ⁅e, f⁆ = killingForm K L e f • ((cartanEquivDual H).symm α : L) from
    (mem_corootSpace α).mpr <| Submodule.subset_span ⟨(killingForm K L e f)⁻¹ • e,
      Submodule.smul_mem _ _ heα, f, hfα, by simpa [inv_smul_eq_iff₀ hf]⟩
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
f : L
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf : Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
⊢ ⁅e, f⁆ =
    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:
lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux heα hfα he

Premises used: LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux
-- 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
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) e
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
f : L
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf : Ne.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) e : L →ₗ[K] K) : (a : L) → K) f : K) (0 : K)
⊢ ⁅e, f⁆ =
    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 lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux heα hfα he

Premises used: LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux
-- 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
α : Weight K (↥H) L
⊢ Membership.mem (γ := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) (coroot α)

Tactic:
nsmul_mem (Submodule.smul_mem _ _ <| cartanEquivDual_symm_apply_mem_corootSpace α) _

Premises used: Set.Mem, LieAlgebra.IsKilling.coroot, nsmul_mem, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, Submodule.smul_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
⊢ Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L))) ⊤

Tactic:
eq_top_iff.mpr (le_trans ?_ (LieModule.range_traceForm_le_span_weight K H L))

Premises used: Iff.mpr, eq_top_iff, Membership.mem, Subtype, LieModule.range_traceForm_le_span_weight, le_trans
-- 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
refine :
  LE.le (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)) ⊤
    (LinearMap.range (traceForm K (↥H) L))
⊢ Eq (α := Submodule K (LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K))
    (span K (range (ι := Weight K (↥H) L) (Weight.toLinear K (↥H) L))) ⊤

Tactic:
refine eq_top_iff.mpr (le_trans ?_ (LieModule.range_traceForm_le_span_weight K H L))

Premises used: Iff.mpr, eq_top_iff, Membership.mem, Subtype, LieModule.range_traceForm_le_span_weight, le_trans