-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem remainder_vars (n : ℕ) : (remainder p n).vars ⊆ univ ×ˢ range (n + 1)

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

Tactic:
rw [remainder]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
        ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

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

Tactic:
apply pow_ne_zero

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

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
        ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

Tactic:
apply Subset.trans (vars_mul _ _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ∪
      (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range (n + 1)).biUnion fun i =>
      ((rename (Prod.mk 1)) ((monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i))).vars) ⊆
    univ ×ˢ range (n + 1)

Tactic:
rw [biUnion_subset]

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    ((rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)

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

Tactic:
simpa using mem_range.mp hx

Result:
no goals

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

Tactic:
exact mod_cast hp.out.ne_zero

Result:
no goals

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ((rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]

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

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

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

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range (n + 1)).biUnion fun i =>
      ((rename (Prod.mk 1)) ((monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i))).vars) ⊆
    univ ×ˢ range (n + 1)

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

Tactic:
apply Subset.trans Finsupp.support_single_subset

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

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    ((rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
intro x hx

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ((rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)