awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
⊢ Ne (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      ((⇑β : (a : ↥H) → K) -
        HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
    ⊥
have pos : ∀ (hα : α.IsZero),
  Ne (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      ((⇑β : (a : ↥H) → K) -
        HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
    ⊥
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
pos :
  ∀ (hα : α.IsZero),
    Ne (α := LieSubmodule K (↥H) L)
      (genWeightSpace L
        ((⇑β : (a : ↥H) → K) -
          HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
      ⊥
⊢ Ne (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      ((⇑β : (a : ↥H) → K) -
        HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
    ⊥
have neg : ∀ (hα : ¬α.IsZero),
  Ne (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      ((⇑β : (a : ↥H) → K) -
        HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
    ⊥
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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α : ¬α.IsZero
⊢ Ne (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      ((⇑β : (a : ↥H) → K) -
        HSMul.hSMul (α := K) (β := (a : ↥H) → K) ((β : (a : ↥H) → K) (coroot α) : K) (⇑α : (a : ↥H) → K)))
    ⊥
have neg : -HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ∧
  - -HSub.hSub (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) ≤
    (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
Tactic: rw [sub_eq_neg_add, apply_coroot_eq_cast α β, ← neg_smul, ← Int.cast_neg,
      Int.cast_smul_eq_zsmul, rootSpace_zsmul_add_ne_bot_iff α β hα]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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β : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
have pos : ∀ (hα : α.IsZero), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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β : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
pos : ∀ (hα : α.IsZero), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
have neg : ∀ (hα : ¬α.IsZero), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
Tactic: by_cases hα : α.IsZero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (hypothesis)
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β : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
⊢ False
have this : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
Tactic: have : β (coroot α) = 0 := by
    by_cases hα : α.IsZero
    · simp [coroot_eq_zero_iff.mpr hα]
    simpa [root_apply_coroot hα, mul_two] using congr_fun (sub_eq_zero.mp e) (coroot α)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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β : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
this : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
⊢ reflectRoot α β = β
have h : ∀ (x : ↥H),
  Eq.{u_1 + 1} (α := K) (((reflectRoot α β : Weight K (↥H) L) : (a : ↥H) → K) x : K) ((β : (a : ↥H) → K) x : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (hypothesis)
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β : β.IsNonZero
e : Weight.IsZero (reflectRoot α β : Weight K (↥H) L)
this : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K) (0 : K)
⊢ False
have this₁ : reflectRoot α β = β
Tactic: have : reflectRoot α β = β := by ext; simp [reflectRoot, this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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))
h :
  Eq (α := Dual.{u_1, u_2} K ↥H)
    ((fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L)) α)
    ((fun (x : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) ↦ Weight.toLinear K (↥H) L (↑x : Weight K (↥H) L)) β)
⊢ α = β
have a : ∀ (x : ↥H),
  Eq.{u_1 + 1} (α := K) (((↑α : Weight K (↥H) L) : (a : ↥H) → K) x : K) (((↑β : Weight K (↥H) L) : (a : ↥H) → K) x : K)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
⊢ 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)))
    ⊤
have 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' := sorry } :
      (a : ↥LieSubalgebra.root) → Dual K ↥H))
  (Set.image (α := Weight K (↥H) L) (Weight.toLinear K (↥H) L) {α : Weight K (↥H) L | α.IsNonZero})
Tactic: convert! span_weight_isNonZero_eq_top K L H
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
⊢ 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})
have 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' := sorry } :
          (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: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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.CorootForm (ι := ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))) (rootSystem H) =
    LinearMap.BilinForm.restrict (killingForm K L) H.toSubmodule
have 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))
Tactic: rw [restrict_killingForm_eq_sum, RootPairing.CorootForm, ← Finset.sum_coe_sort (s := H.root)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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)) ⊤
have 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)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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} (α := 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)))
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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), ⨆ (_ : α.IsNonZero), corootSubmodule α = H.toLieSubmodule
have suffices : Eq.{u_2 + 1} (α := LieIdeal K ↥H) (⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), corootSpace (⇑α : (a : ↥H) → K)) ⊤
Tactic: suffices ⨆ α : Weight K H L, ⨆ (_ : α.IsNonZero), corootSpace α = ⊤ from
    le_antisymm (by simp) (by simp [← LieSubmodule.map_iSup, this])
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (hypothesis)
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)
⊢ 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)
have 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β)
Tactic: rw [LinearIndependent.pair_iff' ((rootSystem H).ne_zero _), not_forall] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (hypothesis)
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β)
⊢ 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)
have e₁ : ∃ (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
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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 β
⊢ (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) u (⇑α : (a : ↥H) → K)
have h : ∀ (x : ↥H), (β : (a : ↥H) → K) x = HSMul.hSMul (β := (a : ↥H) → K) u (⇑α : (a : ↥H) → K) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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 : β = -α
⊢ 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)
have 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)
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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 : β = -α
⊢ 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)
have inl : ∀ (x : ↥H),
  Eq.{u_1 + 1} (α := K)
    ((((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) :
          (a : ↥H) → K)
        x :
      K)
    (((-(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) :
          (a : ↥H) → K)
        x :
      K)
Tactic: ext x