p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)) →
      n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
apply Nat.strongInductionOn n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)) →
      n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)) →
      n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
clear n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)) →
      n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
intro n ih
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n

case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ vars (xInTermsOfW p ℚ n) ∧ vars (xInTermsOfW p ℚ n) ⊆ range (n + 1)
rw [xInTermsOfW_eq, mul_comm, vars_C_mul _ (nonzero_of_invertible _),
  vars_sub_of_disjoint, vars_X, range_succ, insert_eq]
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n

case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n

case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
on_goal 1 =>
  simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
  intro i
  rw [mem_union, mem_union]
  apply Or.imp id
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n

case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n

case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
on_goal 2 => rw [vars_X, disjoint_singleton_left]
case intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i ∈ range n

case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n

case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
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
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
case intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i ∈ range n

case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
. rw [mem_range]
  linarith
no goals
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
. linarith
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) ⊆ {n} ∪ range n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n
simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∪ range n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) ⊆ {n} ∪ range n
intro i
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∨ i ∈ range n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∪ range n
rw [mem_union, mem_union]
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∨ i ∈ range n
apply Or.imp id
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) ⊆ {n} ∪ range n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ n ∈ {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ∧
    {n} ∪ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) ⊆ {n} ∪ range n
simp only [true_and_iff, true_or_iff, eq_self_iff_true, mem_union, mem_singleton]
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∪ range n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) ⊆ {n} ∪ range n
intro i
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∨ i ∈ range n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∪ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∪ range n
rw [mem_union, mem_union]
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ range n
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i : ℕ
⊢ i ∈ {n} ∨ i ∈ vars (∑ x in range n, ↑C (↑p ^ x) * xInTermsOfW p ℚ x ^ p ^ (n - x)) → i ∈ {n} ∨ i ∈ range n
apply Or.imp id
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
rw [vars_X, disjoint_singleton_left]
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ Disjoint (vars (X n)) (vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)))
rw [vars_X, disjoint_singleton_left]
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ False
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
⊢ ¬n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
intro H
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : n ∈ Finset.biUnion (range n) fun i => vars (↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ False
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : n ∈ vars (∑ i in range n, ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ False
replace H := vars_sum_subset _ _ H
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : ∃ a, a ∈ range n ∧ n ∈ vars (↑C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a))
⊢ False
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : n ∈ Finset.biUnion (range n) fun i => vars (↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ False
rw [mem_biUnion] at H
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
case hpq
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
H : ∃ a, a ∈ range n ∧ n ∈ vars (↑C (↑p ^ a) * xInTermsOfW p ℚ a ^ p ^ (n - a))
⊢ False
rcases H with ⟨j, hj, H⟩
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False

case hpq.intro.intro.ha
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
rw [vars_C_mul] at H
case hpq.intro.intro.ha
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0

case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False

case hpq.intro.intro.ha
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
swap
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
case hpq.intro.intro.ha
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0

case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
. apply pow_ne_zero
  exact_mod_cast hp.1.ne_zero
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
rw [mem_range] at hj
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ range (j + 1)
⊢ False
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ vars (xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ False
replace H := (ih j hj).2 (vars_pow _ _ H)
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n ∈ range (j + 1)
⊢ False
rw [mem_range] at H
case hpq.intro.intro.ha.h
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ≠ 0
case hpq.intro.intro.ha
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ^ j ≠ 0
apply pow_ne_zero
no goals
case hpq.intro.intro.ha.h
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ vars (↑C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j))
⊢ ↑p ≠ 0
exact_mod_cast hp.1.ne_zero
case intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i < n
case intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i ∈ range n
rw [mem_range]
no goals
case intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
i j : ℕ
hj : j < n
H : i < j + 1
⊢ i < n
linarith
no goals
case hpq.intro.intro
p : ℕ
R : Type ?u.289237
inst✝¹ : CommRing R
inst✝ : DecidableEq R
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (m : ℕ), m < n → m ∈ vars (xInTermsOfW p ℚ m) ∧ vars (xInTermsOfW p ℚ m) ⊆ range (m + 1)
j : ℕ
hj : j < n
H : n < j + 1
⊢ False
linarith