-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem wittStructureRat_vars [Fintype idx] (Φ : MvPolynomial idx ℚ) (n : ℕ) :
    (wittStructureRat p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (wittStructureRat p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
rw [wittStructureRat]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars ⊆
    Finset.univ ×ˢ Finset.range (n + 1)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
⊢ x ∈ Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
simp only [Finset.mem_product, true_and, Finset.mem_univ, Finset.mem_range]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
⊢ x.2 < n + 1

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars ⊆
    Finset.univ ×ˢ Finset.range (n + 1)

Tactic:
intro x hx

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
⊢ x ∈ Finset.univ ×ˢ Finset.range (n + 1)

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
hk : k < n + 1
⊢ (i, j).2 < n + 1

Tactic:
exact lt_of_lt_of_le hj hk

Result:
no goals

Proof state:
case intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
hx' : x ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
i : idx
hx'' : x ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ x.2 < n + 1

Tactic:
obtain ⟨j, hj, rfl⟩ := mem_vars_rename _ _ hx''

Result:
case intro.intro.intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
i : idx
j : ℕ
hj : j ∈ (W_ ℚ k).vars
hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ (i, j).2 < n + 1

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
i : idx
j : ℕ
hj : j ∈ (W_ ℚ k).vars
hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ (i, j).2 < n + 1

Tactic:
rw [wittPolynomial_vars, Finset.mem_range] at hj

Result:
case intro.intro.intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ (i, j).2 < n + 1

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ (i, j).2 < n + 1

Tactic:
replace hk := xInTermsOfW_vars_subset p _ hk

Result:
case intro.intro.intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
hk : k ∈ Finset.range (n + 1)
⊢ (i, j).2 < n + 1

Proof state:
case intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
hx' : x ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
⊢ x.2 < n + 1

Tactic:
obtain ⟨i, -, hx''⟩ := mem_vars_bind₁ _ _ hx'

Result:
case intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
hx' : x ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
i : idx
hx'' : x ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
⊢ x.2 < n + 1

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
hk : k ∈ Finset.range (n + 1)
⊢ (i, j).2 < n + 1

Tactic:
rw [Finset.mem_range] at hk

Result:
case intro.intro.intro.intro.intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n k : ℕ
i : idx
j : ℕ
hj : j < k + 1
hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars
hk : k < n + 1
⊢ (i, j).2 < n + 1

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
⊢ x.2 < n + 1

Tactic:
obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx

Result:
case intro.intro
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
inst✝ : Fintype idx
Φ : MvPolynomial idx ℚ
n : ℕ
x : idx × ℕ
hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars
k : ℕ
hk : k ∈ (xInTermsOfW p ℚ n).vars
hx' : x ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars
⊢ x.2 < n + 1