[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


[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ ∀ {a b : R × S},
    a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}
[PROOFSTEP]
rintro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨ha₁, ha₂⟩ ⟨hb₁, hb₂⟩
[GOAL]
case mk.mk.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
a₁ : R
a₂ : S
b₁ : R
b₂ : S
ha₁ : (a₁, a₂).fst ∈ I
ha₂ : (a₁, a₂).snd ∈ J
hb₁ : (b₁, b₂).fst ∈ I
hb₂ : (b₁, b₂).snd ∈ J
⊢ (a₁, a₂) + (b₁, b₂) ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}
[PROOFSTEP]
exact ⟨I.add_mem ha₁ hb₁, J.add_mem ha₂ hb₂⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ 0 ∈
    { carrier := {x | x.fst ∈ I ∧ x.snd ∈ J},
        add_mem' :=
          (_ :
            ∀ {a b : R × S},
              a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} →
                b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}) }.carrier
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ ∀ (c : R × S) {x : R × S},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := {x | x.fst ∈ I ∧ x.snd ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {a b : R × S},
                        a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} →
                          b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}) },
              zero_mem' := (_ : 0 ∈ I ∧ 0 ∈ J) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := {x | x.fst ∈ I ∧ x.snd ∈ J},
                  add_mem' :=
                    (_ :
                      ∀ {a b : R × S},
                        a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} →
                          b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}) },
              zero_mem' := (_ : 0 ∈ I ∧ 0 ∈ J) }.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨hb₁, hb₂⟩
[GOAL]
case mk.mk.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
a₁ : R
a₂ : S
b₁ : R
b₂ : S
hb₁ : (b₁, b₂).fst ∈ I
hb₂ : (b₁, b₂).snd ∈ J
⊢ (a₁, a₂) • (b₁, b₂) ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | x.fst ∈ I ∧ x.snd ∈ J},
              add_mem' :=
                (_ :
                  ∀ {a b : R × S},
                    a ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} →
                      b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J} → a + b ∈ {x | x.fst ∈ I ∧ x.snd ∈ J}) },
          zero_mem' := (_ : 0 ∈ I ∧ 0 ∈ J) }.toAddSubsemigroup.carrier
[PROOFSTEP]
exact ⟨I.mul_mem_left _ hb₁, J.mul_mem_left _ hb₂⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ ∀ (x : R × S), x ∈ prod ⊤ ⊤ ↔ x ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ I = prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)
[PROOFSTEP]
apply Ideal.ext
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ ∀ (x : R × S), x ∈ I ↔ x ∈ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)
[PROOFSTEP]
rintro ⟨r, s⟩
[GOAL]
case h.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (r, s) ∈ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)
[PROOFSTEP]
rw [mem_prod, mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective,
  mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
[GOAL]
case h.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (∃ x, x ∈ I ∧ ↑(RingHom.fst R S) x = r) ∧ ∃ x, x ∈ I ∧ ↑(RingHom.snd R S) x = s
[PROOFSTEP]
refine' ⟨fun h => ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, _⟩
[GOAL]
case h.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
r : R
s : S
⊢ ((∃ x, x ∈ I ∧ ↑(RingHom.fst R S) x = r) ∧ ∃ x, x ∈ I ∧ ↑(RingHom.snd R S) x = s) → (r, s) ∈ I
[PROOFSTEP]
rintro ⟨⟨⟨r, s'⟩, ⟨h₁, rfl⟩⟩, ⟨⟨r', s⟩, ⟨h₂, rfl⟩⟩⟩
[GOAL]
case h.mk.intro.intro.mk.intro.intro.mk.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
r : R
s' : S
h₁ : (r, s') ∈ I
r' : R
s : S
h₂ : (r', s) ∈ I
⊢ (↑(RingHom.fst R S) (r, s'), ↑(RingHom.snd R S) (r', s)) ∈ I
[PROOFSTEP]
simpa using I.add_mem (I.mul_mem_left (1, 0) h₁) (I.mul_mem_left (0, 1) h₂)
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ map (RingHom.fst R S) (prod I J) = I
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R
⊢ x ∈ map (RingHom.fst R S) (prod I J) ↔ x ∈ I
[PROOFSTEP]
rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.fst R S) x_1 = x) ↔ x ∈ I
[PROOFSTEP]
exact
  ⟨by
    rintro ⟨x, ⟨h, rfl⟩⟩
    exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, rfl⟩⟩⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.fst R S) x_1 = x) → x ∈ I
[PROOFSTEP]
rintro ⟨x, ⟨h, rfl⟩⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ prod I J
⊢ ↑(RingHom.fst R S) x ∈ I
[PROOFSTEP]
exact h.1
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ map (RingHom.snd R S) (prod I J) = J
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ x ∈ map (RingHom.snd R S) (prod I J) ↔ x ∈ J
[PROOFSTEP]
rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.snd R S) x_1 = x) ↔ x ∈ J
[PROOFSTEP]
exact
  ⟨by
    rintro ⟨x, ⟨h, rfl⟩⟩
    exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1, x_1 ∈ prod I J ∧ ↑(RingHom.snd R S) x_1 = x) → x ∈ J
[PROOFSTEP]
rintro ⟨x, ⟨h, rfl⟩⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ prod I J
⊢ ↑(RingHom.snd R S) x ∈ J
[PROOFSTEP]
exact h.2
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ map (↑RingEquiv.prodComm) (prod I J) = prod J I
[PROOFSTEP]
refine' Trans.trans (ideal_prod_eq _) _
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
⊢ prod (map (RingHom.fst S R) (map (↑RingEquiv.prodComm) (prod I J)))
      (map (RingHom.snd S R) (map (↑RingEquiv.prodComm) (prod I J))) =
    prod J I
[PROOFSTEP]
simp [map_map]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
x✝ : Ideal R × Ideal S
I : Ideal R
J : Ideal S
⊢ (fun I => (map (RingHom.fst R S) I, map (RingHom.snd R S) I)) ((fun I => prod I.fst I.snd) (I, J)) = (I, J)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I'✝ : Ideal R
J✝ J'✝ : Ideal S
I I' : Ideal R
J J' : Ideal S
⊢ prod I J = prod I' J' ↔ I = I' ∧ J = J'
[PROOFSTEP]
simp only [← idealProdEquiv_symm_apply, idealProdEquiv.symm.injective.eq_iff, Prod.mk.inj_iff]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime (prod I ⊤)
⊢ IsPrime I
[PROOFSTEP]
constructor
[GOAL]
case ne_top'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime (prod I ⊤)
⊢ I ≠ ⊤
[PROOFSTEP]
contrapose! h
[GOAL]
case ne_top'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : I = ⊤
⊢ ¬IsPrime (prod I ⊤)
[PROOFSTEP]
rw [h, prod_top_top, isPrime_iff]
[GOAL]
case ne_top'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : I = ⊤
⊢ ¬(⊤ ≠ ⊤ ∧ ∀ {x y : R × S}, x * y ∈ ⊤ → x ∈ ⊤ ∨ y ∈ ⊤)
[PROOFSTEP]
simp [isPrime_iff, h]
[GOAL]
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime (prod I ⊤)
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
intro x y hxy
[GOAL]
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime (prod I ⊤)
x y : R
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
[PROOFSTEP]
have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤ :=
  by
  rw [Prod.mk_mul_mk, mul_one, mem_prod]
  exact ⟨hxy, trivial⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime (prod I ⊤)
x y : R
hxy : x * y ∈ I
⊢ (x, 1) * (y, 1) ∈ prod I ⊤
[PROOFSTEP]
rw [Prod.mk_mul_mk, mul_one, mem_prod]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime (prod I ⊤)
x y : R
hxy : x * y ∈ I
⊢ x * y ∈ I ∧ 1 ∈ ⊤
[PROOFSTEP]
exact ⟨hxy, trivial⟩
[GOAL]
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime (prod I ⊤)
x y : R
hxy : x * y ∈ I
this : (x, 1) * (y, 1) ∈ prod I ⊤
⊢ x ∈ I ∨ y ∈ I
[PROOFSTEP]
simpa using h.mem_or_mem this
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime (prod ⊤ I)
⊢ IsPrime I
[PROOFSTEP]
apply @isPrime_of_isPrime_prod_top _ R
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime (prod ⊤ I)
⊢ IsPrime (prod I ⊤)
[PROOFSTEP]
rw [← map_prodComm_prod]
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime (prod ⊤ I)
⊢ IsPrime (map (↑RingEquiv.prodComm) (prod ⊤ I))
[PROOFSTEP]
exact map_isPrime_of_equiv _
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
⊢ IsPrime (prod I ⊤)
[PROOFSTEP]
constructor
[GOAL]
case ne_top'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
⊢ prod I ⊤ ≠ ⊤
[PROOFSTEP]
rcases h with ⟨h, -⟩
[GOAL]
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : I ≠ ⊤
⊢ prod I ⊤ ≠ ⊤
[PROOFSTEP]
contrapose! h
[GOAL]
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : prod I ⊤ = ⊤
⊢ I = ⊤
[PROOFSTEP]
rw [← prod_top_top, prod.ext_iff] at h
[GOAL]
case ne_top'.mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : I = ⊤ ∧ ⊤ = ⊤
⊢ I = ⊤
[PROOFSTEP]
exact h.1
[GOAL]
case mem_or_mem'
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
⊢ ∀ {x y : R × S}, x * y ∈ prod I ⊤ → x ∈ prod I ⊤ ∨ y ∈ prod I ⊤
[PROOFSTEP]
rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨h₁, _⟩
[GOAL]
case mem_or_mem'.mk.mk.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤
[PROOFSTEP]
cases' h.mem_or_mem h₁ with h h
[GOAL]
case mem_or_mem'.mk.mk.intro.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h✝ : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
h : (r₁, s₁).fst ∈ I
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤
[PROOFSTEP]
exact Or.inl ⟨h, trivial⟩
[GOAL]
case mem_or_mem'.mk.mk.intro.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal R
h✝ : IsPrime I
r₁ : R
s₁ : S
r₂ : R
s₂ : S
h₁ : ((r₁, s₁) * (r₂, s₂)).fst ∈ I
right✝ : ((r₁, s₁) * (r₂, s₂)).snd ∈ ⊤
h : (r₂, s₂).fst ∈ I
⊢ (r₁, s₁) ∈ prod I ⊤ ∨ (r₂, s₂) ∈ prod I ⊤
[PROOFSTEP]
exact Or.inr ⟨h, trivial⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
⊢ IsPrime (prod ⊤ I)
[PROOFSTEP]
letI : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
this : IsPrime (prod I ⊤) := isPrime_ideal_prod_top
⊢ IsPrime (prod ⊤ I)
[PROOFSTEP]
rw [← map_prodComm_prod]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
this : IsPrime (prod I ⊤) := isPrime_ideal_prod_top
⊢ IsPrime (map (↑RingEquiv.prodComm) (prod I ⊤))
[PROOFSTEP]
apply map_isPrime_of_equiv _
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ IsPrime (prod I J) → I = ⊤ ∨ J = ⊤
[PROOFSTEP]
contrapose!
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬IsPrime (prod I J)
[PROOFSTEP]
simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ ¬1 ∈ I ∧ ¬1 ∈ J → ¬1 ∈ prod I J → ∃ x x_1 h, ¬x ∈ prod I J ∧ ¬x_1 ∈ prod I J
[PROOFSTEP]
exact fun ⟨hI, hJ⟩ _ => ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ (0, 1) * (1, 0) ∈ prod I J
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ ¬(0, 1) ∈ prod I J
[PROOFSTEP]
simp [hJ]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ ¬(1, 0) ∈ prod I J
[PROOFSTEP]
simp [hI]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ IsPrime I ↔ (∃ p, IsPrime p ∧ I = prod p ⊤) ∨ ∃ p, IsPrime p ∧ I = prod ⊤ p
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ IsPrime I → (∃ p, IsPrime p ∧ I = prod p ⊤) ∨ ∃ p, IsPrime p ∧ I = prod ⊤ p
[PROOFSTEP]
rw [ideal_prod_eq I]
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I)) →
    (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
      ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
[PROOFSTEP]
intro hI
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
[PROOFSTEP]
rcases ideal_prod_prime_aux hI with (h | h)
[GOAL]
case mp.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
[PROOFSTEP]
right
[GOAL]
case mp.inl.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
[PROOFSTEP]
rw [h] at hI ⊢
[GOAL]
case mp.inl.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod ⊤ (map (RingHom.snd R S) I))
h : map (RingHom.fst R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod ⊤ (map (RingHom.snd R S) I) = prod ⊤ p
[PROOFSTEP]
exact ⟨_, ⟨isPrime_of_isPrime_prod_top' hI, rfl⟩⟩
[GOAL]
case mp.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.snd R S) I = ⊤
⊢ (∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤) ∨
    ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod ⊤ p
[PROOFSTEP]
left
[GOAL]
case mp.inr.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I))
h : map (RingHom.snd R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) (map (RingHom.snd R S) I) = prod p ⊤
[PROOFSTEP]
rw [h] at hI ⊢
[GOAL]
case mp.inr.h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
hI : IsPrime (prod (map (RingHom.fst R S) I) ⊤)
h : map (RingHom.snd R S) I = ⊤
⊢ ∃ p, IsPrime p ∧ prod (map (RingHom.fst R S) I) ⊤ = prod p ⊤
[PROOFSTEP]
exact ⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' : Ideal S
I : Ideal (R × S)
⊢ ((∃ p, IsPrime p ∧ I = prod p ⊤) ∨ ∃ p, IsPrime p ∧ I = prod ⊤ p) → IsPrime I
[PROOFSTEP]
rintro (⟨p, ⟨h, rfl⟩⟩ | ⟨p, ⟨h, rfl⟩⟩)
[GOAL]
case mpr.inl.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' : Ideal S
p : Ideal R
h : IsPrime p
⊢ IsPrime (prod p ⊤)
[PROOFSTEP]
exact isPrime_ideal_prod_top
[GOAL]
case mpr.inr.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I I' : Ideal R
J J' p : Ideal S
h : IsPrime p
⊢ IsPrime (prod ⊤ p)
[PROOFSTEP]
exact isPrime_ideal_prod_top'


[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s => ↑(monomial s) 1) '' s) ↔ ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ si ≤ xi
[PROOFSTEP]
refine' AddMonoidAlgebra.mem_ideal_span_of'_image.trans _
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ (m : σ →₀ ℕ), m ∈ x.support → ∃ m', m' ∈ s ∧ ∃ d, m = d + m') ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ si ≤ xi
[PROOFSTEP]
simp_rw [le_iff_exists_add, add_comm]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ (m : σ →₀ ℕ), m ∈ x.support → ∃ m', m' ∈ s ∧ ∃ d, m = m' + d) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ ∃ c, xi = si + c
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s => ↑(monomial s) 1) '' s) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ ↑(monomial si) 1 ∣ ↑(monomial xi) (coeff xi x)
[PROOFSTEP]
refine' mem_ideal_span_monomial_image.trans (forall₂_congr fun xi hxi => _)
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ support x
⊢ (∃ si, si ∈ s ∧ si ≤ xi) ↔ ∃ si, si ∈ s ∧ ↑(monomial si) 1 ∣ ↑(monomial xi) (coeff xi x)
[PROOFSTEP]
simp_rw [monomial_dvd_monomial, one_dvd, and_true_iff, mem_support_iff.mp hxi, false_or_iff]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
[PROOFSTEP]
have := @mem_ideal_span_monomial_image σ R _ x ((fun i => Finsupp.single i 1) '' s)
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun s => ↑(monomial s) 1) '' ((fun i => Finsupp.single i 1) '' s)) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
[PROOFSTEP]
rw [Set.image_image] at this
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => ↑(monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ x ∈ Ideal.span (X '' s) ↔ ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
[PROOFSTEP]
refine' this.trans _
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set σ
this :
  x ∈ Ideal.span ((fun x => ↑(monomial (Finsupp.single x 1)) 1) '' s) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi
⊢ (∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ (fun i => Finsupp.single i 1) '' s ∧ si ≤ xi) ↔
    ∀ (m : σ →₀ ℕ), m ∈ support x → ∃ i, i ∈ s ∧ ↑m i ≠ 0
[PROOFSTEP]
simp [Nat.one_le_iff_ne_zero]