awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
hα : ¬α.IsZero
e : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (-(⇑α : (a : ↥H) → K))) ⊥
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
this : Membership.mem (γ := Submodule K L) ⊥ x
⊢ False

Tactic:
exact x_ne0 this
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
h :
  ∀ (x : ↥H),
    Eq.{u_2 + 1} (α := K)
      ((({
                toFun :=
                  -(⇑({ toFun := -(⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := ⋯ } : Weight K (↥H) L) : (a : ↥H) → K),
                genWeightSpace_ne_bot' := ⋯ } :
              Weight K (↥H) L) :
            (a : ↥H) → K)
          x :
        K)
      ((α : (a : ↥H) → K) x : K)
⊢ { toFun := -(⇑({ toFun := -(⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := ⋯ } : Weight K (↥H) L) : (a : ↥H) → K),
      genWeightSpace_ne_bot' := ⋯ } =
    α

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
inst_6 : IsKilling K L
H : LieSubalgebra K L
inst_7 : H.IsCartanSubalgebra
inst_8 : IsTriangularizable K (↥H) L
α_1 α : Weight K (↥H) L
x : ↥H
⊢ Eq.{u_2 + 1} (α := K)
    ((({ toFun := -(⇑({ toFun := -(⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := ⋯ } : Weight K (↥H) L) : (a : ↥H) → K),
              genWeightSpace_ne_bot' := ⋯ } :
            Weight K (↥H) L) :
          (a : ↥H) → K)
        x :
      K)
    ((α : (a : ↥H) → K) x : K)

Tactic:
simp
-- 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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
⊢ Eq (α := (a : ↥H) → K) (⇑(-α) : (a : ↥H) → K) (-(⇑α : (a : ↥H) → K))

Tactic:
rfl

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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
h₁ : ∀ (x : ↥H), Eq.{u_2 + 1} (α := K) ((-α : (a : ↥H) → K) x : K) (0 x : K)
⊢ (-α).IsZero

Tactic:
ext
-- 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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x : ↥H
h₁ : Eq.{u_2 + 1} (α := K) ((-(⇑α : (a : ↥H) → K)) x : K) (0 x : K)
h₂ : Eq.{u_2 + 1} (α := K) ((-0) x) (0 x)
h₃ h₄ : Eq.{u_2 + 1} (α := K) (0 x) (0 x)
⊢ Eq.{u_2 + 1} (α := K) ((-α : (a : ↥H) → K) x : K) (0 x : K)

Tactic:
rw [coe_neg, h, neg_zero]

Premises used: neg_zero, LieModule.Weight.coe_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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
⊢ (-α).IsZero ↔ α.IsZero

Tactic:
⟨fun h ↦ neg_neg α ▸ h.neg, fun h ↦ h.neg⟩

Premises used: LieModule.Weight.IsZero.neg, Eq.rec, neg_neg, Iff.intro
-- 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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsNonZero
e : (-α).IsZero
⊢ α.IsZero

Tactic:
simpa using e.neg

Premises used: LieModule.Weight.IsZero.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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
⊢ (-α).IsNonZero ↔ α.IsNonZero

Tactic:
isZero_neg.not

Premises used: Iff.not, LieModule.Weight.isZero_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
inst_4 : IsKilling K L
H : LieSubalgebra K L
inst_5 : H.IsCartanSubalgebra
inst_6 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
⊢ toLinear K (↥H) L (-α) = -toLinear K (↥H) L α

Tactic:
rfl

Premises used: LieModule.Weight.toLinear, 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
this :
  Membership.mem (γ := Submodule K ↥H) (LinearMap.ker (traceForm K (↥H) L)) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx = 0

Tactic:
simp only [ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.mem_bot] at this

Premises used: LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.mem_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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
this : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx = 0
⊢ x = 0

Tactic:
(AddSubmonoid.mk_eq_zero H.toAddSubmonoid).mp this

Premises used: Submodule.toAddSubmonoid, Iff.mp, AddSubmonoid.mk_eq_zero, LieSubalgebra.toSubmodule
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
this : Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx = 0
⊢ x = 0

Tactic:
exact (AddSubmonoid.mk_eq_zero H.toAddSubmonoid).mp this

Premises used: Submodule.toAddSubmonoid, Iff.mp, AddSubmonoid.mk_eq_zero, LieSubalgebra.toSubmodule
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
suffices :
  Membership.mem (γ := Submodule K ↥H) (LinearMap.ker (traceForm K (↥H) L)) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx)
⊢ x = 0

Tactic:
suffices ⟨x, hx⟩ ∈ LinearMap.ker (traceForm K H L) by
    simp only [ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.mem_bot] at this
    exact (AddSubmonoid.mk_eq_zero H.toAddSubmonoid).mp this
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
h :
  ∀ (y : ↥H),
    Eq.{u_2 + 1} (α := K)
      ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) :
              LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
            (a : ↥H) → K)
          y :
        K)
      ((0 : (a : ↥H) → K) y : K)
⊢ Eq (α := LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
    ((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) :
      LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)
    (0 : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K)

Tactic:
ext y
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
rw :
  Eq (α := End K L)
    (Bracket.bracket (L := End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
        ((toEnd K (↥H) L : (a : ↥H) → End K L) y) :
      End K L)
    (0 : End K L)
rw₁ :
  Eq (α := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx, y⁆ : End K L)
    (0 : End K L)
rw₂ : Eq (α := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) 0 : End K L) (0 : End K L)
rw₃ rw₄ : Eq.{u_3 + 1} (α := End K L) 0 0
⊢ Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)

Tactic:
rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]

Premises used: LieHom.map_lie, map_zero, trivial_lie_zero, commute_iff_lie_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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
⊢ Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)

Tactic:
have comm : Commute (toEnd K H L ⟨x, hx⟩) (toEnd K H L y) := by
    rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
comm :
  Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
h :
  Eq.{u_2 + 1} (α := K)
    ((LinearMap.trace K L : (a : L →ₗ[K] L) → K)
        (HMul.hMul (α := End K L) (β := End K L)
          ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
          ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)) :
      K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) :
            LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        y :
      K)
    ((0 : (a : ↥H) → K) y : K)

Tactic:
rw [traceForm_apply_apply, ← Module.End.mul_eq_comp, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, Module.End.mul_eq_comp, LieModule.traceForm_apply_apply
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
comm :
  Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
⊢ Eq.{u_2 + 1} (α := K)
    ((LinearMap.trace K L : (a : L →ₗ[K] L) → K)
        (HMul.hMul (α := End K L) (β := End K L)
          ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
          ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)) :
      K)
    (0 : K)

Tactic:
(LinearMap.isNilpotent_trace_of_isNilpotent (comm.isNilpotent_mul_right hx')).eq_zero

Premises used: LinearMap.isNilpotent_trace_of_isNilpotent, IsNilpotent.eq_zero, Commute.isNilpotent_mul_right
-- 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
x : L
hx : x ∈ H
hx' : _root_.IsNilpotent (R := End K L) ((ad K L : (a : L) → End K L) x : End K L)
y : ↥H
comm :
  Commute (S := End K L) ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
    ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)
⊢ Eq.{u_2 + 1} (α := K)
    ((LinearMap.trace K L : (a : L →ₗ[K] L) → K)
        (HMul.hMul (α := End K L) (β := End K L)
          ((toEnd K (↥H) L : (a : ↥H) → End K L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) x hx) : End K L)
          ((toEnd K (↥H) L : (a : ↥H) → End K L) y : End K L)) :
      K)
    (0 : K)

Tactic:
exact (LinearMap.isNilpotent_trace_of_isNilpotent (comm.isNilpotent_mul_right hx')).eq_zero

Premises used: LinearMap.isNilpotent_trace_of_isNilpotent, IsNilpotent.eq_zero, Commute.isNilpotent_mul_right
-- 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
⊢ Eq.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace 0) ⊥

Tactic:
eq_bot_iff.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, eq_bot_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
refine :
  ∀ (x : ↥H) (hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x),
    Membership.mem (γ := LieSubmodule K ↥H ↥H) ⊥ x
⊢ Eq.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace 0) ⊥

Tactic:
refine eq_bot_iff.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, eq_bot_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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
this : Eq (α := Set L) {x : L | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} {0}
⊢ Membership.mem (γ := LieSubmodule K ↥H ↥H) ⊥ x

Tactic:
simpa [mem_corootSpace, this] using hx

Premises used: 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
suffices : Eq (α := Set L) {x : L | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} {0}
⊢ Membership.mem (γ := LieSubmodule K ↥H ↥H) ⊥ x

Tactic:
suffices {x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} = {0} by simpa [mem_corootSpace, this] 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
⊢ Eq (α := Set L) {x : L | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} {0}

Tactic:
eq_singleton_iff_unique_mem.mpr ⟨⟨0, H.zero_mem, 0, H.zero_mem, zero_lie 0⟩, ?_⟩

Premises used: Iff.mpr, And.intro, zero_lie, Exists.intro, LieSubalgebra.zero_mem, Set.eq_singleton_iff_unique_mem, OfNat.ofNat
-- 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
refine : ∀ (x : L), Membership.mem (γ := Set L) {x : L | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} x → x = 0
⊢ Eq (α := Set L) {x : L | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} {0}

Tactic:
refine eq_singleton_iff_unique_mem.mpr ⟨⟨0, H.zero_mem, 0, H.zero_mem, zero_lie 0⟩, ?_⟩
-- 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
y : L
hy : y ∈ H
z : L
hz : z ∈ H
this : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz⁆ = 0
⊢ ⁅y, z⁆ = 0

Tactic:
simpa only [Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero] using this

Premises used: Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero
-- 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
y : L
hy : y ∈ H
z : L
hz : z ∈ H
suffices : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz⁆ = 0
⊢ ⁅y, z⁆ = 0

Tactic:
suffices ⁅(⟨y, hy⟩ : H), (⟨z, hz⟩ : H)⁆ = 0 by
    simpa only [Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero] using this
-- 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
x : ↥H
hx : Membership.mem (γ := LieSubmodule K ↥H ↥H) (corootSpace 0) x
y : L
hy : y ∈ H
z : L
hz : z ∈ H
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz⁆ = 0

Tactic:
simp [trivial_lie_zero]

Premises used: trivial_lie_zero
-- 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
α : Weight K (↥H) L
x : ↥H
rw : Eq.{u_2 + 1} (α := K) ((Weight.toLinear K (↥H) L α : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
rw₁ rw₂ : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
⊢ Eq.{u_2 + 1} (α := K)
    ((((cartanEquivDual H : (a : ↥H) → Dual K ↥H)
              (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
            Dual.{u_2, u_3} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
    ((α : (a : ↥H) → K) x : K)

Tactic:
rw [LinearEquiv.apply_symm_apply, Weight.toLinear_apply]

Premises used: LinearEquiv.apply_symm_apply, LieModule.Weight.toLinear_apply
-- 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
α : Weight K (↥H) L
x : ↥H
⊢ Eq.{u_2 + 1} (α := K)
    ((((cartanEquivDual H : (a : ↥H) → Dual K ↥H)
              (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
            Dual.{u_2, u_3} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
    ((α : (a : ↥H) → K) x : K)

Tactic:
have : cartanEquivDual H ((cartanEquivDual H).symm α) x = α x := by
    rw [LinearEquiv.apply_symm_apply, Weight.toLinear_apply]
-- 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
α : Weight K (↥H) L
x : ↥H
this :
  Eq.{u_2 + 1} (α := K)
    ((((cartanEquivDual H : (a : ↥H) → Dual K ↥H)
              (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
            Dual.{u_2, u_3} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
    ((α : (a : ↥H) → K) x : K)
rw :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := K) (β := K)
        (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ :
          K)
        ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K)
                  (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
                LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
              (a : ↥H) → K)
            x :
          K)) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := K) (β := K)
        (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ :
          K)
        ((α : (a : ↥H) → K) x : K))
⊢ (((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) (coroot α) : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
        (a : ↥H) → K)
      x =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := K) (β := K)
        (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ :
          K)
        ((α : (a : ↥H) → K) x : K))

Tactic:
rw [coroot, map_nsmul, map_smul, LinearMap.smul_apply, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, LieAlgebra.IsKilling.coroot, map_nsmul, map_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
α : Weight K (↥H) L
x : ↥H
this :
  Eq.{u_2 + 1} (α := K)
    ((((cartanEquivDual H : (a : ↥H) → Dual K ↥H)
              (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
            Dual.{u_2, u_3} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
    ((α : (a : ↥H) → K) x : K)
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := K) (β := K)
        (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ :
          K)
        ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K)
                  (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α)) :
                LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
              (a : ↥H) → K)
            x :
          K)) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := K) (β := K)
        (((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H))⁻¹ :
          K)
        ((α : (a : ↥H) → K) x : K))

Tactic:
congr 2
-- 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
⊢ coroot (-α) = -coroot α

Tactic:
simp [coroot]

Premises used: LieAlgebra.IsKilling.coroot