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 : CharZero K
α : Weight K (↥H) L
h₀ : ¬α.IsZero
t : K
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (t • coroot α) : K) (2 : K)
h_mem : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) (t • coroot α)
this : t = 1
⊢ t • coroot α = coroot α

Tactic:
simp [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
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
h₀ : ¬α.IsZero
t : K
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (t • coroot α) : K) (2 : K)
h_mem : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) (t • coroot α)
neg : t = 1
⊢ t • coroot α = coroot α

Tactic:
suffices t = 1 by simp [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
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
h₀ : ¬α.IsZero
t : K
h_two : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) (t • coroot α) : K) (2 : K)
h_mem : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) (t • coroot α)
⊢ t = 1

Tactic:
simpa [root_apply_coroot h₀] using h_two

Premises used: LieAlgebra.IsKilling.root_apply_coroot
-- 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} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥ ↔ α.IsZero

Tactic:
simp [← LieSubmodule.toSubmodule_eq_bot, coe_corootSpace_eq_span_singleton α]

Premises used: LieSubmodule.toSubmodule_eq_bot, LieAlgebra.IsKilling.coe_corootSpace_eq_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 : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
⊢ IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)

Tactic:
simpa [Weight.coe_toLinear_eq_zero_iff.mpr hα, coroot_eq_zero_iff.mpr hα, Weight.ker]
      using isCompl_top_bot

Premises used: Iff.mpr, LieModule.Weight.coe_toLinear_eq_zero_iff, LieModule.Weight.ker, LieAlgebra.IsKilling.coroot_eq_zero_iff, isCompl_top_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
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
rw :
  IsCompl.{u_3} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α))
    (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)
⊢ IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)

Tactic:
rw [← coe_corootSpace_eq_span_singleton]

Premises used: LieAlgebra.IsKilling.coe_corootSpace_eq_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 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ Weight.toLinear K (↥H) L α ≠ 0

Tactic:
simp_all
-- 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
hα : ¬α.IsZero
apply :
  Ne.{u_3 + 1} (α := Submodule K ↥H)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
⊢ IsCompl.{u_3} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α))
    (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H)

Tactic:
apply Module.Dual.isCompl_ker_of_disjoint_of_ne_bot (by simp_all)
      (disjoint_ker_weight_corootSpace α)

Premises used: Module.Dual.isCompl_ker_of_disjoint_of_ne_bot, LieAlgebra.IsKilling.disjoint_ker_weight_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
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ Ne.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥

Tactic:
simpa using 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
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ Ne.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥

Tactic:
replace hα : corootSpace α ≠ ⊥ := by simpa using 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
inst_7 : CharZero K
α : Weight K (↥H) L
hα : Ne.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥
rwa :
  ∀ (hα : ¬Eq.{u_3 + 1} (α := LieIdeal K ↥H) (corootSpace (⇑α : (a : ↥H) → K)) ⊥),
    Ne.{u_3 + 1} (α := Submodule K ↥H)
      (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hα :
      ¬Eq.{u_3 + 1} (α := Submodule K ↥H) (↑(corootSpace (⇑α : (a : ↥H) → K)) : Submodule K ↥H) (↑⊥ : Submodule K ↥H)),
    Ne.{u_3 + 1} (α := Submodule K ↥H)
      (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥
⊢ Ne.{u_3 + 1} (α := Submodule K ↥H)
    (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra K (↥H) (corootSpace (⇑α : (a : ↥H) → K)))) ⊥

Tactic:
rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at hα

Premises used: LieSubmodule.toSubmodule_inj, ne_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
if : ∀ (hα : α.IsZero), IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
if₁ : ∀ (hα : ¬α.IsZero), IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
if₂ : ∀ (hα : α.IsZero), IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
if₃ if₄ : ∀ (hα : ¬α.IsZero), IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)
⊢ IsCompl (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) (K ∙ coroot α)

Tactic:
if hα : α.IsZero then
    simpa [Weight.coe_toLinear_eq_zero_iff.mpr hα, coroot_eq_zero_iff.mpr hα, Weight.ker]
      using isCompl_top_bot
  else
    rw [← coe_corootSpace_eq_span_singleton]
    apply Module.Dual.isCompl_ker_of_disjoint_of_ne_bot (by simp_all)
      (disjoint_ker_weight_corootSpace α)
    replace hα : corootSpace α ≠ ⊥ := by simpa using hα
    rwa [ne_eq, ← LieSubmodule.toSubmodule_inj] at hα

Premises used: Module.Dual.isCompl_ker_of_disjoint_of_ne_bot, LieModule.Weight.IsZero, LieSubmodule.toSubmodule_inj, ne_eq, LieModule.Weight.ker, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, isCompl_top_bot, LieAlgebra.IsKilling.coe_corootSpace_eq_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 : CharZero K
α : Weight K (↥H) L
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
z : ↥H
hz :
  Membership.mem (γ := Set ↥H)
    {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)} z
mem :
  ∀ (u : L) (hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)) (v : L) (huv : ⁅u, v⁆ = (↑z : L)),
    Eq.{u_2 + 1} (α := K)
      ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
            (a : ↥H) → K)
          z :
        K)
      (0 : K)
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        z :
      K)
    (0 : K)

Tactic:
obtain ⟨u, hu, v, -, huv⟩ := 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
inst_7 : CharZero K
α : Weight K (↥H) L
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
mem :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        z :
      K)
    (0 : K)

Tactic:
change killingForm K L (x : L) (z : L) = 0

Premises used: killingForm, Subtype.val, 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
α : Weight K (↥H) L
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
⊢ Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)

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
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
⊢ Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)

Tactic:
replace hx : α x = 0 := by 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
x y z : ↥H
u : L
hu : u ∈ rootSpace H (⇑α : (a : ↥H) → K)
v : L
huv : ⁅u, v⁆ = (↑z : L)
hx : Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
mem :
  Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) ⁅u, v⁆ : K)
    (0 : K)
mem₁ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅(↑x : L), u⁆ : L →ₗ[K] K) : (a : L) → K) v : K)
    (0 : K)
mem₂ :
  Eq.{u_2 + 1} (α := K) ((((traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, u⁆ : L →ₗ[K] K) : (a : L) → K) v : K) (0 : K)
mem₃ :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K L L : (a : L) → L →ₗ[K] K) (HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) x : K) u) :
            L →ₗ[K] K) :
          (a : L) → K)
        v :
      K)
    (0 : K)
mem₄ :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K L L : (a : L) → L →ₗ[K] K) (HSMul.hSMul.{u_2, u_3, u_3} (α := K) 0 u) : L →ₗ[K] K) : (a : L) → K)
        v :
      K)
    (0 : K)
mem₅ : Eq.{u_2 + 1} (α := K) (((traceForm K L L : (a : L) → L →ₗ[K] K) 0 : (a : L) → K) v : K) (0 : K)
mem₆ : Eq.{u_2 + 1} (α := K) ((0 : (a : L) → K) v : K) (0 : K)
mem₇ mem₈ : Eq.{u_2 + 1} (α := K) 0 0
⊢ Eq.{u_2 + 1} (α := K) ((((killingForm K L : (a : L) → L →ₗ[K] K) (↑x : L) : L →ₗ[K] K) : (a : L) → K) (↑z : L) : K)
    (0 : K)

Tactic:
rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module,
      lie_eq_smul_of_mem_rootSpace hu, hx, zero_smul, map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, LieSubalgebra.coe_bracket_of_module, map_zero, LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace, zero_smul, LieModule.traceForm_apply_lie_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
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        0 :
      K)
    (0 : 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
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
x y : ↥H
hx_1 : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
x_1 y_1 : ↥H
hx_2 :
  Membership.mem (γ := Submodule K ↥H)
    (span K
      {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
    x_1
hy_1 :
  Membership.mem (γ := Submodule K ↥H)
    (span K
      {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
    y_1
hx :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        x_1 :
      K)
    (0 : K)
hy :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        y_1 :
      K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        (x_1 + y_1) :
      K)
    (0 : K)

Tactic:
simp [hx, hy]
-- 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
x y : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
a : K
x_1 : ↥H
hx_1 :
  Membership.mem (γ := Submodule K ↥H)
    (span K
      {x : ↥H | ∃ y ∈ rootSpace H (⇑α : (a : ↥H) → K), ∃ z ∈ rootSpace H (-(⇑α : (a : ↥H) → K)), ⁅y, z⁆ = (↑x : L)})
    x_1
hz :
  Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        x_1 :
      K)
    (0 : K)
⊢ Eq.{u_2 + 1} (α := K)
    ((((traceForm K (↥H) L : (a : ↥H) → ↥H →ₗ[K] K) x : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        (a • x_1) :
      K)
    (0 : K)

Tactic:
simp [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
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
⊢ coroot α = 0

Tactic:
simpa
-- 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
hα : α.IsZero
⊢ coroot α = 0

Tactic:
have hα' : coroot α = 0 := by simpa
-- 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
hα : α.IsZero
hα' : coroot α = 0
h :
  ∀ (x : ↥H),
    Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x ↔ Membership.mem (γ := Submodule K ↥H) ⊤ x
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) ⊤

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
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
hα : α.IsZero
hα' : coroot α = 0
x : ↥H
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x ↔ Membership.mem (γ := Submodule K ↥H) ⊤ x

Tactic:
simp [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
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
hα' : coroot α = 0
⊢ Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) ⊤

Tactic:
replace hα : α.ker = ⊤ := by ext; simp [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
inst_7 : CharZero K
α : Weight K (↥H) L
hα' : coroot α = 0
hα : Eq.{u_3 + 1} (α := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) ⊤
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))

Tactic:
simp [hα, 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
inst_7 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))

Tactic:
le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)

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 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
refine_1 :
  ∀ (x : ↥H)
    (hx : Membership.mem (γ := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α)) x),
    Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x
refine_2 :
  ∀ (x : ↥H) (hx : Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x) (y : ↥H)
    (hy : Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) y), LinearMap.IsOrtho (traceForm K (↥H) L) y x
⊢ Eq (α := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α))
    (Weight.ker (M := L) (χ := α))

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)

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 : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
x : ↥H
hx : Membership.mem (γ := Submodule K ↥H) (LinearMap.BilinForm.orthogonal (traceForm K (↥H) L) (K ∙ coroot α)) x
⊢ ∀ (n : ↥H),
    Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) n → LinearMap.BilinForm.IsOrtho (traceForm K (↥H) L) n x

Tactic:
simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx

Premises used: LinearMap.BilinForm.mem_orthogonal_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
hα : ¬α.IsZero
x : ↥H
hx :
  ∀ (n : ↥H),
    Membership.mem (γ := Submodule K ↥H) (K ∙ coroot α) n → LinearMap.BilinForm.IsOrtho (traceForm K (↥H) L) n x
⊢ LinearMap.BilinForm.IsOrtho (traceForm K (↥H) L) (coroot α) x

Tactic:
specialize hx (coroot α) (Submodule.mem_span_singleton_self _)

Premises used: LieAlgebra.IsKilling.coroot, Submodule.mem_span_singleton_self
-- 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
hα : ¬α.IsZero
x : ↥H
hx : LinearMap.BilinForm.IsOrtho (traceForm K (↥H) L) (coroot α) x
⊢ Eq.{u_2 + 1} (α := K)
      ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
      (0 : K) ∨
    Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)

Tactic:
simp only [LinearMap.BilinForm.isOrtho_def, traceForm_coroot, smul_eq_mul, nsmul_eq_mul,
        Nat.cast_ofNat, mul_eq_zero, OfNat.ofNat_ne_zero, inv_eq_zero, false_or] at hx

Premises used: inv_eq_zero, Nat.cast_ofNat, OfNat.ofNat_ne_zero, false_or, mul_eq_zero, nsmul_eq_mul, LieAlgebra.IsKilling.traceForm_coroot, smul_eq_mul, LinearMap.BilinForm.isOrtho_def
-- 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
hα : ¬α.IsZero
x : ↥H
hx :
  Eq.{u_2 + 1} (α := K)
      ((α : (a : ↥H) → K) (((cartanEquivDual H).symm : (a : Dual K ↥H) → ↥H) (Weight.toLinear K (↥H) L α) : ↥H) : K)
      (0 : K) ∨
    Eq.{u_2 + 1} (α := K) ((α : (a : ↥H) → K) x : K) (0 : K)
⊢ Membership.mem (γ := Submodule K ↥H) (Weight.ker (M := L) (χ := α)) x

Tactic:
simpa using hx.resolve_left (root_apply_cartanEquivDual_symm_ne_zero hα)

Premises used: Or.resolve_left, LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero