awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
IH :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((n + 1) • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)
have succ : Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((n + 1) • χ₁ + χ₂))
  (⁅x,
      (HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m⁆ :
    M)
Tactic: simp only [pow_succ', Module.End.mul_apply, toEnd_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
IH :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((n + 1) • χ₁ + χ₂))
    (⁅x,
        (HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              n :
            (a : M) → M)
          m⁆ :
      M)
have h : (n + 1) • χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
Tactic: convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
IH :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
⊢ (n + 1) • χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
have h : n • χ₁ + χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
Tactic: rw [succ_nsmul, ← add_assoc, add_comm (n • _)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
IH :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
h : n • χ₁ + χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
⊢ (n + 1) • χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
have h₁ : n • χ₁ + χ₁ + χ₂ = χ₁ + n • χ₁ + χ₂
Tactic: rw [succ_nsmul, ← add_assoc, add_comm (n • _)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
IH :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
h : n • χ₁ + χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
h₁ : n • χ₁ + χ₁ + χ₂ = χ₁ + n • χ₁ + χ₂
⊢ (n + 1) • χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
have h₂ : χ₁ + n • χ₁ + χ₂ = χ₁ + n • χ₁ + χ₂
Tactic: rw [succ_nsmul, ← add_assoc, add_comm (n • _)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
have zero : Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 χ₁ + χ₂))
  ((HPow.hPow (α := Module.End R M) (β := ℕ)
          (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
          0 :
        (a : M) → M)
      m :
    M)
Tactic: induction n with
  | zero => simpa using hm
  | succ n IH =>
    simp only [pow_succ', Module.End.mul_apply, toEnd_apply_apply]
    convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2
    rw [succ_nsmul, ← add_assoc, add_comm (n • _)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
zero :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M) (β := ℕ)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            0 :
          (a : M) → M)
        m :
      M)
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
have succ : ∀ (n : ℕ)
  (IH :
    Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              n :
            (a : M) → M)
          m :
        M)),
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((n + 1) • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)
Tactic: induction n with
  | zero => simpa using hm
  | succ n IH =>
    simp only [pow_succ', Module.End.mul_apply, toEnd_apply_apply]
    convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2
    rw [succ_nsmul, ← add_assoc, add_comm (n • _)]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
x_1 y : L
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ i ∈ s, rootSpace H i) x_1
hy : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ i ∈ s, rootSpace H i) y
hu : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅x_1, m⁆
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅y, m⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅x_1 + y, m⁆
have add : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) (⁅x_1, m⁆ + ⁅y, m⁆)
Tactic: rw [add_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
χ₁ : ↥H → R
u : L
hu : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ (_ : χ₁ ∈ s), rootSpace H χ₁) u
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
have pos : ∀ (hχ₁ : χ₁ ∈ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
Tactic: by_cases hχ₁ : χ₁ ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
χ₁ : ↥H → R
u : L
hu : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ (_ : χ₁ ∈ s), rootSpace H χ₁) u
pos : ∀ (hχ₁ : χ₁ ∈ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
have neg : ∀ (hχ₁ : χ₁ ∉ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
Tactic: by_cases hχ₁ : χ₁ ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
χ₁ : ↥H → R
u : L
hu : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ (_ : χ₁ ∈ s), rootSpace H χ₁) u
hχ₁ : χ₁ ∈ s
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
have hu₁ : u ∈ rootSpace H χ₁
Tactic: replace hu : u ∈ rootSpace H χ₁ := by simpa [hχ₁] using hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x_1 y : M
hx : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) x_1
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) y
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x_1⁆
hw : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, y⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x_1 + y⁆
have pos : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) (⁅u, x_1⁆ + ⁅u, y⁆)
Tactic: rw [lie_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
have pos : ∀ (hχ₂ : χ₂ ∈ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
Tactic: by_cases hχ₂ : χ₂ ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v
pos : ∀ (hχ₂ : χ₂ ∈ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
have neg : ∀ (hχ₂ : χ₂ ∉ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
Tactic: by_cases hχ₂ : χ₂ ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v
hχ₂ : χ₂ ∈ s
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
have pos : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₁ + χ₂ ∈ s), genWeightSpace M (χ₁ + χ₂)) ⁅u, v⁆
Tactic: apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
have pos : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, 0⁆
Tactic: induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
pos : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, 0⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
have pos₁ : ∀ (x y : M),
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) x →
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) y →
      ∀ (hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x⁆)
        (hw : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, y⁆),
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x + y⁆
Tactic: induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
pos : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, 0⁆
pos₁ :
  ∀ (x y : M),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) x →
      Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) y →
        ∀ (hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x⁆)
          (hw : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, y⁆),
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x + y⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
have pos₂ : ∀ (χ₂ : ↥H → R) (v : M)
  (hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v),
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
Tactic: induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ χ ∈ s, rootSpace H χ) x
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅x, m⁆
have zero : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ)
  (Bracket.bracket.{u_2, u_3} (L := L) 0 m)
Tactic: induction hx using LieSubmodule.iSup_induction' with
  | zero => simp
  | add _ _ _ _ hu hv => rw [add_lie]; exact add_mem hu hv
  | mem χ₁ u hu =>
    by_cases hχ₁ : χ₁ ∈ s; swap
    · simp_all
    replace hu : u ∈ rootSpace H χ₁ := by simpa [hχ₁] using hu
    induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]
Cleared hypotheses: hx