-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem select_add_select_not : ∀ x : 𝕎 R, select P x + select (fun i => ¬P i) x = x

Proof state:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Tactic:
intro n

Result:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Proof state:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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 ∈ 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)

Tactic:
refine fun m _ => mul_eq_mul_left_iff.mpr (Or.inl ?_)

Result:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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)

Proof state:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Tactic:
simp only [wittPolynomial_eq_sum_C_mul_X_pow, selectPoly, map_sum, map_pow, map_mul,
  bind₁_X_right, bind₁_C_right, ← Finset.sum_add_distrib, ← mul_add]

Result:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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 ∈ 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)) =
    ∑ x ∈ Finset.range (n + 1), C ↑p ^ x * X x ^ p ^ (n - x)

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Tactic:
ghost_calc x

Result:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Proof state:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Tactic:
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 [map_add, aeval_bind₁, ← coeff_select]

Result:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Proof state:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Tactic:
simpa only [map_add, aeval_bind₁, ← coeff_select]

Result:
no goals

Proof state:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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 ∈ 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)) =
    ∑ x ∈ Finset.range (n + 1), C ↑p ^ x * X x ^ p ^ (n - x)

Tactic:
apply Finset.sum_congr rfl

Result:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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 ∈ 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)

Proof state:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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)

Tactic:
rw [ite_pow, zero_pow (pow_ne_zero _ hp.out.ne_zero)]

Result:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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)

Proof state:
case pos
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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)

Tactic:
rw [if_pos Pm, if_neg <| not_not_intro Pm, zero_pow Fin.pos'.ne', add_zero]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
hp : Fact (Nat.Prime p)
⊢ ∀ (x : 𝕎 R), select P x + select (fun i => ¬P i) x = x

Tactic:
have : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x :=
  IsPoly₂.diag (hf := IsPoly₂.comp)

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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

Proof state:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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)

Tactic:
by_cases Pm : P m

Result:
case pos
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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)

case neg
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
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)