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
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⁆

Tactic:
have hfg : toEnd R H _ u = ⁅f, g⁆ := by
      ext
      rw [toEnd_apply_apply, LieSubmodule.coe_bracket, LieSubalgebra.coe_bracket_of_module, ← hyz]
      simp only [lie_lie, LieHom.lie_apply, LinearMap.coe_mk, AddHom.coe_mk, Module.End.lie_apply,
        AddSubgroupClass.coe_sub, f, g]
-- 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 : 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' := ⋯ }
hfg :
  ((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⁆
⊢ 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:
simp [hfg]
-- 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 : 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
⊢ 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))
          0) :
      R)
    (0 : R)

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 : 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 x_1 y : ↥H
hx :
  Membership.mem (γ := Submodule R ↥H)
    (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x_1
hy :
  Membership.mem (γ := Submodule R ↥H)
    (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) y
h :
  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_1 :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)
h_1 :
  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))
            y :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)
⊢ 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_1 + y) :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)

Tactic:
simp_all
-- 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 : 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
a : R
x_1 : ↥H
hx :
  Membership.mem (γ := Submodule R ↥H)
    (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x_1
h :
  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_1 :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)
⊢ 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))
            (a • x_1) :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)

Tactic:
simp_all
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
obtain :
  ∀ (p : ℤ) (hp₀ : p < 0) (q : ℤ) (hq₀ : q > 0)
    (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 • α + χ)) ⊥),
    ∃ (a : ℤ) (b : ℤ), 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0
⊢ ∃ (a : ℤ) (b : ℤ), 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0

Tactic:
obtain ⟨p, hp₀, q, hq₀, hp, hq⟩ := exists₂_genWeightSpace_smul_add_eq_bot M α χ hα

Premises used: LieModule.exists₂_genWeightSpace_smul_add_eq_bot
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
rwa rwa₁ rwa₂ rwa₃ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
⊢ Nontrivial.{u_3} ↥(genWeightSpace M χ)

Tactic:
rwa [LieSubmodule.nontrivial_iff_ne_bot]

Premises used: LieSubmodule.nontrivial_iff_ne_bot
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
⊢ Nontrivial.{u_3} ↥(genWeightSpace M χ)

Tactic:
replace hχ : Nontrivial (genWeightSpace M χ) := by rwa [LieSubmodule.nontrivial_iff_ne_bot]
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hχ : Nontrivial.{u_3} ↥(genWeightSpace M χ)
⊢ 0 < b

Tactic:
Finset.sum_pos' (fun _ _ ↦ zero_le) ⟨0, Finset.mem_Ioo.mpr ⟨hp₀, hq₀⟩, ?_⟩

Premises used: Iff.mpr, zero_le, Finset.sum_pos', Finset.mem_Ioo, And.intro, Exists.intro, OfNat.ofNat
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hχ : Nontrivial.{u_3} ↥(genWeightSpace M χ)
refine : 0 < finrank.{u_1, u_3} R ↥(genWeightSpace M (HSMul.hSMul (α := ℤ) 0 α + χ))
⊢ 0 < b

Tactic:
refine Finset.sum_pos' (fun _ _ ↦ zero_le) ⟨0, Finset.mem_Ioo.mpr ⟨hp₀, hq₀⟩, ?_⟩

Premises used: Iff.mpr, zero_le, Finset.sum_pos', Finset.mem_Ioo, And.intro, Exists.intro, OfNat.ofNat
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hχ : Nontrivial.{u_3} ↥(genWeightSpace M χ)
rw : 0 < finrank.{u_1, u_3} R ↥(genWeightSpace M χ)
⊢ 0 < finrank.{u_1, u_3} R ↥(genWeightSpace M (HSMul.hSMul (α := ℤ) 0 α + χ))

Tactic:
rw [zero_smul, zero_add]

Premises used: zero_add, zero_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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hχ : Nontrivial.{u_3} ↥(genWeightSpace M χ)
⊢ 0 < finrank.{u_1, u_3} R ↥(genWeightSpace M χ)

Tactic:
finrank_pos

Premises used: Module.finrank_pos
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hχ : Nontrivial.{u_3} ↥(genWeightSpace M χ)
⊢ 0 < finrank.{u_1, u_3} R ↥(genWeightSpace M χ)

Tactic:
exact finrank_pos

Premises used: Module.finrank_pos
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
⊢ 0 < b

Tactic:
have hb : 0 < b := by
    replace hχ : Nontrivial (genWeightSpace M χ) := by rwa [LieSubmodule.nontrivial_iff_ne_bot]
    refine Finset.sum_pos' (fun _ _ ↦ zero_le) ⟨0, Finset.mem_Ioo.mpr ⟨hp₀, hq₀⟩, ?_⟩
    rw [zero_smul, zero_add]
    exact finrank_pos
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
⊢ ∃ (a : ℤ) (b : ℤ), 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0

Tactic:
⟨a, b, Int.natCast_pos.mpr hb, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Nat.cast, And.intro, Exists.intro, Int.natCast_pos
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
refine : ∀ (x : ↥H) (hx : x ∈ corootSpace α), (a • α + HSMul.hSMul (α := ℤ) (↑b : ℤ) χ) x = 0
⊢ ∃ (a : ℤ) (b : ℤ), 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0

Tactic:
refine ⟨a, b, Int.natCast_pos.mpr hb, fun x hx ↦ ?_⟩
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun (k : ℤ) ↦ (↑(genWeightSpace M (k • α + χ)) : Submodule R M)
rw :
  iSupIndep.{1, u_3} (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) fun (i : ↥(Finset.Ioo p q)) ↦
    genWeightSpace M ((↑i : ℤ) • α + χ)
⊢ iSupIndep.{1, u_3} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦ N (↑i : ℤ)

Tactic:
rw [LieSubmodule.iSupIndep_toSubmodule]

Premises used: LieSubmodule.iSupIndep_toSubmodule
-- 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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 • α + χ)) ⊥
a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i
b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))
hb : 0 < b
x : ↥H
hx : x ∈ corootSpace α
N : ℤ → Submodule R M := fun (k : ℤ) ↦ (↑(genWeightSpace M (k • α + χ)) : Submodule R M)
⊢ iSupIndep.{1, u_3} (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) fun (i : ↥(Finset.Ioo p q)) ↦
    genWeightSpace M ((↑i : ℤ) • α + χ)

Tactic:
(iSupIndep_genWeightSpace R H M).comp fun i j hij ↦ ?_

Premises used: iInf, Set.Mem, iSupIndep.comp, setOf, Membership.mem, Subtype, LieModule.iSupIndep_genWeightSpace, LieModule.genWeightSpace