[GOAL]
p : ℕ
R : Type u_1
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = coeff y n
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case mk'
p : ℕ
R : Type u_1
y : 𝕎 R
coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff { coeff := coeff✝ } n = coeff y n
⊢ { coeff := coeff✝ } = y
[PROOFSTEP]
cases y
[GOAL]
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff { coeff := coeff✝¹ } n = coeff { coeff := coeff✝ } n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
[PROOFSTEP]
simp only at h 
[GOAL]
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff✝¹ n = coeff✝ n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
[PROOFSTEP]
simp [Function.funext_iff, h]
[GOAL]
p : ℕ
R : Type u_1
x y : 𝕎 R
h : x = y
n : ℕ
⊢ coeff x n = coeff y n
[PROOFSTEP]
rw [h]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ wittZero p n = 0
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑(map (Int.castRingHom ℚ)) (wittZero p n) = ↑(map (Int.castRingHom ℚ)) 0
[PROOFSTEP]
simp only [wittZero, wittStructureRat, bind₁, aeval_zero', constantCoeff_xInTermsOfW, RingHom.map_zero, AlgHom.map_zero,
  map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittOne p 0 = 1
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittOne p 0) = ↑(map (Int.castRingHom ℚ)) 1
[PROOFSTEP]
simp only [wittOne, wittStructureRat, xInTermsOfW_zero, AlgHom.map_one, RingHom.map_one, bind₁_X_right,
  map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ wittOne p n = 0
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(map (Int.castRingHom ℚ)) (wittOne p n) = ↑(map (Int.castRingHom ℚ)) 0
[PROOFSTEP]
simp only [wittOne, wittStructureRat, RingHom.map_zero, AlgHom.map_one, RingHom.map_one, map_wittStructureInt]
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
[PROOFSTEP]
induction n using Nat.strong_induction_on with
| h n IH => ?_
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
[PROOFSTEP]
induction n using Nat.strong_induction_on with
| h n IH => ?_
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
[PROOFSTEP]
rw [xInTermsOfW_eq]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑(bind₁ fun k => 1)
      ((X n - Finset.sum (Finset.range n) fun i => ↑C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * ↑C (⅟↑p ^ n)) =
    0
[PROOFSTEP]
simp only [AlgHom.map_mul, AlgHom.map_sub, AlgHom.map_sum, AlgHom.map_pow, bind₁_X_right, bind₁_C_right]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ (1 - Finset.sum (Finset.range n) fun x => ↑C (↑p ^ x) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
      ↑C (⅟↑p ^ n) =
    0
[PROOFSTEP]
rw [sub_mul, one_mul]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (⅟↑p ^ n) -
      (Finset.sum (Finset.range n) fun x => ↑C (↑p ^ x) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        ↑C (⅟↑p ^ n) =
    0
[PROOFSTEP]
rw [Finset.sum_eq_single 0]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (⅟↑p ^ n) - ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) * ↑C (⅟↑p ^ n) = 0
[PROOFSTEP]
simp only [invOf_eq_inv, one_mul, inv_pow, tsub_zero, RingHom.map_one, pow_zero]
[GOAL]
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ↑C (↑p ^ n)⁻¹ - ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ n * ↑C (↑p ^ n)⁻¹ = 0
[PROOFSTEP]
simp only [one_pow, one_mul, xInTermsOfW_zero, sub_self, bind₁_X_right]
[GOAL]
case a.h.h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ∀ (b : ℕ), b ∈ Finset.range n → b ≠ 0 → ↑C (↑p ^ b) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ b) ^ p ^ (n - b) = 0
[PROOFSTEP]
intro i hin hi0
[GOAL]
case a.h.h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i ∈ Finset.range n
hi0 : i ≠ 0
⊢ ↑C (↑p ^ i) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
[PROOFSTEP]
rw [Finset.mem_range] at hin 
[GOAL]
case a.h.h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
i : ℕ
hin : i < n
hi0 : i ≠ 0
⊢ ↑C (↑p ^ i) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ i) ^ p ^ (n - i) = 0
[PROOFSTEP]
rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_pos hp.1.pos _), mul_zero]
[GOAL]
case a.h.h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ¬0 ∈ Finset.range n → ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
[PROOFSTEP]
rw [Finset.mem_range]
[GOAL]
case a.h.h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ ¬0 < n → ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
[PROOFSTEP]
intro
[GOAL]
case a.h.h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
IH : ∀ (m : ℕ), m < n → 0 < m → ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
a✝ : ¬0 < n
⊢ ↑C (↑p ^ 0) * ↑(bind₁ fun k => 1) (xInTermsOfW p ℚ 0) ^ p ^ (n - 0) = 0
[PROOFSTEP]
contradiction
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittAdd p 0 = X (0, 0) + X (1, 0)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittAdd p 0) = ↑(map (Int.castRingHom ℚ)) (X (0, 0) + X (1, 0))
[PROOFSTEP]
simp only [wittAdd, wittStructureRat, AlgHom.map_add, RingHom.map_add, rename_X, xInTermsOfW_zero, map_X,
  wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittSub p 0 = X (0, 0) - X (1, 0)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittSub p 0) = ↑(map (Int.castRingHom ℚ)) (X (0, 0) - X (1, 0))
[PROOFSTEP]
simp only [wittSub, wittStructureRat, AlgHom.map_sub, RingHom.map_sub, rename_X, xInTermsOfW_zero, map_X,
  wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittMul p 0 = X (0, 0) * X (1, 0)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittMul p 0) = ↑(map (Int.castRingHom ℚ)) (X (0, 0) * X (1, 0))
[PROOFSTEP]
simp only [wittMul, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero, RingHom.map_mul,
  bind₁_X_right, AlgHom.map_mul, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ wittNeg p 0 = -X (0, 0)
[PROOFSTEP]
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case a
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(map (Int.castRingHom ℚ)) (wittNeg p 0) = ↑(map (Int.castRingHom ℚ)) (-X (0, 0))
[PROOFSTEP]
simp only [wittNeg, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero, RingHom.map_neg,
  AlgHom.map_neg, bind₁_X_right, map_wittStructureInt]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittAdd p n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (X 0 + X 1) = 0
[PROOFSTEP]
simp only [add_zero, RingHom.map_add, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittSub p n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (X 0 - X 1) = 0
[PROOFSTEP]
simp only [sub_zero, RingHom.map_sub, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittMul p n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (X 0 * X 1) = 0
[PROOFSTEP]
simp only [mul_zero, RingHom.map_mul, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (wittNeg p n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑constantCoeff (-X 0) = 0
[PROOFSTEP]
simp only [neg_zero, RingHom.map_neg, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m n : ℕ
⊢ ↑constantCoeff (wittNSMul p m n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m n : ℕ
⊢ ↑constantCoeff (m • X 0) = 0
[PROOFSTEP]
simp only [smul_zero, map_nsmul, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
z : ℤ
n : ℕ
⊢ ↑constantCoeff (wittZSMul p z n) = 0
[PROOFSTEP]
apply constantCoeff_wittStructureInt p _ _ n
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
z : ℤ
n : ℕ
⊢ ↑constantCoeff (z • X 0) = 0
[PROOFSTEP]
simp only [smul_zero, map_zsmul, constantCoeff_X]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ ↑(aeval (Function.uncurry fun i => ![].coeff)) (wittZero p n) = 0
[PROOFSTEP]
simp only [wittZero_eq_zero, AlgHom.map_zero]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ↑(aeval (Function.uncurry fun i => ![].coeff)) (wittOne p 0) = 1
[PROOFSTEP]
simp only [wittOne_zero_eq_one, AlgHom.map_one]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ ↑(aeval (Function.uncurry fun i => ![].coeff)) (wittOne p n) = 0
[PROOFSTEP]
simp only [hn, wittOne_pos_eq_zero, AlgHom.map_zero]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
i : Fin 2
⊢ (Matrix.vecCons x ![y] i).coeff = Matrix.vecCons x.coeff ![y.coeff] i
[PROOFSTEP]
fin_cases i
[GOAL]
case head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
⊢ (Matrix.vecCons x ![y] { val := 0, isLt := (_ : 0 < 2) }).coeff =
    Matrix.vecCons x.coeff ![y.coeff] { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp
[GOAL]
case tail.head
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
⊢ (Matrix.vecCons x ![y] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).coeff =
    Matrix.vecCons x.coeff ![y.coeff] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ coeff (x + y) n = peval (wittAdd p n) ![x.coeff, y.coeff]
[PROOFSTEP]
simp [(· + ·), Add.add, eval, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ coeff (x - y) n = peval (wittSub p n) ![x.coeff, y.coeff]
[PROOFSTEP]
simp [(· - ·), Sub.sub, eval, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ coeff (x * y) n = peval (wittMul p n) ![x.coeff, y.coeff]
[PROOFSTEP]
simp [(· * ·), Mul.mul, eval, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ coeff (-x) n = peval (wittNeg p n) ![x.coeff]
[PROOFSTEP]
simp [Neg.neg, eval, Matrix.cons_fin_one, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ coeff (m • x) n = peval (wittNSMul p m n) ![x.coeff]
[PROOFSTEP]
simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℤ
x : 𝕎 R
n : ℕ
⊢ coeff (m • x) n = peval (wittZSMul p m n) ![x.coeff]
[PROOFSTEP]
simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ coeff (x ^ m) n = peval (wittPow p m n) ![x.coeff]
[PROOFSTEP]
simp [(· ^ ·), Pow.pow, eval, Matrix.cons_fin_one, coeff_mk]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ coeff (x + y) 0 = coeff x 0 + coeff y 0
[PROOFSTEP]
simp [add_coeff, peval]
[GOAL]
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ coeff (x * y) 0 = coeff x 0 * coeff y 0
[PROOFSTEP]
simp [mul_coeff, peval]
