awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
h :
  Eq (α := Set (Dual.{u_1, u_2} K ↥H))
    (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑{
            toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
              Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
            inj' := ⋯ } :
        (a : ↥LieSubalgebra.root) → Dual K ↥H))
    (Set.image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero})
⊢ Eq (α := Submodule K (Dual.{u_1, u_2} K ↥H))
    (Submodule.span K
      (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑{
              toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
                Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
              inj' := ⋯ } :
          (a : ↥LieSubalgebra.root) → Dual K ↥H)))
    ⊤

Tactic:
convert! span_weight_isNonZero_eq_top K L H

Premises used: LieAlgebra.IsKilling.span_weight_isNonZero_eq_top
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
h :
  ∀ (x : Dual.{u_1, u_2} K ↥H),
    Membership.mem (γ := Set (Dual.{u_1, u_2} K ↥H))
        (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
          (⇑{
                toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
                  Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
                inj' := ⋯ } :
            (a : ↥LieSubalgebra.root) → Dual K ↥H))
        x ↔
      Membership.mem (γ := Set (Dual.{u_1, u_2} K ↥H))
        (Set.image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}) x
⊢ Eq (α := Set (Dual.{u_1, u_2} K ↥H))
    (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑{
            toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
              Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
            inj' := ⋯ } :
        (a : ↥LieSubalgebra.root) → Dual K ↥H))
    (Set.image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero})

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : Dual.{u_1, u_2} K ↥H
⊢ Membership.mem (γ := Set (Dual.{u_1, u_2} K ↥H))
      (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑{
              toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
                Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
              inj' := ⋯ } :
          (a : ↥LieSubalgebra.root) → Dual K ↥H))
      x ↔
    Membership.mem (γ := Set (Dual.{u_1, u_2} K ↥H))
      (Set.image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero}) x

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 : Weight K (↥H) L
α β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ Eq.{u_1 + 1} (α := K)
    ((↑(HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) (↑α : Weight K (↥H) L)) : ℤ)
            (↑(chainTopCoeff (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) (↑α : Weight K (↥H) L)) : ℤ)) :
        K) :
      K)
    ((((LinearMap.id : (a : Dual K ↥H) → ↥H →ₗ[K] K)
              (({
                    toFun := fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦
                      Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L),
                    inj' := ⋯ } :
                  (a : ↥LieSubalgebra.root) → Dual K ↥H)
                α) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        ((({
                  toFun :=
                    Function.comp (β := Weight K (↥H) L) (coroot : (α : Weight K (↥H) L) → ↥H)
                      (Subtype.val (p := fun (x : Weight K (↥H) L) ↦
                          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L))
                            x) :
                        (self : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) → Weight K (↥H) L),
                  inj' := ⋯ } :
                ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)) ↪ ↥H) :
              (a : ↥LieSubalgebra.root) → ↥H)
            β :
          ↥H) :
      K)

Tactic:
simp [apply_coroot_eq_cast β.1 α.1]

Premises used: LieAlgebra.IsKilling.apply_coroot_eq_cast, Subtype.val
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
rw :
  RootPairing.RootForm (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (RootPairing.flip (rootSystem H)) =
    ∑ i : ↥LieSubalgebra.root,
      (Weight.toLinear K (↥H) L (↑i : Weight K (↥H) L)).smulRight (Weight.toLinear K (↥H) L (↑i : Weight K (↥H) L))
⊢ RootPairing.CorootForm (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) =
    LinearMap.BilinForm.restrict (killingForm K L) H.toSubmodule

Tactic:
rw [restrict_killingForm_eq_sum, RootPairing.CorootForm, ← Finset.sum_coe_sort (s := H.root)]

Premises used: LieAlgebra.IsKilling.restrict_killingForm_eq_sum, RootPairing.CorootForm, LieSubalgebra.root, Finset.sum_coe_sort
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
⊢ RootPairing.RootForm (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (RootPairing.flip (rootSystem H)) =
    ∑ i : ↥LieSubalgebra.root,
      (Weight.toLinear K (↥H) L (↑i : Weight K (↥H) L)).smulRight (Weight.toLinear K (↥H) L (↑i : Weight K (↥H) L))

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
f : Dual.{u_1, u_2} K ↥H
x : ↥H
⊢ Eq.{u_1 + 1} (α := K)
    ((((RootPairing.toLinearMap (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) :
                (a : Dual K ↥H) → ↥H →ₗ[K] K)
              f :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id K) (↥H) K) :
          (a : ↥H) → K)
        x :
      K)
    ((f : (a : ↥H) → K) x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ RootPairing.pairing (rootSystem H) β α = ((↑β : Weight K (↥H) L) : (a : ↥H) → K) (coroot (↑α : Weight K (↥H) L))

Tactic:
rfl

Premises used: RootPairing.pairing, LieAlgebra.IsKilling.coroot, rfl
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ (RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H) α =
    Weight.toLinear K (↥H) L (↑α : Weight K (↥H) L)

Tactic:
rfl

Premises used: LieModule.Weight.toLinear, rfl
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ (RootPairing.coroot (rootSystem H) : (a : ↥LieSubalgebra.root) → ↥H) α = coroot (↑α : Weight K (↥H) L)

Tactic:
rfl

Premises used: LieAlgebra.IsKilling.coroot, rfl
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
simp :
  Eq.{u_2 + 1} (α := Submodule K ↥H) (Submodule.span K (⋃ (i : Weight K (↥H) L), ⋃ (_ : i.IsNonZero), {coroot i}))
    (Submodule.span K
      (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑(RootPairing.coroot (rootSystem H)) : (a : ↥LieSubalgebra.root) → ↥H)))
⊢ Eq.{u_2 + 1} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K)) ⊤

Tactic:
simp only [← toSubmodule_inj, top_toSubmodule, iSup_toSubmodule,
    ← RootPairing.IsRootSystem.span_coroot_eq_top (P := rootSystem H),
    coe_corootSpace_eq_span_singleton, Submodule.iSup_span]

Premises used: LieSubmodule.iSup_toSubmodule, Submodule.iSup_span, LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj, RootPairing.IsRootSystem.span_coroot_eq_top, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
e_s :
  Eq.{u_2 + 1} (α := Set ↥H) (⋃ (i : Weight K (↥H) L), ⋃ (_ : i.IsNonZero), {coroot i})
    (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
      (⇑(RootPairing.coroot (rootSystem H)) : (a : ↥LieSubalgebra.root) → ↥H))
⊢ Eq.{u_2 + 1} (α := Submodule K ↥H) (Submodule.span K (⋃ (i : Weight K (↥H) L), ⋃ (_ : i.IsNonZero), {coroot i}))
    (Submodule.span K
      (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑(RootPairing.coroot (rootSystem H)) : (a : ↥LieSubalgebra.root) → ↥H)))

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : ↥H
⊢ Membership.mem (γ := Set ↥H) (⋃ (i : Weight K (↥H) L), ⋃ (_ : i.IsNonZero), {coroot i}) α ↔
    Membership.mem (γ := Set ↥H)
      (Set.range (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L)))
        (⇑(RootPairing.coroot (rootSystem H)) : (a : ↥LieSubalgebra.root) → ↥H))
      α

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
this :
  Eq.{u_2 + 1} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K)) ⊤
⊢ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSubmodule α ≤ H.toLieSubmodule

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
this :
  Eq.{u_2 + 1} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K)) ⊤
⊢ H.toLieSubmodule ≤ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSubmodule α

Tactic:
simp [← LieSubmodule.map_iSup, this]

Premises used: LieSubmodule.map_iSup
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
suffices :
  Eq.{u_2 + 1} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K)) ⊤
⊢ ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSubmodule α = H.toLieSubmodule

Tactic:
suffices ⨆ α : Weight K H L, ⨆ (_ : α.IsNonZero), corootSpace α = ⊤ from
    le_antisymm (by simp) (by simp [← LieSubmodule.map_iSup, this])
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
⊢ Eq.{u_2 + 1} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K)) ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 : Weight K (↥H) L
α β : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))
⊢ (algebraMap ℤ K : (a : ℤ) → K)
      (HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) (↑α : Weight K (↥H) L)) : ℤ)
        (↑(chainTopCoeff (⇑(↑β : Weight K (↥H) L) : (a : ↥H) → K) (↑α : Weight K (↥H) L)) : ℤ)) =
    RootPairing.pairing (rootSystem H) α β

Tactic:
simp [apply_coroot_eq_cast β.1 α.1]

Premises used: LieAlgebra.IsKilling.apply_coroot_eq_cast, Subtype.val
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
e :
  ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Dual.{u_1, u_2} K ↥H)
      (![(RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
            (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
              Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα),
          (RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
            (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
              Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ)] :
        Fin (Nat.succ 0).succ → Dual.{u_1, u_2} K ↥H)
⊢ ∃ (x : K),
    ¬HSMul.hSMul (β := Dual.{u_1, u_2} K ↥H) x
          ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
              (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                hα) :
            Dual.{u_1, u_2} K ↥H) ≠
        (RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ)

Tactic:
rw [LinearIndependent.pair_iff' ((rootSystem H).ne_zero _), not_forall] at e

Premises used: LieAlgebra.IsKilling.rootSystem, RootPairing.ne_zero, LinearIndependent.pair_iff', Classical.not_forall
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
e :
  ∃ (x : K),
    ¬HSMul.hSMul (β := Dual.{u_1, u_2} K ↥H) x
          ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
              (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                hα) :
            Dual.{u_1, u_2} K ↥H) ≠
        (RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ)
⊢ ∃ (x : K), x • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β

Tactic:
simp only [rootSystem_root_apply, ne_eq, not_not] at e

Premises used: Classical.not_not, ne_eq, LieAlgebra.IsKilling.rootSystem_root_apply
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
⊢ β.IsNonZero

Tactic:
simpa using hβ
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : ∀ (x : ↥H), (β : (a : ↥H) → K) x = HSMul.hSMul (β := (a : ↥H) → K) u (⇑α : (a : ↥H) → K) x
⊢ (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) u (⇑α : (a : ↥H) → K)

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
x : ↥H
⊢ (β : (a : ↥H) → K) x = HSMul.hSMul (β := (a : ↥H) → K) u (⇑α : (a : ↥H) → K) x

Tactic:
DFunLike.congr_fun hu.symm x

Premises used: DFunLike.congr_fun, Eq.symm
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
x : ↥H
⊢ (β : (a : ↥H) → K) x = HSMul.hSMul (β := (a : ↥H) → K) u (⇑α : (a : ↥H) → K) x

Tactic:
exact DFunLike.congr_fun hu.symm x

Premises used: DFunLike.congr_fun, Eq.symm
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = -α
inl :
  Eq (α := Dual.{u_1, u_2} K ↥H)
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
      Dual.{u_1, u_2} K ↥H)
    (-(RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
      Dual.{u_1, u_2} K ↥H)
⊢ Eq (α := Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
        Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
        Dual.{u_1, u_2} K ↥H) ∨
    Eq (α := Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
        Dual.{u_1, u_2} K ↥H)
      (-(RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
            (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
              Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
        Dual.{u_1, u_2} K ↥H)

Tactic:
right