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 : 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' := ⋯ }
x_1 : ↥(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_1) :
      M)
    (↑((⁅f, g⁆ : (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q)) x_1) : M)
have h : ⁅⁅y, z⁆, (↑x_1 : M)⁆ = (↑((⁅f, g⁆ : (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q)) x_1) : M)
Tactic: rw [toEnd_apply_apply, LieSubmodule.coe_bracket, LieSubalgebra.coe_bracket_of_module, ← hyz]
-- 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 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' := ⋯ }
⊢ 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 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⁆
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]
-- 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 : ↥H
hx :
  Membership.mem (γ := Submodule R ↥H)
    (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x
⊢ 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 mem : ∀ (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)
Tactic: induction hx using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨y, hy, z, hz, hyz⟩ := hu
    let f : Module.End R (genWeightSpaceChain M α χ p q) :=
      { toFun := fun ⟨m, hm⟩ ↦ ⟨⁅(y : L), m⁆,
          lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M α χ p q hq hy hm⟩
        map_add' := fun _ _ ↦ by simp
        map_smul' := fun t m ↦ by simp }
    let g : Module.End R (genWeightSpaceChain M α χ p q) :=
      { toFun := fun ⟨m, hm⟩ ↦ ⟨⁅(z : L), m⁆,
          lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left M α χ p q hp hz hm⟩
        map_add' := fun _ _ ↦ by simp
        map_smul' := fun t m ↦ by simp }
    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]
    simp [hfg]
  | zero => simp
  | add => simp_all
  | smul => simp_all
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
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 χ) ⊥
⊢ ∃ (a : ℤ) (b : ℤ), 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0
have 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
Tactic: obtain ⟨p, hp₀, q, hq₀, hp, hq⟩ := exists₂_genWeightSpace_smul_add_eq_bot M α χ hα
-- 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
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
have hχ₁ : Nontrivial.{u_3} ↥(genWeightSpace M χ)
Tactic: replace hχ : Nontrivial (genWeightSpace M χ) := by rwa [LieSubmodule.nontrivial_iff_ne_bot]
Cleared hypotheses: hχ
-- 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
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
have refine : 0 < finrank.{u_1, u_3} R ↥(genWeightSpace M (HSMul.hSMul (α := ℤ) 0 α + χ))
Tactic: refine Finset.sum_pos' (fun _ _ ↦ zero_le) ⟨0, Finset.mem_Ioo.mpr ⟨hp₀, hq₀⟩, ?_⟩
-- 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
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 (HSMul.hSMul (α := ℤ) 0 α + χ))
have rw : 0 < finrank.{u_1, u_3} R ↥(genWeightSpace M χ)
Tactic: rw [zero_smul, zero_add]
-- 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
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 • α + χ))
⊢ ∃ (a : ℤ) (b : ℤ), 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0
have hb : 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
-- 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
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
have refine : ∀ (x : ↥H) (hx : x ∈ corootSpace α), (a • α + HSMul.hSMul (α := ℤ) (↑b : ℤ) χ) x = 0
Tactic: refine ⟨a, b, Int.natCast_pos.mpr hb, fun x 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
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} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦ N (↑i : ℤ)
have rw : iSupIndep.{1, u_3} (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) fun (i : ↥(Finset.Ioo p q)) ↦
  genWeightSpace M ((↑i : ℤ) • α + χ)
Tactic: rw [LieSubmodule.iSupIndep_toSubmodule]
-- 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
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 : ℤ) • α + χ)
have refine : ∀ (i j : ↥(Finset.Ioo p q)) (hij : (↑i : ℤ) • α + χ = (↑j : ℤ) • α + χ), i = j
Tactic: refine (iSupIndep_genWeightSpace R H M).comp fun i j hij ↦ ?_
-- 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
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)
i j : ↥(Finset.Ioo p q)
hij : (↑i : ℤ) • α + χ = (↑j : ℤ) • α + χ
⊢ Eq (α := ↥H → R) ((fun (x : ℤ) ↦ x • α) (↑i : ℤ)) ((fun (x : ℤ) ↦ x • α) (↑j : ℤ))
have rwa : ∀ (hij : (↑i : ℤ) • α = (↑j : ℤ) • α),
  Eq (α := ↥H → R) ((fun (x : ℤ) ↦ x • α) (↑i : ℤ)) ((fun (x : ℤ) ↦ x • α) (↑j : ℤ))
Tactic: rwa [add_left_inj] at hij
Cleared hypotheses: hij
-- 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
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)
⊢ (a • α + HSMul.hSMul (α := ℤ) (↑b : ℤ) χ) x = 0
have h₁ : iSupIndep.{1, u_3} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦ N (↑i : ℤ)
Tactic: have h₁ : iSupIndep fun (i : Finset.Ioo p q) ↦ N i := by
    rw [LieSubmodule.iSupIndep_toSubmodule]
    refine (iSupIndep_genWeightSpace R H M).comp fun i j hij ↦ ?_
    exact SetCoe.ext <| smul_left_injective ℤ hα <| by rwa [add_left_inj] at hij
-- 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
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)
h₁ : iSupIndep.{1, u_3} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦ N (↑i : ℤ)
h₂ :
  ∀ (i : ℤ),
    MapsTo (⇑((toEnd R (↥H) M : (a : ↥H) → End R M) x : End R M) : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
simp_rw :
  Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M)
    (⨆ i ∈ Finset.Ioo p q, (↑(genWeightSpace M (i • α + χ)) : Submodule R M))
⊢ Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M) (⨆ i ∈ Finset.Ioo p q, N i)
have simp_rw₁ : Eq.{u_3 + 1} (α := Submodule R M) (↑(⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • α + χ)) : Submodule R M)
  (⨆ i ∈ Finset.Ioo p q, (↑(genWeightSpace M (i • α + χ)) : Submodule R M))
Tactic: simp_rw [N, genWeightSpaceChain_def', LieSubmodule.iSup_toSubmodule]
-- 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
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)
h₁ : iSupIndep.{1, u_3} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦ N (↑i : ℤ)
h₂ :
  ∀ (i : ℤ),
    MapsTo (⇑((toEnd R (↥H) M : (a : ↥H) → End R M) x : End R M) : (a : M) → M) (↑(N i) : Set M) (↑(N i) : Set M)
⊢ (a • α + HSMul.hSMul (α := ℤ) (↑b : ℤ) χ) x = 0
have h₃ : Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M) (⨆ i ∈ Finset.Ioo p q, N i)
Tactic: have h₃ : genWeightSpaceChain M α χ p q = ⨆ i ∈ Finset.Ioo p q, N i := by
    simp_rw [N, genWeightSpaceChain_def', LieSubmodule.iSup_toSubmodule]