English
For p prime and invertible in R, the pair (n ∈ (xInTermsOfW p ℚ n).vars) and (xInTermsOfW p ℚ n).vars ⊆ range(n+1) holds, with a structured inductive proof controlling the variables.
Русский
Пусть p — простое и обращаемое в ℚ; тогда выполняются вложенные условия: множество переменных xInTermsOfW(p,ℚ,n) содержит n и подмножество переменных не превосходит range(n+1).
LaTeX
$$$ n \in (xInTermsOfW\ p\ ℚ\ n).vars \land (xInTermsOfW\ p\ ℚ\ n).vars \subseteq \operatorname{range}(n+1) $$$
Lean4
theorem xInTermsOfW_vars_aux (n : ℕ) : n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1) :=
by
induction n using Nat.strongRecOn with
| ind n ih => ?_
rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (Invertible.ne_zero _), vars_sub_of_disjoint, vars_X, range_add_one,
insert_eq]
on_goal 1 =>
simp only [true_and, true_or, mem_union, mem_singleton]
intro i
rw [mem_union, mem_union]
apply Or.imp id
on_goal 2 => rw [vars_X, disjoint_singleton_left]
all_goals
intro H
replace H := vars_sum_subset _ _ H
rw [mem_biUnion] at H
rcases H with ⟨j, hj, H⟩
rw [vars_C_mul] at H
swap
· apply pow_ne_zero
exact mod_cast hp.1.ne_zero
rw [mem_range] at hj
replace H := (ih j hj).2 (vars_pow _ _ H)
rw [mem_range] at H
· rw [mem_range]
cutsat
· cutsat
