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
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)
refine : ∀ (i j : ↥(Finset.Ioo p q)) (hij : (↑i : ℤ) • α + χ = (↑j : ℤ) • α + χ), i = j
⊢ iSupIndep.{1, u_3} (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) fun (i : ↥(Finset.Ioo p q)) ↦
    genWeightSpace M ((↑i : ℤ) • α + χ)

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

Premises used: iSupIndep.comp, Membership.mem, Subtype, LieModule.iSupIndep_genWeightSpace
-- 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)
i j : ↥(Finset.Ioo p q)
hij : (↑i : ℤ) • α + χ = (↑j : ℤ) • α + χ
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hij : (↑i : ℤ) • α = (↑j : ℤ) • α),
    Eq (α := ↥H → R) ((fun (x : ℤ) ↦ x • α) (↑i : ℤ)) ((fun (x : ℤ) ↦ x • α) (↑j : ℤ))
⊢ Eq (α := ↥H → R) ((fun (x : ℤ) ↦ x • α) (↑i : ℤ)) ((fun (x : ℤ) ↦ x • α) (↑j : ℤ))

Tactic:
rwa [add_left_inj] at hij

Premises used: add_left_inj
-- 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)
i j : ↥(Finset.Ioo p q)
hij : (↑i : ℤ) • α + χ = (↑j : ℤ) • α + χ
⊢ i = j

Tactic:
exact SetCoe.ext <| smul_left_injective ℤ hα <| by rwa [add_left_inj] at hij

Premises used: SetCoe.ext, smul_left_injective, Int
-- 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} (α := 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
-- 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)
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))
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))
⊢ Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M) (⨆ i ∈ Finset.Ioo p q, N i)

Tactic:
simp_rw [N, genWeightSpaceChain_def', LieSubmodule.iSup_toSubmodule]

Premises used: LieSubmodule.iSup_toSubmodule, LieModule.genWeightSpaceChain_def'
-- 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)
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)
⊢ 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]
-- 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)
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)
h₃ : Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M) (⨆ i ∈ Finset.Ioo p q, N i)
rw :
  (a • α + HSMul.hSMul (α := ℤ) (↑b : ℤ) χ) x =
    (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
        (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
      (LinearMap.restrict ((toEnd R (↥H) M : (a : ↥H) → End R M) x) ⋯)
⊢ (a • α + HSMul.hSMul (α := ℤ) (↑b : ℤ) χ) x = 0

Tactic:
rw [← trace_toEnd_genWeightSpaceChain_eq_zero M α χ p q hp hq hx,
    ← LieSubmodule.toEnd_restrict_eq_toEnd]

Premises used: LieSubmodule.toEnd_comp_subtype_mem, LieSubmodule.toEnd_restrict_eq_toEnd, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero
-- 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)
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)
h₃ : Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M) (⨆ i ∈ Finset.Ioo p q, N i)
subst :
  ∀ (hb : LT.lt (α := ℕ) 0 (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))))
    (h₁ :
      iSupIndep.{1, u_3} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦
        (fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) (↑i : ℤ))
    (h₂ :
      ∀ (i : ℤ),
        MapsTo (⇑((toEnd R (↥H) M : (a : ↥H) → End R M) x : End R M) : (a : M) → M)
          (↑((fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i) : Set M)
          (↑((fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i) : Set M))
    (h₃ :
      Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M)
        (⨆ i ∈ Finset.Ioo p q, (fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i)),
    (HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) α +
          HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) χ)
        x =
      (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
          (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
        (LinearMap.restrict ((toEnd R (↥H) M : (a : ↥H) → End R M) x) ⋯)
⊢ (a • α + HSMul.hSMul (α := ℤ) (↑b : ℤ) χ) x =
    (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
        (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
      (LinearMap.restrict ((toEnd R (↥H) M : (a : ↥H) → End R M) x) ⋯)

Tactic:
subst a b N
-- 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 • α + χ)) ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : LT.lt (α := ℕ) 0 (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)))
h₁ :
  iSupIndep.{1, u_3} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦
    (fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) (↑i : ℤ)
h₂ :
  ∀ (i : ℤ),
    MapsTo (⇑((toEnd R (↥H) M : (a : ↥H) → End R M) x : End R M) : (a : M) → M)
      (↑((fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i) : Set M)
      (↑((fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i) : Set M)
h₃ :
  Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M)
    (⨆ i ∈ Finset.Ioo p q, (fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i)
erw :
  (HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) α +
        HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) χ)
      x =
    ∑ i ∈ Finset.Ioo p q,
      (LinearMap.trace R ↥(↑(genWeightSpace M (i • α + χ)) : Submodule R M) :
          (a :
              ↥(↑(genWeightSpace M (i • α + χ)) : Submodule R M) →ₗ[R]
                ↥(↑(genWeightSpace M (i • α + χ)) : Submodule R M)) →
            R)
        (LinearMap.restrict ((toEnd R (↥H) M : (a : ↥H) → End R M) x) ⋯)
⊢ (HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) α +
        HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) χ)
      x =
    (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
        (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
      (LinearMap.restrict ((toEnd R (↥H) M : (a : ↥H) → End R M) x) ⋯)

Tactic:
erw [LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup _ h₁ h₂ (genWeightSpaceChain M α χ p q) h₃]

Premises used: LieModule.genWeightSpaceChain, LieSubmodule.toSubmodule, Eq.rec, SetLike.coe, Eq.symm, LinearMap.mapsTo_biSup_of_mapsTo, LinearMap.trace_eq_sum_trace_restrict_of_eq_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
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 • α + χ)) ⊥
x : ↥H
hx : x ∈ corootSpace α
hb : LT.lt (α := ℕ) 0 (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)))
h₁ :
  iSupIndep.{1, u_3} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦
    (fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) (↑i : ℤ)
h₂ :
  ∀ (i : ℤ),
    MapsTo (⇑((toEnd R (↥H) M : (a : ↥H) → End R M) x : End R M) : (a : M) → M)
      (↑((fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i) : Set M)
      (↑((fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i) : Set M)
h₃ :
  Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M)
    (⨆ i ∈ Finset.Ioo p q, (fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i)
simp_rw :
  (HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) α +
        HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) χ)
      x =
    ∑ x_1 ∈ Finset.Ioo p q,
      (LinearMap.trace R ↥(↑(genWeightSpace M (x_1 • α + χ)) : Submodule R M) :
          (a :
              ↥(↑(genWeightSpace M (x_1 • α + χ)) : Submodule R M) →ₗ[R]
                ↥(↑(genWeightSpace M (x_1 • α + χ)) : Submodule R M)) →
            R)
        (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpace M (x_1 • α + χ)) :
                LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpace M (x_1 • α + χ)))) :
              (a : ↥H) → End R ↥(genWeightSpace M (x_1 • α + χ)))
            x :
          End R ↥(genWeightSpace M (x_1 • α + χ)))
⊢ (HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) α +
        HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) χ)
      x =
    ∑ i ∈ Finset.Ioo p q,
      (LinearMap.trace R ↥(↑(genWeightSpace M (i • α + χ)) : Submodule R M) :
          (a :
              ↥(↑(genWeightSpace M (i • α + χ)) : Submodule R M) →ₗ[R]
                ↥(↑(genWeightSpace M (i • α + χ)) : Submodule R M)) →
            R)
        (LinearMap.restrict ((toEnd R (↥H) M : (a : ↥H) → End R M) x) ⋯)

Tactic:
simp_rw [LieSubmodule.toEnd_restrict_eq_toEnd]

Premises used: LieSubmodule.toEnd_comp_subtype_mem, LieSubmodule.toEnd_restrict_eq_toEnd
-- 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
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainTopCoeff (-α) β = chainBotCoeff α β

Tactic:
rfl

Premises used: LieModule.chainBotCoeff, 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
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
rw : chainTopCoeff (- -α) β = chainTopCoeff α β
rw₁ rw₂ : chainTopCoeff α β = chainTopCoeff α β
⊢ chainBotCoeff (-α) β = chainTopCoeff α β

Tactic:
rw [← chainTopCoeff_neg, neg_neg]

Premises used: neg_neg, LieModule.chainTopCoeff_neg
-- 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
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
β : Weight R L M
⊢ chainTopCoeff 0 β = 0

Tactic:
dif_pos rfl

Premises used: dif_pos, LieModule.chainTopCoeff, 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
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
β : Weight R L M
⊢ chainBotCoeff 0 β = 0

Tactic:
dif_pos neg_zero

Premises used: dif_pos, LieModule.chainBotCoeff, neg_zero, LieModule.chainTopCoeff
-- 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
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
rw :
  (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥)
          ⋯).pred +
      1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
⊢ chainTopCoeff α β + 1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯

Tactic:
rw [chainTopCoeff, dif_neg hα]

Premises used: dif_neg, LieModule.chainTopCoeff
-- 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
inst_8 : IsAddTorsionFree R
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
a : 0 < Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯
⊢ (Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥)
          ⋯).pred +
      1 =
    Nat.find (p := fun (n : ℕ) ↦ Eq (α := LieSubmodule R L M) (genWeightSpace M (n • α + (⇑β : (a : L) → R))) ⊥) ⋯

Tactic:
apply Nat.succ_pred_eq_of_pos

Premises used: Nat.succ_pred_eq_of_pos