awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
have zero : (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[0] x =
  x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Identities (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
zero :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[0] x =
    x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
have succ : ∀ (n : ℕ)
  (ih :
    (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
      x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n),
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n + 1] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ (select P x).coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (selectPoly P n)
have dsimp : (if P n then x.coeff n else 0) =
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (if P n then X n else 0)
Tactic: dsimp [select, selectPoly]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ (if P n then x.coeff n else 0) =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (if P n then X n else 0)
have pos : ∀ (hi : P n), x.coeff n = ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (X n)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
pos : ∀ (hi : P n), x.coeff n = ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (X n)
⊢ (if P n then x.coeff n else 0) =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (if P n then X n else 0)
have neg : ∀ (hi : ¬P n),
  Eq (α := R) (0 : R) (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) 0 : R)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
P_1 P : ℕ → Prop
⊢ IsPoly.{u_2} p fun (x : Type u_2) (x_1 : CommRing x) (x_2 : 𝕎 x) ↦ select P x_2
have h : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
  (select P x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (selectPoly P n)
Tactic: use selectPoly P
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p n : ℕ
R_1 : Type u_1
inst : CommRing R_1
P_1 P : ℕ → Prop
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
⊢ (select P x).coeff = fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (selectPoly P n)
have h : ∀ (i : ℕ),
  (select P x).coeff i =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (selectPoly P i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (hypothesis)
Goal:
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
have this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
Tactic: have : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x :=
    IsPoly₂.diag (hf := IsPoly₂.comp)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
⊢ ∀ (x : 𝕎 R), select P x + select (fun (i : ℕ) ↦ ¬P i) x = x
have refine_3 : ∀ (R : Type u_1) [R._inst : CommRing R] (x : 𝕎 R) (n : ℕ),
  Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (select P x + select (fun (i : ℕ) ↦ ¬P i) x) : R)
    ((ghostComponent n : (a : 𝕎 R) → R) x : R)
Tactic: ghost_calc x
Cleared hypotheses: R, inst
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ Eq (α := R) ((ghostComponent n : (a : 𝕎 R) → R) (select P x + select (fun (i : ℕ) ↦ ¬P i) x) : R)
    ((ghostComponent n : (a : 𝕎 R) → R) x : R)
have refine_3 : HAdd.hAdd (α := R) (β := R) ((ghostComponent n : (a : 𝕎 R) → R) (select P x) : R)
    ((ghostComponent n : (a : 𝕎 R) → R) (select (fun (i : ℕ) ↦ ¬P i) x) : R) =
  (ghostComponent n : (a : 𝕎 R) → R) x
Tactic: simp only [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (hypothesis)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this_1 : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
this :
  HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
      ((bind₁ (selectPoly P) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
      ((bind₁ (selectPoly fun (i : ℕ) ↦ ¬P i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
        MvPolynomial ℕ ℤ) =
    wittPolynomial p ℤ n
⊢ HAdd.hAdd (α := R) (β := R) ((ghostComponent n : (a : 𝕎 R) → R) (select P x) : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (select (fun (i : ℕ) ↦ ¬P i) x) : R) =
    (ghostComponent n : (a : 𝕎 R) → R) x
have this₁ : Eq (α := R)
  (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
        ((bind₁ (selectPoly P) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
        ((bind₁ (selectPoly fun (i : ℕ) ↦ ¬P i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
          MvPolynomial ℕ ℤ)) :
    R)
  (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittPolynomial p ℤ n) : R)
Tactic: apply_fun aeval x.coeff at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ HAdd.hAdd (α := R) (β := R) ((ghostComponent n : (a : 𝕎 R) → R) (select P x) : R)
      ((ghostComponent n : (a : 𝕎 R) → R) (select (fun (i : ℕ) ↦ ¬P i) x) : R) =
    (ghostComponent n : (a : 𝕎 R) → R) x
have refine_3 : HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
    ((bind₁ (selectPoly P) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
    ((bind₁ (selectPoly fun (i : ℕ) ↦ ¬P i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
      MvPolynomial ℕ ℤ) =
  wittPolynomial p ℤ n
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]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
      ((bind₁ (selectPoly P) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) : MvPolynomial ℕ ℤ)
      ((bind₁ (selectPoly fun (i : ℕ) ↦ ¬P i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ n) :
        MvPolynomial ℕ ℤ) =
    wittPolynomial p ℤ n
have refine_3 : Eq (α := MvPolynomial ℕ ℤ)
  (∑ x ∈ Finset.range (n + 1),
    HPow.hPow (α := MvPolynomial ℕ ℤ) ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (↑p : ℤ)) x *
      (HPow.hPow (α := MvPolynomial ℕ ℤ) (if P x then X x else 0) (p ^ (n - x)) +
        HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P x then X x else 0) (p ^ (n - x))))
  (∑ x ∈ Finset.range (n + 1),
    HPow.hPow (α := MvPolynomial ℕ ℤ) ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (↑p : ℤ)) x *
      HPow.hPow (α := MvPolynomial ℕ ℤ) (X x) (p ^ (n - x)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ Eq (α := MvPolynomial ℕ ℤ)
    (∑ x ∈ Finset.range (n + 1),
      HPow.hPow (α := MvPolynomial ℕ ℤ) ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (↑p : ℤ)) x *
        (HPow.hPow (α := MvPolynomial ℕ ℤ) (if P x then X x else 0) (p ^ (n - x)) +
          HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P x then X x else 0) (p ^ (n - x))))
    (∑ x ∈ Finset.range (n + 1),
      HPow.hPow (α := MvPolynomial ℕ ℤ) ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (↑p : ℤ)) x *
        HPow.hPow (α := MvPolynomial ℕ ℤ) (X x) (p ^ (n - x)))
have refine_3 : ∀ x ∈ Finset.range (n + 1),
  HPow.hPow (α := MvPolynomial ℕ ℤ) ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (↑p : ℤ)) x *
      (HPow.hPow (α := MvPolynomial ℕ ℤ) (if P x then X x else 0) (p ^ (n - x)) +
        HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P x then X x else 0) (p ^ (n - x))) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (↑p : ℤ)) x *
      HPow.hPow (α := MvPolynomial ℕ ℤ) (X x) (p ^ (n - x))
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ 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),
    HPow.hPow (α := MvPolynomial ℕ ℤ) ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (↑p : ℤ)) x *
        (HPow.hPow (α := MvPolynomial ℕ ℤ) (if P x then X x else 0) (p ^ (n - x)) +
          HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P x then X x else 0) (p ^ (n - x))) =
      HPow.hPow (α := MvPolynomial ℕ ℤ) ((C : (a : ℤ) → MvPolynomial ℕ ℤ) (↑p : ℤ)) x *
        HPow.hPow (α := MvPolynomial ℕ ℤ) (X x) (p ^ (n - x))
have refine_3 : ∀ m ∈ Finset.range (n + 1),
  HPow.hPow (α := MvPolynomial ℕ ℤ) (if P m then X m else 0) (p ^ (n - m)) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: refine fun m _ => mul_eq_mul_left_iff.mpr (Or.inl ?_)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
⊢ HPow.hPow (α := MvPolynomial ℕ ℤ) (if P m then X m else 0) (p ^ (n - m)) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have refine_3 : (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
    HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: rw [ite_pow, zero_pow (pow_ne_zero _ hp.out.ne_zero)]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have pos : ∀ (Pm : P m),
  (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: by_cases Pm : P m
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
pos :
  ∀ (Pm : P m),
    (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
        HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
      HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have neg : ∀ (Pm : ¬P m),
  (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: by_cases Pm : P m
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
Pm : P m
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have pos : HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) +
    HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: rw [if_pos Pm, if_neg <| not_not_intro Pm, zero_pow Fin.pos'.ne', add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
Pm : P m
pos :
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have pos₁ : HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) + HPow.hPow (α := MvPolynomial ℕ ℤ) 0 (p ^ (n - m)) =
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: rw [if_pos Pm, if_neg <| not_not_intro Pm, zero_pow Fin.pos'.ne', add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
Pm : P m
pos :
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
pos₁ :
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) + HPow.hPow (α := MvPolynomial ℕ ℤ) 0 (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have pos₂ : HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) + 0 = HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: rw [if_pos Pm, if_neg <| not_not_intro Pm, zero_pow Fin.pos'.ne', add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
Pm : P m
pos :
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
pos₁ :
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) + HPow.hPow (α := MvPolynomial ℕ ℤ) 0 (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
pos₂ : HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) + 0 = HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have pos₃ : HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) = HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: rw [if_pos Pm, if_neg <| not_not_intro Pm, zero_pow Fin.pos'.ne', add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
Pm : ¬P m
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have neg : 0 + HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: rwa [if_neg Pm, if_pos, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
Pm : ¬P m
neg :
  0 + HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have neg₁ : 0 + HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) = HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: rwa [if_neg Pm, if_pos, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly.{u_1} p fun {R : Type u_1} [CommRing R] (x : 𝕎 R) ↦ select P x + select (fun (i : ℕ) ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n m : ℕ
h : m ∈ Finset.range (n + 1)
Pm : ¬P m
neg :
  0 + HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
neg₁ : 0 + HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) = HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
neg₂ : ¬P m
⊢ (if P m then HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) else 0) +
      HPow.hPow (α := MvPolynomial ℕ ℤ) (if ¬P m then X m else 0) (p ^ (n - m)) =
    HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
have neg₃ : HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) = HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
Tactic: rwa [if_neg Pm, if_pos, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun (n : ℕ) ↦ y.coeff n = 0
⊢ (x + y).coeff n = x.coeff n + y.coeff n
have haveI : ∀ (this : DecidablePred P), (x + y).coeff n = x.coeff n + y.coeff n
Tactic: haveI : DecidablePred P := Classical.decPred P
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun (n : ℕ) ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun (n : ℕ) ↦ if P n then x.coeff n else y.coeff n
⊢ select P z = x
have h₁ : ∀ (n : ℕ), (select P z).coeff n = x.coeff n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p n_1 : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun (n : ℕ) ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun (n : ℕ) ↦ if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (select P z).coeff n = x.coeff n
have h₁ : (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n
Tactic: rw [select, coeff_mk, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p n_1 : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun (n : ℕ) ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun (n : ℕ) ↦ if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n
have pos : ∀ (hn : P n), x.coeff n = x.coeff n
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p n_1 : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun (n : ℕ) ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun (n : ℕ) ↦ if P n then x.coeff n else y.coeff n
n : ℕ
pos : ∀ (hn : P n), x.coeff n = x.coeff n
⊢ (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n
have neg : ∀ (hn : ¬P n), 0 = x.coeff n
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p n_1 : ℕ
R : Type u_1
inst : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun (n : ℕ) ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun (n : ℕ) ↦ if P n then x.coeff n else y.coeff n
n : ℕ
hn : ¬P n
⊢ 0 = x.coeff n
have neg : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [(h n).resolve_right hn]