-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem wittPolyProdRemainder_vars (n : ℕ) :
    (wittPolyProdRemainder p n).vars ⊆ univ ×ˢ range n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range n).biUnion fun i => (↑p ^ i * wittMul p i ^ p ^ (n - i)).vars) ⊆ univ ×ˢ range n

Tactic:
rw [biUnion_subset]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range n, (↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (wittMul p x).vars ⊆ univ ×ˢ range n

Tactic:
apply Subset.trans (wittMul_vars _ _)

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ univ ×ˢ range (x + 1) ⊆ univ ×ˢ range n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ ↑p = C ↑p

Tactic:
simp only [Int.cast_natCast, eq_intCast]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p ^ x).vars ∪ (wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Tactic:
refine union_subset ?_ ?_

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p ^ x).vars ⊆ univ ×ˢ range n

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProdRemainder p n).vars ⊆ univ ×ˢ range n

Tactic:
rw [wittPolyProdRemainder]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ i ∈ range n, ↑p ^ i * wittMul p i ^ p ^ (n - i)).vars ⊆ univ ×ˢ range n

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x < n
⊢ x + 1 ≤ n

Tactic:
exact hx

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ i ∈ range n, ↑p ^ i * wittMul p i ^ p ^ (n - i)).vars ⊆ univ ×ˢ range n

Tactic:
refine Subset.trans (vars_sum_subset _ _) ?_

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range n).biUnion fun i => (↑p ^ i * wittMul p i ^ p ^ (n - i)).vars) ⊆ univ ×ˢ range n

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : ↑p = C ↑p
⊢ ∅ ⊆ univ ×ˢ range n

Tactic:
apply empty_subset

Result:
no goals

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ range (x + 1) ⊆ range n

Tactic:
simp only [mem_range, range_subset] at hx ⊢

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x < n
⊢ x + 1 ≤ n

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Tactic:
apply Subset.trans (vars_pow _ _)

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (wittMul p x).vars ⊆ univ ×ˢ range n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range n, (↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Tactic:
intro x hx

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ univ ×ˢ range (x + 1) ⊆ univ ×ˢ range n

Tactic:
apply product_subset_product (Subset.refl _)

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ range (x + 1) ⊆ range n

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p).vars ⊆ univ ×ˢ range n

Tactic:
have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_natCast, eq_intCast]

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : ↑p = C ↑p
⊢ (↑p).vars ⊆ univ ×ˢ range n

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : ↑p = C ↑p
⊢ (↑p).vars ⊆ univ ×ˢ range n

Tactic:
rw [this, vars_C]

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
this : ↑p = C ↑p
⊢ ∅ ⊆ univ ×ˢ range n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Tactic:
apply Subset.trans (vars_mul _ _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p ^ x).vars ∪ (wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p ^ x).vars ⊆ univ ×ˢ range n

Tactic:
apply Subset.trans (vars_pow _ _)

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p).vars ⊆ univ ×ˢ range n