p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)) ⊆
    Finset.univ ×ˢ Finset.range (n + 1)
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ vars (wittStructureRat p Φ n) ⊆ Finset.univ ×ˢ Finset.range (n + 1)
rw [wittStructureRat]
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
⊢ x ∈ Finset.univ ×ˢ Finset.range (n + 1)
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)) ⊆
    Finset.univ ×ˢ Finset.range (n + 1)
intro x hx
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
⊢ x.snd < n + 1
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
⊢ x ∈ Finset.univ ×ˢ Finset.range (n + 1)
simp only [Finset.mem_product, true_and_iff, Finset.mem_univ, Finset.mem_range]
case intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' : x ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
⊢ x.snd < n + 1
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
⊢ x.snd < n + 1
obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx
case intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' : x ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
i : idx
hx'' : x ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ x.snd < n + 1
case intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' : x ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
⊢ x.snd < n + 1
obtain ⟨i, -, hx''⟩ := mem_vars_bind₁ _ _ hx'
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j ∈ vars (W_ ℚ k)
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ (i, j).snd < n + 1
case intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
hx' : x ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
i : idx
hx'' : x ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ x.snd < n + 1
obtain ⟨j, hj, rfl⟩ := mem_vars_rename _ _ hx''
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ (i, j).snd < n + 1
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j ∈ vars (W_ ℚ k)
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ (i, j).snd < n + 1
rw [wittPolynomial_vars, Finset.mem_range] at hj
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
hk : k ∈ Finset.range (n + 1)
⊢ (i, j).snd < n + 1
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ vars (xInTermsOfW p ℚ n)
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
⊢ (i, j).snd < n + 1
replace hk := xInTermsOfW_vars_subset p _ hk
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
hk : k < n + 1
⊢ (i, j).snd < n + 1
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
hk : k ∈ Finset.range (n + 1)
⊢ (i, j).snd < n + 1
rw [Finset.mem_range] at hk
no goals
case intro.intro.intro.intro.intro.intro
p : ℕ
R : Type ?u.2115631
idx : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ vars (↑(bind₁ fun k => ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n))
hx' : (i, j) ∈ vars (↑(bind₁ fun i => ↑(rename (Prod.mk i)) (W_ ℚ k)) Φ)
hx'' : (i, j) ∈ vars (↑(rename (Prod.mk i)) (W_ ℚ k))
hk : k < n + 1
⊢ (i, j).snd < n + 1
exact lt_of_lt_of_le hj hk