awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z
⊢ LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ))
have mem : ∀ (hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ)) ⊥) (hk : k ∈ Ioo p (k + 1))
  (hz :
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
      (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p (k + 1))) k hk) : ℤ) • α + χ)) z),
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (⨆ k_1 ∈ Ioo p (k + 1), genWeightSpace M (k_1 • α + χ))
Tactic: rcases eq_or_ne (k + 1) q with rfl | hk'
Cleared hypotheses: q, hq, hk, hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z
mem :
  ∀ (hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ)) ⊥)
    (hk : k ∈ Ioo p (k + 1))
    (hz :
      Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
        (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p (k + 1))) k hk) : ℤ) • α + χ)) z),
    LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
      (⨆ k_1 ∈ Ioo p (k + 1), genWeightSpace M (k_1 • α + χ))
⊢ LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ))
have mem₁ : ∀ (hk' : k + 1 ≠ q),
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ))
Tactic: rcases eq_or_ne (k + 1) q with rfl | hk'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z
hk' : k + 1 ≠ q
⊢ p < k + 1
have linarith : k + 1 ≤ p → HMul.hMul (α := ℤ) 2 (-1) + (k + 1 - p) + (p + 1 - k) = 0
Tactic: linarith [hk.1]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z
hk' : k + 1 ≠ q
linarith : k + 1 ≤ p → HMul.hMul (α := ℤ) 2 (-1) + (k + 1 - p) + (p + 1 - k) = 0
⊢ p < k + 1
have linarith₁ : k + 1 ≤ p → GT.gt (α := ℤ) 2 0
Tactic: linarith [hk.1]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M ((↑(Subtype.mk (p := Membership.mem (Ioo p q)) k hk) : ℤ) • α + χ)) z
hk' : k + 1 ≠ q
⊢ LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ))
have hk'₁ : k + 1 ∈ Ioo p q
Tactic: replace hk' : k + 1 ∈ Ioo p q := ⟨by linarith [hk.1], lt_of_le_of_ne hk.2 hk'⟩
Cleared hypotheses: hk'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y x_1 y_1 : M
hx_1 :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (⨆ (i : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑i : ℤ) • α + χ)) x_1
hy :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (⨆ (i : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑i : ℤ) • α + χ)) y_1
hz₁ : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, x_1⁆
hz₂ : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y_1⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, x_1 + y_1⁆
have add : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) (⁅x, x_1⁆ + ⁅x, y_1⁆)
Tactic: rw [lie_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y : M
hy :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (⨆ (x : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑x : ℤ) • α + χ)) y
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆
have mem : ∀ (k : Subtype (Membership.mem (Ioo p q))) (z : M)
  (hz : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((↑k : ℤ) • α + χ)) z),
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆
Tactic: induction hy using LieSubmodule.iSup_induction' with
  | mem k z hz =>
    obtain ⟨k, hk⟩ := k
    suffices genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q by
      apply this
      -- was `simpa using [...]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      simpa only [zsmul_eq_mul, Int.cast_add, Pi.intCast_def, Int.cast_one] using
        (rootSpaceWeightSpaceProduct R L H M α (k • α + χ) ((k + 1) • α + χ)
            (by rw [add_smul]; abel) (⟨x, hx⟩ ⊗ₜ ⟨z, hz⟩)).property
    rw [genWeightSpaceChain]
    rcases eq_or_ne (k + 1) q with rfl | hk'; · simp only [hq, bot_le]
    replace hk' : k + 1 ∈ Ioo p q := ⟨by linarith [hk.1], lt_of_le_of_ne hk.2 hk'⟩
    exact le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'
  | zero => simp
  | add _ _ _ _ hz₁ hz₂ => rw [lie_add]; exact add_mem hz₁ hz₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y : M
hy :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (⨆ (x : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑x : ℤ) • α + χ)) y
mem :
  ∀ (k : Subtype (Membership.mem (Ioo p q))) (z : M)
    (hz : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((↑k : ℤ) • α + χ)) z),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆
have zero : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, 0⁆
Tactic: induction hy using LieSubmodule.iSup_induction' with
  | mem k z hz =>
    obtain ⟨k, hk⟩ := k
    suffices genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q by
      apply this
      -- was `simpa using [...]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      simpa only [zsmul_eq_mul, Int.cast_add, Pi.intCast_def, Int.cast_one] using
        (rootSpaceWeightSpaceProduct R L H M α (k • α + χ) ((k + 1) • α + χ)
            (by rw [add_smul]; abel) (⟨x, hx⟩ ⊗ₜ ⟨z, hz⟩)).property
    rw [genWeightSpaceChain]
    rcases eq_or_ne (k + 1) q with rfl | hk'; · simp only [hq, bot_le]
    replace hk' : k + 1 ∈ Ioo p q := ⟨by linarith [hk.1], lt_of_le_of_ne hk.2 hk'⟩
    exact le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'
  | zero => simp
  | add _ _ _ _ hz₁ hz₂ => rw [lie_add]; exact add_mem hz₁ hz₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y : M
hy :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (⨆ (x : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑x : ℤ) • α + χ)) y
mem :
  ∀ (k : Subtype (Membership.mem (Ioo p q))) (z : M)
    (hz : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((↑k : ℤ) • α + χ)) z),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆
zero : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, 0⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆
have add : ∀ (x_1 y : M),
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
      (⨆ (i : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑i : ℤ) • α + χ)) x_1 →
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
        (⨆ (i : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑i : ℤ) • α + χ)) y →
      ∀ (hz₁ : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, x_1⁆)
        (hz₂ : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆),
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, x_1 + y⁆
Tactic: induction hy using LieSubmodule.iSup_induction' with
  | mem k z hz =>
    obtain ⟨k, hk⟩ := k
    suffices genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q by
      apply this
      -- was `simpa using [...]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      simpa only [zsmul_eq_mul, Int.cast_add, Pi.intCast_def, Int.cast_one] using
        (rootSpaceWeightSpaceProduct R L H M α (k • α + χ) ((k + 1) • α + χ)
            (by rw [add_smul]; abel) (⟨x, hx⟩ ⊗ₜ ⟨z, hz⟩)).property
    rw [genWeightSpaceChain]
    rcases eq_or_ne (k + 1) q with rfl | hk'; · simp only [hq, bot_le]
    replace hk' : k + 1 ∈ Ioo p q := ⟨by linarith [hk.1], lt_of_le_of_ne hk.2 hk'⟩
    exact le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'
  | zero => simp
  | add _ _ _ _ hz₁ hz₂ => rw [lie_add]; exact add_mem hz₁ hz₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) y
⊢ Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥
have rwa : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-(-p • α) + χ)) ⊥
Tactic: rwa [smul_neg, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) y
rwa : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-(-p • α) + χ)) ⊥
⊢ Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥
have rwa₁ : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (- -(p • α) + χ)) ⊥
Tactic: rwa [smul_neg, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) y
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆
have hp₁ : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥
Tactic: replace hp : genWeightSpace M ((-p) • (-α) + χ) = ⊥ := by rwa [smul_neg, neg_smul, neg_neg]
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) y
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆
have rw : ∀ (hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M (-α) χ (-q) (-p)) y)
  (hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥),
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M (-α) χ (-q) (-p)) ⁅x, y⁆
Tactic: rw [← genWeightSpaceChain_neg] at hy ⊢
Cleared hypotheses: hy, hp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : ↥H
hx : x ∈ corootSpace α
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
          (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
        (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
              (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
            x :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)
have hx₁ : Membership.mem (γ := Submodule R ↥H)
  (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x
Tactic: rw [LieAlgebra.mem_corootSpace'] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
hu : Membership.mem (γ := Set ↥H) {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)} u
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
          (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
        (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
              (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
            u :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)
have mem : ∀ (y : L) (hy : y ∈ rootSpace H α) (z : L) (hz : z ∈ rootSpace H (-α)) (hyz : ⁅y, z⁆ = (↑u : L)),
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
          (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
        (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
              (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
            u :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)
Tactic: obtain ⟨y, hy, z, hz, hyz⟩ := hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = (↑u : L)
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
⊢ ((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
          LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
        (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
      u =
    ⁅f, g⁆
have h : ∀ (x : ↥(genWeightSpaceChain M α χ p q)),
  Eq.{u_3 + 1} (α := M)
    (↑(((((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                    LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                  (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
                u :
              End R ↥(genWeightSpaceChain M α χ p q)) :
            (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q))
          x) :
      M)
    (↑((⁅f, g⁆ : (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q)) x) : M)
Tactic: ext