[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (wittPolyProd p n) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
rw [wittPolyProd]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ n) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ n)) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
apply Subset.trans (vars_mul _ _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ n)) ∪ vars (↑(rename (Prod.mk 1)) (wittPolynomial p ℤ n)) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
refine' union_subset _ _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ n)) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
refine' Subset.trans (vars_rename _ _) _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ image (Prod.mk 0) (vars (wittPolynomial p ℤ n)) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
simp [wittPolynomial_vars, image_subset_iff]
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (↑(rename (Prod.mk 1)) (wittPolynomial p ℤ n)) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
refine' Subset.trans (vars_rename _ _) _
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ image (Prod.mk 1) (vars (wittPolynomial p ℤ n)) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
simp [wittPolynomial_vars, image_subset_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (wittPolyProdRemainder p n) ⊆ univ ×ˢ range n
[PROOFSTEP]
rw [wittPolyProdRemainder]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (∑ i in range n, ↑p ^ i * wittMul p i ^ p ^ (n - i)) ⊆ univ ×ˢ range n
[PROOFSTEP]
refine' Subset.trans (vars_sum_subset _ _) _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ (Finset.biUnion (range n) fun i => vars (↑p ^ i * wittMul p i ^ p ^ (n - i))) ⊆ univ ×ˢ range n
[PROOFSTEP]
rw [biUnion_subset]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → vars (↑p ^ x * wittMul p x ^ p ^ (n - x)) ⊆ univ ×ˢ range n
[PROOFSTEP]
intro x hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ vars (↑p ^ x * wittMul p x ^ p ^ (n - x)) ⊆ univ ×ˢ range n
[PROOFSTEP]
apply Subset.trans (vars_mul _ _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ vars (↑p ^ x) ∪ vars (wittMul p x ^ p ^ (n - x)) ⊆ univ ×ˢ range n
[PROOFSTEP]
refine' union_subset _ _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ vars (↑p ^ x) ⊆ univ ×ˢ range n
[PROOFSTEP]
apply Subset.trans (vars_pow _ _)
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ vars ↑p ⊆ univ ×ˢ range n
[PROOFSTEP]
have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_ofNat, eq_intCast]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ ↑p = ↑C ↑p
[PROOFSTEP]
simp only [Int.cast_ofNat, eq_intCast]
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
this : ↑p = ↑C ↑p
⊢ vars ↑p ⊆ univ ×ˢ range n
[PROOFSTEP]
rw [this, vars_C]
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
this : ↑p = ↑C ↑p
⊢ ∅ ⊆ univ ×ˢ range n
[PROOFSTEP]
apply empty_subset
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ vars (wittMul p x ^ p ^ (n - x)) ⊆ univ ×ˢ range n
[PROOFSTEP]
apply Subset.trans (vars_pow _ _)
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ vars (wittMul p x) ⊆ univ ×ˢ range n
[PROOFSTEP]
apply Subset.trans (wittMul_vars _ _)
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ univ ×ˢ range (x + 1) ⊆ univ ×ˢ range n
[PROOFSTEP]
apply product_subset_product (Subset.refl _)
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range n
⊢ range (x + 1) ⊆ range n
[PROOFSTEP]
simp only [mem_range, range_subset] at hx ⊢
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x < n
⊢ x + 1 ≤ n
[PROOFSTEP]
exact hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (remainder p n) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
rw [remainder]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars
      ((∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
        ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
apply Subset.trans (vars_mul _ _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ∪
      vars (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
refine' union_subset _ _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
refine' Subset.trans (vars_sum_subset _ _) _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ (Finset.biUnion (range (n + 1)) fun i =>
      vars (↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)))) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
rw [biUnion_subset]
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (n + 1) →
      vars (↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ vars (↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.single (0, x) (p ^ (n + 1 - x))).support ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
apply Subset.trans Finsupp.support_single_subset
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ {(0, x)} ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
simpa using mem_range.mp hx
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case refine'_1.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.out.ne_zero
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
refine' Subset.trans (vars_sum_subset _ _) _
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ (Finset.biUnion (range (n + 1)) fun i =>
      vars (↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i)))) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
rw [biUnion_subset]
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (n + 1) →
      vars (↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ vars (↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.single (1, x) (p ^ (n + 1 - x))).support ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
apply Subset.trans Finsupp.support_single_subset
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ {(1, x)} ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
simpa using mem_range.mp hx
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case refine'_2.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.out.ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ∑ i in range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) = wittPolyProd p n
[PROOFSTEP]
simp only [wittPolyProd]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ∑ i in range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) =
    ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ n) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ n)
[PROOFSTEP]
convert wittStructureInt_prop p (X (0 : Fin 2) * X 1) n using 1
[GOAL]
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ∑ i in range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) =
    ↑(bind₁ (wittStructureInt p (X 0 * X 1))) (wittPolynomial p ℤ n)
[PROOFSTEP]
simp only [wittPolynomial, wittMul]
[GOAL]
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ∑ x in range (n + 1), ↑p ^ x * wittStructureInt p (X 0 * X 1) x ^ p ^ (n - x) =
    ↑(bind₁ (wittStructureInt p (X 0 * X 1)))
      (∑ x in range (n + 1), ↑(monomial (Finsupp.single x (p ^ (n - x)))) (↑p ^ x))
[PROOFSTEP]
rw [AlgHom.map_sum]
[GOAL]
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ∑ x in range (n + 1), ↑p ^ x * wittStructureInt p (X 0 * X 1) x ^ p ^ (n - x) =
    ∑ x in range (n + 1),
      ↑(bind₁ (wittStructureInt p (X 0 * X 1))) (↑(monomial (Finsupp.single x (p ^ (n - x)))) (↑p ^ x))
[PROOFSTEP]
congr 1 with i
[GOAL]
case h.e'_2.e_f.h.a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i)) =
    MvPolynomial.coeff m✝
      (↑(bind₁ (wittStructureInt p (X 0 * X 1))) (↑(monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)))
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_2.e_f.h.a.e_p
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    ↑(bind₁ (wittStructureInt p (X 0 * X 1))) (↑(monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))
[PROOFSTEP]
have hsupp : (Finsupp.single i (p ^ (n - i))).support = { i } :=
  by
  rw [Finsupp.support_eq_singleton]
  simp only [and_true_iff, Finsupp.single_eq_same, eq_self_iff_true, Ne.def]
  exact pow_ne_zero _ hp.out.ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ (Finsupp.single i (p ^ (n - i))).support = {i}
[PROOFSTEP]
rw [Finsupp.support_eq_singleton]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ↑(Finsupp.single i (p ^ (n - i))) i ≠ 0 ∧
    Finsupp.single i (p ^ (n - i)) = Finsupp.single i (↑(Finsupp.single i (p ^ (n - i))) i)
[PROOFSTEP]
simp only [and_true_iff, Finsupp.single_eq_same, eq_self_iff_true, Ne.def]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ¬p ^ (n - i) = 0
[PROOFSTEP]
exact pow_ne_zero _ hp.out.ne_zero
[GOAL]
case h.e'_2.e_f.h.a.e_p
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
hsupp : (Finsupp.single i (p ^ (n - i))).support = {i}
⊢ ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    ↑(bind₁ (wittStructureInt p (X 0 * X 1))) (↑(monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))
[PROOFSTEP]
simp only [bind₁_monomial, hsupp, Int.cast_ofNat, prod_singleton, eq_intCast, Finsupp.single_eq_same, C_pow,
  mul_eq_mul_left_iff, true_or_iff, eq_self_iff_true, Int.cast_pow]
[GOAL]
case h.e'_3
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ n) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ n) =
    ↑(bind₁ fun i => ↑(rename (Prod.mk i)) (wittPolynomial p ℤ n)) (X 0 * X 1)
[PROOFSTEP]
simp only [map_mul, bind₁_X_right]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ n * wittMul p n + wittPolyProdRemainder p n = wittPolyProd p n
[PROOFSTEP]
convert mul_polyOfInterest_aux1 p n
[GOAL]
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ n * wittMul p n + wittPolyProdRemainder p n = ∑ i in range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i)
[PROOFSTEP]
rw [sum_range_succ, add_comm, Nat.sub_self, pow_zero, pow_one]
[GOAL]
case h.e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ wittPolyProdRemainder p n + ↑p ^ n * wittMul p n =
    ∑ x in range n, ↑p ^ x * wittMul p x ^ p ^ (n - x) + ↑p ^ n * wittMul p n
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n
[PROOFSTEP]
have mvpz : (p : 𝕄) ^ (n + 1) = MvPolynomial.C ((p : ℤ) ^ (n + 1)) := by simp only;
  norm_cast
    -- Porting note: the original proof applies `sum_range_succ` through a non-`conv` rewrite,
      -- but this does not work in Lean 4; the whole proof also times out very badly. The proof has been
      -- nearly totally rewritten here and now finishes quite fast.
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
[PROOFSTEP]
simp only
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
[PROOFSTEP]
norm_cast
  -- Porting note: the original proof applies `sum_range_succ` through a non-`conv` rewrite,
    -- but this does not work in Lean 4; the whole proof also times out very badly. The proof has been
    -- nearly totally rewritten here and now finishes quite fast.
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n
[PROOFSTEP]
rw [wittPolyProd, wittPolynomial, AlgHom.map_sum, AlgHom.map_sum]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ (∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
      ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x in range (n + 1 + 1),
              ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n
[PROOFSTEP]
conv_lhs =>
  arg 1
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| (∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
    ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
  arg 1
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| (∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
    ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
  arg 1
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| (∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
    ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
arg 1
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1)) *
      ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x in range (n + 1 + 1),
              ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n
[PROOFSTEP]
conv_lhs =>
  arg 2
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (0, n + 1)) *
    ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
  arg 2
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (0, n + 1)) *
    ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
  arg 2
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (0, n + 1)) *
    ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
arg 2
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1)) *
      (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x in range (n + 1 + 1),
              ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n
[PROOFSTEP]
conv_rhs =>
  enter [1, 1, 2, 2]
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n
[PROOFSTEP]
  enter [1, 1, 2, 2]
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n
[PROOFSTEP]
  enter [1, 1, 2, 2]
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n
[PROOFSTEP]
enter [1, 1, 2, 2]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1)) *
      (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
              ↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      remainder p n
[PROOFSTEP]
conv_rhs =>
  enter [1, 2, 2]
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n
[PROOFSTEP]
  enter [1, 2, 2]
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n
[PROOFSTEP]
  enter [1, 2, 2]
  rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n
[PROOFSTEP]
enter [1, 2, 2]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
| ∑ x in range (n + 1 + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
[PROOFSTEP]
rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul, rename_C, rename_X, ← mvpz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1)) *
      (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (1, n + 1)) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) *
            (∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
              ↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) *
          (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (0, n + 1)) +
      remainder p n
[PROOFSTEP]
simp only [add_mul, mul_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (0, n + 1) *
              ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) +
        (↑p ^ (n + 1) * X (1, n + 1) *
            ∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))) +
      remainder p n
[PROOFSTEP]
rw [add_comm _ (remainder p n)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    remainder p n +
      (-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (0, n + 1) *
              ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) +
        (↑p ^ (n + 1) * X (1, n + 1) *
            ∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))))
[PROOFSTEP]
simp only [add_assoc]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ (∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
        ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      (↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ((∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
            (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)))) =
    remainder p n +
      (-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        (↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) +
            (↑p ^ (n + 1) * X (1, n + 1) *
                ∑ x in range (n + 1),
                  ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
              ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))))))
[PROOFSTEP]
apply congrArg (Add.add _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
mvpz : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) * X (0, n + 1) *
        ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
      (↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x in range (n + 1), ↑(rename (Prod.mk 1)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (1, n + 1) *
              ∑ x in range (n + 1), ↑(rename (Prod.mk 0)) (↑(monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1)))))
[PROOFSTEP]
ring
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      (remainder p n - wittPolyProdRemainder p (n + 1))
[PROOFSTEP]
rw [← add_sub_assoc, eq_sub_iff_add_eq, mul_polyOfInterest_aux2]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      remainder p n
[PROOFSTEP]
exact mul_polyOfInterest_aux3 _ _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)
[PROOFSTEP]
simp only [polyOfInterest, mul_sub, mul_add, sub_eq_iff_eq_add']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) + ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))
[PROOFSTEP]
rw [mul_polyOfInterest_aux4 p n]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
            ↑p ^ (n + 1) * X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
          ↑p ^ (n + 1) * X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
        (remainder p n - wittPolyProdRemainder p (n + 1)) +
      ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))
[PROOFSTEP]
ring
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (↑p ^ (n + 1) * polyOfInterest p n) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
rw [mul_polyOfInterest_aux5]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (remainder p n - wittPolyProdRemainder p (n + 1)) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
apply Subset.trans (vars_sub_subset _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (remainder p n) ∪ vars (wittPolyProdRemainder p (n + 1)) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
refine' union_subset _ _
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (remainder p n) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
apply remainder_vars
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (wittPolyProdRemainder p (n + 1)) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
apply wittPolyProdRemainder_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (polyOfInterest p n) =
    vars
      (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))))
[PROOFSTEP]
have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by simp only; norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
[PROOFSTEP]
simp only
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
this : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ vars (polyOfInterest p n) =
    vars
      (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))))
[PROOFSTEP]
rw [polyOfInterest, this, vars_C_mul]
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
this : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
this : ↑p ^ (n + 1) = ↑C (↑p ^ (n + 1))
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.out.ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars (polyOfInterest p n) ⊆ univ ×ˢ range (n + 1)
[PROOFSTEP]
rw [polyOfInterest_vars_eq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
⊢ vars
      (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * ↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * ↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))) ⊆
    univ ×ˢ range (n + 1)
[PROOFSTEP]
apply mul_polyOfInterest_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ peval (polyOfInterest p n) ![fun i => coeff x i, fun i => coeff y i] =
    coeff (x * y) (n + 1) + ↑(p ^ (n + 1)) * coeff x (n + 1) * coeff y (n + 1) -
        coeff y (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff x i ^ p ^ (n + 1 - i) -
      coeff x (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff y i ^ p ^ (n + 1 - i)
[PROOFSTEP]
simp only [polyOfInterest, peval, map_natCast, Matrix.head_cons, map_pow, Function.uncurry_apply_pair, aeval_X,
  Matrix.cons_val_one, map_mul, Matrix.cons_val_zero, map_sub]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        coeff x (n + 1) *
          ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
            (↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) -
      coeff y (n + 1) *
        ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
          (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) =
    coeff (x * y) (n + 1) + ↑(p ^ (n + 1)) * coeff x (n + 1) * coeff y (n + 1) -
        coeff y (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff x i ^ p ^ (n + 1 - i) -
      coeff x (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff y i ^ p ^ (n + 1 - i)
[PROOFSTEP]
rw [sub_sub, add_comm (_ * _), ← sub_sub]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        coeff y (n + 1) *
          ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
            (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) -
      coeff x (n + 1) *
        ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
          (↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) =
    coeff (x * y) (n + 1) + ↑(p ^ (n + 1)) * coeff x (n + 1) * coeff y (n + 1) -
        coeff y (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff x i ^ p ^ (n + 1 - i) -
      coeff x (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff y i ^ p ^ (n + 1 - i)
[PROOFSTEP]
have mvpz : (p : MvPolynomial ℕ ℤ) = MvPolynomial.C ↑p := by rw [eq_intCast, Int.cast_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ ↑p = ↑C ↑p
[PROOFSTEP]
rw [eq_intCast, Int.cast_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
mvpz : ↑p = ↑C ↑p
⊢ ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        coeff y (n + 1) *
          ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
            (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) -
      coeff x (n + 1) *
        ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
          (↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) =
    coeff (x * y) (n + 1) + ↑(p ^ (n + 1)) * coeff x (n + 1) * coeff y (n + 1) -
        coeff y (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff x i ^ p ^ (n + 1 - i) -
      coeff x (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff y i ^ p ^ (n + 1 - i)
[PROOFSTEP]
have : ∀ (f : ℤ →+* k) (g : ℕ → k), eval₂ f g p = f p := by intros; rw [mvpz, MvPolynomial.eval₂_C]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
mvpz : ↑p = ↑C ↑p
⊢ ∀ (f : ℤ →+* k) (g : ℕ → k), eval₂ f g ↑p = ↑f ↑p
[PROOFSTEP]
intros
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
mvpz : ↑p = ↑C ↑p
f✝ : ℤ →+* k
g✝ : ℕ → k
⊢ eval₂ f✝ g✝ ↑p = ↑f✝ ↑p
[PROOFSTEP]
rw [mvpz, MvPolynomial.eval₂_C]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
mvpz : ↑p = ↑C ↑p
this : ∀ (f : ℤ →+* k) (g : ℕ → k), eval₂ f g ↑p = ↑f ↑p
⊢ ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        coeff y (n + 1) *
          ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
            (↑(rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) -
      coeff x (n + 1) *
        ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i]))
          (↑(rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) =
    coeff (x * y) (n + 1) + ↑(p ^ (n + 1)) * coeff x (n + 1) * coeff y (n + 1) -
        coeff y (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff x i ^ p ^ (n + 1 - i) -
      coeff x (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff y i ^ p ^ (n + 1 - i)
[PROOFSTEP]
simp [wittPolynomial_eq_sum_C_mul_X_pow, aeval, eval₂_rename, this, mul_coeff, peval, map_natCast, map_add, map_pow,
  map_mul]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
⊢ peval (polyOfInterest p n) ![fun i => coeff x i, fun i => coeff y i] =
    coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
rw [peval_polyOfInterest]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
⊢ coeff (x * y) (n + 1) + ↑(p ^ (n + 1)) * coeff x (n + 1) * coeff y (n + 1) -
        coeff y (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff x i ^ p ^ (n + 1 - i) -
      coeff x (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff y i ^ p ^ (n + 1 - i) =
    coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
have : (p : k) = 0 := CharP.cast_eq_zero k p
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
⊢ coeff (x * y) (n + 1) + ↑(p ^ (n + 1)) * coeff x (n + 1) * coeff y (n + 1) -
        coeff y (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff x i ^ p ^ (n + 1 - i) -
      coeff x (n + 1) * ∑ i in range (n + 1 + 1), ↑(p ^ i) * coeff y i ^ p ^ (n + 1 - i) =
    coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
simp only [this, Nat.cast_pow, ne_eq, add_eq_zero, and_false, zero_pow', zero_mul, add_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
⊢ coeff (x * y) (n + 1) - coeff y (n + 1) * ∑ x_1 in range (n + 1 + 1), 0 ^ x_1 * coeff x x_1 ^ p ^ (n + 1 - x_1) -
      coeff x (n + 1) * ∑ x in range (n + 1 + 1), 0 ^ x * coeff y x ^ p ^ (n + 1 - x) =
    coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
have sum_zero_pow_mul_pow_p :
  ∀ y : 𝕎 k, ∑ x : ℕ in range (n + 1 + 1), (0 : k) ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1) :=
  by
  intro y
  rw [Finset.sum_eq_single_of_mem 0]
  · simp
  · simp
  · intro j _ hj
    simp [zero_pow (zero_lt_iff.mpr hj)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
⊢ ∀ (y : 𝕎 k), ∑ x in range (n + 1 + 1), 0 ^ x * coeff y x ^ p ^ (n + 1 - x) = coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
intro y
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ ∑ x in range (n + 1 + 1), 0 ^ x * coeff y x ^ p ^ (n + 1 - x) = coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
rw [Finset.sum_eq_single_of_mem 0]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ 0 ^ 0 * coeff y 0 ^ p ^ (n + 1 - 0) = coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
simp
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ 0 ∈ range (n + 1 + 1)
[PROOFSTEP]
simp
[GOAL]
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ ∀ (b : ℕ), b ∈ range (n + 1 + 1) → b ≠ 0 → 0 ^ b * coeff y b ^ p ^ (n + 1 - b) = 0
[PROOFSTEP]
intro j _ hj
[GOAL]
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
j : ℕ
a✝ : j ∈ range (n + 1 + 1)
hj : j ≠ 0
⊢ 0 ^ j * coeff y j ^ p ^ (n + 1 - j) = 0
[PROOFSTEP]
simp [zero_pow (zero_lt_iff.mpr hj)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x in range (n + 1 + 1), 0 ^ x * coeff y x ^ p ^ (n + 1 - x) = coeff y 0 ^ p ^ (n + 1)
⊢ coeff (x * y) (n + 1) - coeff y (n + 1) * ∑ x_1 in range (n + 1 + 1), 0 ^ x_1 * coeff x x_1 ^ p ^ (n + 1 - x_1) -
      coeff x (n + 1) * ∑ x in range (n + 1 + 1), 0 ^ x * coeff y x ^ p ^ (n + 1 - x) =
    coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x in range (n + 1 + 1), 0 ^ x * coeff y x ^ p ^ (n + 1 - x) = coeff y 0 ^ p ^ (n + 1)
⊢ ∑ x_1 in range (n + 1 + 1), 0 ^ x_1 * coeff x x_1 ^ p ^ (n + 1 - x_1) = coeff x 0 ^ p ^ (n + 1)
[PROOFSTEP]
apply sum_zero_pow_mul_pow_p
[GOAL]
case e_a.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x in range (n + 1 + 1), 0 ^ x * coeff y x ^ p ^ (n + 1 - x) = coeff y 0 ^ p ^ (n + 1)
⊢ ∑ x in range (n + 1 + 1), 0 ^ x * coeff y x ^ p ^ (n + 1 - x) = coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
apply sum_zero_pow_mul_pow_p
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
[PROOFSTEP]
simp only [← peval_polyOfInterest']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun i => coeff x i, fun i => coeff y i]
[PROOFSTEP]
obtain ⟨f₀, hf₀⟩ := exists_restrict_to_vars k (polyOfInterest_vars p n)
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun i => coeff x i, fun i => coeff y i]
[PROOFSTEP]
have : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b := fun a b => rfl
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun i => coeff x i, fun i => coeff y i]
[PROOFSTEP]
let f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  by
  intro x y
  apply f₀
  rintro ⟨a, ha⟩
  apply Function.uncurry ![x, y]
  simp_rw [product_val, this, Multiset.mem_product, mem_univ_val, true_and_iff, range_val, Multiset.range_succ,
    Multiset.mem_cons, Multiset.mem_range] at ha 
  refine' ⟨a.fst, ⟨a.snd, _⟩⟩
  cases' ha with ha ha <;> linarith only [ha]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
⊢ TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
[PROOFSTEP]
intro x y
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
x y : TruncatedWittVector p (n + 1) k
⊢ k
[PROOFSTEP]
apply f₀
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
x y : TruncatedWittVector p (n + 1) k
⊢ (↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ fun a => a ∈ (univ ×ˢ range (n + 1)).val
⊢ k
[PROOFSTEP]
apply Function.uncurry ![x, y]
[GOAL]
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ fun a => a ∈ (univ ×ˢ range (n + 1)).val
⊢ Fin (Nat.succ (Nat.succ 0)) × Fin (n + 1)
[PROOFSTEP]
simp_rw [product_val, this, Multiset.mem_product, mem_univ_val, true_and_iff, range_val, Multiset.range_succ,
  Multiset.mem_cons, Multiset.mem_range] at ha 
[GOAL]
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ fun a => a.snd = n ∨ a.snd < n
⊢ Fin (Nat.succ (Nat.succ 0)) × Fin (n + 1)
[PROOFSTEP]
refine' ⟨a.fst, ⟨a.snd, _⟩⟩
[GOAL]
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ fun a => a.snd = n ∨ a.snd < n
⊢ a.snd < n + 1
[PROOFSTEP]
cases' ha with ha ha
[GOAL]
case mk.inl
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a.snd = n
⊢ a.snd < n + 1
[PROOFSTEP]
linarith only [ha]
[GOAL]
case mk.inr
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a.snd < n
⊢ a.snd < n + 1
[PROOFSTEP]
linarith only [ha]
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun i => coeff x i, fun i => coeff y i]
[PROOFSTEP]
use f
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
⊢ ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      peval (polyOfInterest p n) ![fun i => coeff x i, fun i => coeff y i]
[PROOFSTEP]
intro x y
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
⊢ f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
    peval (polyOfInterest p n) ![fun i => coeff x i, fun i => coeff y i]
[PROOFSTEP]
dsimp [peval]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
⊢ (f₀ fun a =>
      Matrix.vecCons (truncateFun (n + 1) x) ![truncateFun (n + 1) y] (↑a).fst
        { val := (↑a).snd, isLt := (_ : (↑a).snd < n + 1) }) =
    ↑(aeval (Function.uncurry ![fun i => coeff x i, fun i => coeff y i])) (polyOfInterest p n)
[PROOFSTEP]
rw [← hf₀]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
⊢ (f₀ fun a =>
      Matrix.vecCons (truncateFun (n + 1) x) ![truncateFun (n + 1) y] (↑a).fst
        { val := (↑a).snd, isLt := (_ : (↑a).snd < n + 1) }) =
    f₀ (Function.uncurry ![fun i => coeff x i, fun i => coeff y i] ∘ Subtype.val)
[PROOFSTEP]
congr
[GOAL]
case h.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
⊢ (fun a =>
      Matrix.vecCons (truncateFun (n + 1) x) ![truncateFun (n + 1) y] (↑a).fst
        { val := (↑a).snd, isLt := (_ : (↑a).snd < n + 1) }) =
    Function.uncurry ![fun i => coeff x i, fun i => coeff y i] ∘ Subtype.val
[PROOFSTEP]
ext a
[GOAL]
case h.e_a.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
a : ↑fun a => a ∈ univ.val ×ˢ Multiset.range (n + 1)
⊢ Matrix.vecCons (truncateFun (n + 1) x) ![truncateFun (n + 1) y] (↑a).fst
      { val := (↑a).snd, isLt := (_ : (↑a).snd < n + 1) } =
    (Function.uncurry ![fun i => coeff x i, fun i => coeff y i] ∘ Subtype.val) a
[PROOFSTEP]
cases' a with a ha
[GOAL]
case h.e_a.h.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
a : Fin 2 × ℕ
ha : a ∈ fun a => a ∈ univ.val ×ˢ Multiset.range (n + 1)
⊢ Matrix.vecCons (truncateFun (n + 1) x) ![truncateFun (n + 1) y] (↑{ val := a, property := ha }).fst
      { val := (↑{ val := a, property := ha }).snd, isLt := (_ : (↑{ val := a, property := ha }).snd < n + 1) } =
    (Function.uncurry ![fun i => coeff x i, fun i => coeff y i] ∘ Subtype.val) { val := a, property := ha }
[PROOFSTEP]
cases' a with i m
[GOAL]
case h.e_a.h.mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
i : Fin 2
m : ℕ
ha : (i, m) ∈ fun a => a ∈ univ.val ×ˢ Multiset.range (n + 1)
⊢ Matrix.vecCons (truncateFun (n + 1) x) ![truncateFun (n + 1) y] (↑{ val := (i, m), property := ha }).fst
      { val := (↑{ val := (i, m), property := ha }).snd,
        isLt := (_ : (↑{ val := (i, m), property := ha }).snd < n + 1) } =
    (Function.uncurry ![fun i => coeff x i, fun i => coeff y i] ∘ Subtype.val) { val := (i, m), property := ha }
[PROOFSTEP]
fin_cases i
[GOAL]
case h.e_a.h.mk.mk.head
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
m : ℕ
ha : ({ val := 0, isLt := (_ : 0 < 2) }, m) ∈ fun a => a ∈ univ.val ×ˢ Multiset.range (n + 1)
⊢ Matrix.vecCons (truncateFun (n + 1) x) ![truncateFun (n + 1) y]
      (↑{ val := ({ val := 0, isLt := (_ : 0 < 2) }, m), property := ha }).fst
      { val := (↑{ val := ({ val := 0, isLt := (_ : 0 < 2) }, m), property := ha }).snd,
        isLt := (_ : (↑{ val := ({ val := 0, isLt := (_ : 0 < 2) }, m), property := ha }).snd < n + 1) } =
    (Function.uncurry ![fun i => coeff x i, fun i => coeff y i] ∘ Subtype.val)
      { val := ({ val := 0, isLt := (_ : 0 < 2) }, m), property := ha }
[PROOFSTEP]
rfl
  -- surely this case split is not necessary
[GOAL]
case h.e_a.h.mk.mk.tail.head
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : ((↑fun a => a ∈ (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = ↑(aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = Multiset.product a b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha => Function.uncurry ![x, y] (a.fst, { val := a.snd, isLt := (_ : a.snd < n + 1) })
x y : 𝕎 k
m : ℕ
ha : ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, m) ∈ fun a => a ∈ univ.val ×ˢ Multiset.range (n + 1)
⊢ Matrix.vecCons (truncateFun (n + 1) x) ![truncateFun (n + 1) y]
      (↑{ val := ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, m), property := ha }).fst
      { val := (↑{ val := ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, m), property := ha }).snd,
        isLt := (_ : (↑{ val := ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, m), property := ha }).snd < n + 1) } =
    (Function.uncurry ![fun i => coeff x i, fun i => coeff y i] ∘ Subtype.val)
      { val := ({ val := 1, isLt := (_ : (fun a => a < 2) 1) }, m), property := ha }
[PROOFSTEP]
rfl
  -- surely this case split is not necessary
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      coeff (x * y) (n + 1) =
        coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1) + coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
[PROOFSTEP]
obtain ⟨f, hf⟩ := nth_mul_coeff' p k n
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      coeff (x * y) (n + 1) =
        coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1) + coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
[PROOFSTEP]
use f
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
⊢ ∀ (x y : 𝕎 k),
    coeff (x * y) (n + 1) =
      coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1) + coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) +
        f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
[PROOFSTEP]
intro x y
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
x y : 𝕎 k
⊢ coeff (x * y) (n + 1) =
    coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1) + coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) +
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
[PROOFSTEP]
rw [hf x y]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1)
x y : 𝕎 k
⊢ coeff (x * y) (n + 1) =
    coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1) + coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) +
      (coeff (x * y) (n + 1) - coeff y (n + 1) * coeff x 0 ^ p ^ (n + 1) - coeff x (n + 1) * coeff y 0 ^ p ^ (n + 1))
[PROOFSTEP]
ring
