English
A refinement of the previous lemma asserts the same representation with an explicit constructive proof step.
Русский
Уточнение предыдущей леммы: то же представление с явным конструктивным шагом доказательства.
LaTeX
$$same as 133511$$
Lean4
theorem add_zsmul {i j k : ι} {z : ℤ} (hij : i ≠ j) (hi : b.IsPos i) (hj : j ∈ b.support)
(hk : P.root k = P.root i + z • P.root j) : b.IsPos k :=
by
replace hij : LinearIndependent R ![P.root j, P.root i] :=
by
refine IsReduced.linearIndependent P hij.symm fun contra ↦ ?_
letI := P.indexNeg
replace contra : i = -j := by rw [eq_comm, neg_eq_iff_eq_neg]; simpa using contra
rw [contra, isPos_iff, height_reflectionPerm_self, height_one_of_mem_support hj] at hi
omega
induction z generalizing i k with
| zero => simp_all
| succ w
hw =>
obtain ⟨l, hl⟩ : P.root i + (w : ℤ) • P.root j ∈ range P.root :=
by
replace hk : P.root i + (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
simp only [natCast_zsmul, root_add_nsmul_mem_range_iff_le_chainTopCoeff hij] at hk ⊢
cutsat
replace hk : P.root k = P.root l + P.root j := by rw [hk, hl]; module
exact (hw hi hl hij).add (b.isPos_of_mem_support hj) hk
| pred w
hw =>
obtain ⟨l, hl⟩ : P.root i + (-w : ℤ) • P.root j ∈ range P.root :=
by
replace hk : P.root i - (w + 1) • P.root j ∈ range P.root := ⟨k, by rw [hk]; module⟩
rw [neg_smul, ← sub_eq_add_neg, natCast_zsmul]
simp only [root_sub_nsmul_mem_range_iff_le_chainBotCoeff hij] at hk ⊢
cutsat
replace hk : P.root k = P.root l - P.root j := by rw [hk, hl]; module
exact (hw hi hl hij).sub hj hk
