[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ coeff (select P x) n = ↑(aeval x.coeff) (selectPoly P n)
[PROOFSTEP]
dsimp [select, selectPoly]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ coeff (mk p fun n => if P n then coeff x n else 0) n = ↑(aeval x.coeff) (if P n then X n else 0)
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ coeff (mk p fun n => if P n then coeff x n else 0) n = ↑(aeval x.coeff) (X n)
[PROOFSTEP]
rw [aeval_X, mk]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ coeff { coeff := fun n => if P n then coeff x n else 0 } n = coeff x n
[PROOFSTEP]
simp only [hi]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ (if True then coeff x n else 0) = coeff x n
[PROOFSTEP]
rfl
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ coeff (mk p fun n => if P n then coeff x n else 0) n = ↑(aeval x.coeff) 0
[PROOFSTEP]
rw [AlgHom.map_zero, mk]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ coeff { coeff := fun n => if P n then coeff x n else 0 } n = 0
[PROOFSTEP]
simp only [hi]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ (if False then coeff x n else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ P : ℕ → Prop
⊢ IsPoly p fun x x_1 x_2 => select P x_2
[PROOFSTEP]
use selectPoly P
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ P : ℕ → Prop
⊢ ∀ ⦃R : Type ?u.31994⦄ [inst : CommRing R] (x : 𝕎 R), (select P x).coeff = fun n => ↑(aeval x.coeff) (selectPoly P n)
[PROOFSTEP]
rintro R _Rcr x
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R✝ : Type u_1
inst✝ : CommRing R✝
P✝ P : ℕ → Prop
R : Type ?u.31994
_Rcr : CommRing R
x : 𝕎 R
⊢ (select P x).coeff = fun n => ↑(aeval x.coeff) (selectPoly P n)
[PROOFSTEP]
funext i
[GOAL]
case h.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R✝ : Type u_1
inst✝ : CommRing R✝
P✝ P : ℕ → Prop
R : Type ?u.31994
_Rcr : CommRing R
x : 𝕎 R
i : ℕ
⊢ coeff (select P x) i = ↑(aeval x.coeff) (selectPoly P i)
[PROOFSTEP]
apply coeff_select
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
⊢ ∀ (x : 𝕎 R), select P x + select (fun i => ¬P i) x = x
[PROOFSTEP]
have : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x := IsPoly₂.diag (hf := IsPoly₂.comp)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
⊢ ∀ (x : 𝕎 R), select P x + select (fun i => ¬P i) x = x
[PROOFSTEP]
ghost_calc x
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
⊢ ∀ (n : ℕ), ↑(ghostComponent n) (select P x + select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
intro n
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ↑(ghostComponent n) (select P x + select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
simp only [RingHom.map_add]
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ↑(ghostComponent n) (select P x) + ↑(ghostComponent n) (select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
suffices
  (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
  by
  apply_fun aeval x.coeff at this 
  simpa only [AlgHom.map_add, aeval_bind₁, ← coeff_select]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this✝ : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
this :
  ↑(bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + ↑(bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
⊢ ↑(ghostComponent n) (select P x) + ↑(ghostComponent n) (select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
apply_fun aeval x.coeff at this 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this✝ : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
this :
  ↑(aeval x.coeff)
      (↑(bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + ↑(bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n)) =
    ↑(aeval x.coeff) (wittPolynomial p ℤ n)
⊢ ↑(ghostComponent n) (select P x) + ↑(ghostComponent n) (select (fun i => ¬P i) x) = ↑(ghostComponent n) x
[PROOFSTEP]
simpa only [AlgHom.map_add, aeval_bind₁, ← coeff_select]
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ↑(bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + ↑(bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
[PROOFSTEP]
simp only [wittPolynomial_eq_sum_C_mul_X_pow, selectPoly, AlgHom.map_sum, AlgHom.map_pow, AlgHom.map_mul, bind₁_X_right,
  bind₁_C_right, ← Finset.sum_add_distrib, ← mul_add]
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ (Finset.sum (Finset.range (n + 1)) fun x =>
      ↑C (↑p ^ x) * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x))) =
    Finset.sum (Finset.range (n + 1)) fun x => ↑C (↑p ^ x) * X x ^ p ^ (n - x)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      ↑C (↑p ^ x) * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x)) =
        ↑C (↑p ^ x) * X x ^ p ^ (n - x)
[PROOFSTEP]
refine' fun m _ => mul_eq_mul_left_iff.mpr (Or.inl _)
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
⊢ (if P m then X m else 0) ^ p ^ (n - m) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
[PROOFSTEP]
rw [ite_pow, zero_pow (pow_pos hp.out.pos _)]
[GOAL]
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
⊢ (if P m then X m ^ p ^ (n - m) else 0) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
[PROOFSTEP]
by_cases Pm : P m
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ (if P m then X m ^ p ^ (n - m) else 0) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
[PROOFSTEP]
rw [if_pos Pm, if_neg _, zero_pow, add_zero]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ 0 < p ^ (n - m)
[PROOFSTEP]
exact Fin.size_positive'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : P m
⊢ ¬¬P m
[PROOFSTEP]
exact not_not_intro Pm
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
P : ℕ → Prop
this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
x✝ : m ∈ Finset.range (n + 1)
Pm : ¬P m
⊢ (if P m then X m ^ p ^ (n - m) else 0) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
[PROOFSTEP]
rwa [if_neg Pm, if_pos, zero_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
let P : ℕ → Prop := fun n => y.coeff n = 0
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
haveI : DecidablePred P := Classical.decPred P
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
set z := mk p fun n => if P n then x.coeff n else y.coeff n
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
have hx : select P z = x := by
  ext1 n; rw [select, coeff_mk, coeff_mk]
  split_ifs with hn
  · rfl
  · rw [(h n).resolve_right hn]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
⊢ select P z = x
[PROOFSTEP]
ext1 n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
n : ℕ
⊢ coeff (select P z) n = coeff x n
[PROOFSTEP]
rw [select, coeff_mk, coeff_mk]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
n : ℕ
⊢ (if P n then if P n then coeff x n else coeff y n else 0) = coeff x n
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
n : ℕ
hn : P n
⊢ coeff x n = coeff x n
[PROOFSTEP]
rfl
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
n : ℕ
hn : ¬P n
⊢ 0 = coeff x n
[PROOFSTEP]
rw [(h n).resolve_right hn]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
have hy : select (fun i => ¬P i) z = y := by
  ext1 n; rw [select, coeff_mk, coeff_mk]
  split_ifs with hn
  · exact hn.symm
  · rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
⊢ select (fun i => ¬P i) z = y
[PROOFSTEP]
ext1 n
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
n : ℕ
⊢ coeff (select (fun i => ¬P i) z) n = coeff y n
[PROOFSTEP]
rw [select, coeff_mk, coeff_mk]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
n : ℕ
⊢ (if ¬P n then if P n then coeff x n else coeff y n else 0) = coeff y n
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
n : ℕ
hn : P n
⊢ 0 = coeff y n
[PROOFSTEP]
exact hn.symm
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
n : ℕ
hn : ¬P n
⊢ coeff y n = coeff y n
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ coeff (x + y) n = coeff x n + coeff y n
[PROOFSTEP]
calc
  (x + y).coeff n = z.coeff n := by rw [← hx, ← hy, select_add_select_not P z]
  _ = x.coeff n + y.coeff n := by
    simp [mk]
    split_ifs with y0
    · rw [y0, add_zero]
    · rw [h n |>.resolve_right y0, zero_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ coeff (x + y) n = coeff z n
[PROOFSTEP]
rw [← hx, ← hy, select_add_select_not P z]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ coeff z n = coeff x n + coeff y n
[PROOFSTEP]
simp [mk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
⊢ (if coeff y n = 0 then coeff x n else coeff y n) = coeff x n + coeff y n
[PROOFSTEP]
split_ifs with y0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
y0 : coeff y n = 0
⊢ coeff x n = coeff x n + coeff y n
[PROOFSTEP]
rw [y0, add_zero]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ : ℕ → Prop
x y : 𝕎 R
h : ∀ (n : ℕ), coeff x n = 0 ∨ coeff y n = 0
P : ℕ → Prop := fun n => coeff y n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n => if P n then coeff x n else coeff y n
hx : select P z = x
hy : select (fun i => ¬P i) z = y
y0 : ¬coeff y n = 0
⊢ coeff y n = coeff x n + coeff y n
[PROOFSTEP]
rw [h n |>.resolve_right y0, zero_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ init n x + tail n x = x
[PROOFSTEP]
simp only [init, tail, ← not_lt, select_add_select_not]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ init n (init n x) = init n x
[PROOFSTEP]
rw [ext_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∀ (n_1 : ℕ), coeff (init n (init n x)) n_1 = coeff (init n x) n_1
[PROOFSTEP]
intro i
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
⊢ coeff (init n (init n x)) i = coeff (init n x) i
[PROOFSTEP]
simp only [WittVector.init, WittVector.select, WittVector.coeff_mk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
⊢ (if i < n then if i < n then coeff x i else 0 else 0) = if i < n then coeff x i else 0
[PROOFSTEP]
by_cases hi : i < n
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
hi : i < n
⊢ (if i < n then if i < n then coeff x i else 0 else 0) = if i < n then coeff x i else 0
[PROOFSTEP]
simp [hi]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
hi : ¬i < n
⊢ (if i < n then if i < n then coeff x i else 0 else 0) = if i < n then coeff x i else 0
[PROOFSTEP]
simp [hi]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ init n (x + y) = init n (init n x + init n y)
[PROOFSTEP]
init_ring using wittAdd_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ init n (x * y) = init n (init n x * init n y)
[PROOFSTEP]
init_ring using wittMul_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ init n (-x) = init n (-init n x)
[PROOFSTEP]
init_ring using wittNeg_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ init n (x - y) = init n (init n x - init n y)
[PROOFSTEP]
init_ring using wittSub_vars
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ init n (m • x) = init n (m • init n x)
[PROOFSTEP]
init_ring using fun p [Fact (Nat.Prime p)] n => wittNSMul_vars p m n
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℤ
x : 𝕎 R
n : ℕ
⊢ init n (m • x) = init n (m • init n x)
[PROOFSTEP]
init_ring using fun p [Fact (Nat.Prime p)] n => wittZSMul_vars p m n
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
m : ℕ
x : 𝕎 R
n : ℕ
⊢ init n (x ^ m) = init n (init n x ^ m)
[PROOFSTEP]
init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n
