awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥

Tactic:
exact hp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
refine_2 : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (HSMul.hSMul (α := ℤ) (↑q : ℤ) χ₁ + χ₂)) ⊥

Tactic:
rw [natCast_zsmul]

Premises used: natCast_zsmul
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥

Tactic:
hq
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥
p : ℕ
hp₀ : p > 0
hp : Eq (α := LieSubmodule R L M) (genWeightSpace M (p • -χ₁ + χ₂)) ⊥
⊢ Eq (α := LieSubmodule R L M) (genWeightSpace M (q • χ₁ + χ₂)) ⊥

Tactic:
exact hq
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ Eq (α := LieSubmodule R L M) (genWeightSpaceChain M χ₁ χ₂ p q) (⨆ k ∈ Ioo p q, genWeightSpace M (k • χ₁ + χ₂))

Tactic:
rfl

Premises used: LieModule.genWeightSpaceChain, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q

Tactic:
have : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q := by simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯
simp_rw :
  Eq.{u_3 + 1} (α := LieSubmodule R L M) (⨆ k ∈ Ioo (-q) (-p), genWeightSpace M (k • -χ₁ + χ₂))
    (⨆ (i : ℤ),
      ⨆ (_ : Membership.mem (γ := Set ℤ) ((⇑e.symm : (a : ℤ) → ℤ) '' Ioo p q) i),
        genWeightSpace M (HSMul.hSMul (α := ℤ) ((e : (a : ℤ) → ℤ) i : ℤ) χ₁ + χ₂))
⊢ Eq (α := LieSubmodule R L M) (genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p)) (genWeightSpaceChain M χ₁ χ₂ p q)

Tactic:
simp_rw [genWeightSpaceChain, ← e.biSup_comp (Ioo p q)]

Premises used: LieModule.genWeightSpaceChain, Equiv.biSup_comp, Set.Ioo
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯
⊢ Eq.{u_3 + 1} (α := LieSubmodule R L M) (⨆ k ∈ Ioo (-q) (-p), genWeightSpace M (k • -χ₁ + χ₂))
    (⨆ (i : ℤ),
      ⨆ (_ : Membership.mem (γ := Set ℤ) ((⇑e.symm : (a : ℤ) → ℤ) '' Ioo p q) i),
        genWeightSpace M (HSMul.hSMul (α := ℤ) ((e : (a : ℤ) → ℤ) i : ℤ) χ₁ + χ₂))

Tactic:
simp [e, -mem_Ioo]

Premises used: Set.mem_Ioo
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q k : ℤ
hk : k ∈ Ioo p q
⊢ LE.le (α := LieSubmodule R L M) (genWeightSpace M (k • χ₁ + χ₂)) (genWeightSpaceChain M χ₁ χ₂ p q)

Tactic:
le_biSup (fun i ↦ genWeightSpace M (i • χ₁ + χ₂)) hk

Premises used: Set.Mem, setOf, HAdd.hAdd, HSMul.hSMul, LieModule.genWeightSpace, le_biSup
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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) (genWeightSpaceChain M α χ p q) y
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (⨆ (x : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑x : ℤ) • α + χ)) y

Tactic:
rw [genWeightSpaceChain, iSup_subtype'] at hy

Premises used: iSup_subtype', LieModule.genWeightSpaceChain
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
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
mem :
  ∀ (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),
    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, z⁆

Tactic:
obtain ⟨k, hk⟩ := k
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
this :
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (genWeightSpaceChain M α χ p q)
a : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ)) ⁅x, z⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆

Tactic:
apply this
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
this :
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (genWeightSpaceChain M α χ p q)
rw : α + (k • α + χ) = k • α + HSMul.hSMul (α := ℤ) 1 α + χ
⊢ α + (k • α + χ) = (k + 1) • α + χ

Tactic:
rw [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
this :
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (genWeightSpaceChain M α χ p q)
⊢ α + (k • α + χ) = k • α + HSMul.hSMul (α := ℤ) 1 α + χ

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
this :
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (genWeightSpaceChain M α χ p q)
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ)) ⁅x, z⁆

Tactic:
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

Premises used: LieAlgebra.rootSpaceWeightSpaceProduct, zsmul_eq_mul, Int.cast_add, Pi.intCast_def, Subtype.mk, HAdd.hAdd, HSMul.hSMul, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe, Int.cast_one, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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 :
  LE.le (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((k + 1) • α + χ))
    (genWeightSpaceChain M α χ p q)
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆

Tactic:
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
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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 • α + χ))
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 • α + χ))
⊢ 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'

Premises used: HAdd.hAdd, eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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 : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
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:
simp only [hq, bot_le]

Premises used: bot_le
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
linarith₁ : k + 1 ≤ p → GT.gt (α := ℤ) 2 0
⊢ p < k + 1

Tactic:
linarith [hk.1]

Premises used: And.left
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
⊢ 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'⟩
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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 ∈ Ioo p 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:
le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'

Premises used: Set.Mem, setOf, HAdd.hAdd, HSMul.hSMul, LieModule.genWeightSpace, le_biSup
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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 ∈ Ioo p 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:
exact le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'

Premises used: HAdd.hAdd, HSMul.hSMul, LieModule.genWeightSpace, le_biSup
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, 0⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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⁆
add : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) (⁅x, x_1⁆ + ⁅x, y_1⁆)
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, x_1 + y_1⁆

Tactic:
rw [lie_add]

Premises used: lie_add
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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⁆ + ⁅x, y_1⁆)

Tactic:
add_mem hz₁ hz₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Weights.Chain
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⁆ + ⁅x, y_1⁆)

Tactic:
exact add_mem hz₁ hz₂

Premises used: AddMemClass.add_mem