awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (hypothesis)
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
⊢ (x + y).coeff n = x.coeff n + y.coeff n
have hx : select P z = x
Tactic: 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]
-- 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
hx : select P z = x
⊢ select (fun (i : ℕ) ↦ ¬P i) z = y
have h₁ : ∀ (n : ℕ), (select (fun (i : ℕ) ↦ ¬P i) z).coeff n = y.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
hx : select P z = x
n : ℕ
⊢ (select (fun (i : ℕ) ↦ ¬P i) z).coeff n = y.coeff n
have h₁ : (if ¬P n then if P n then x.coeff n else y.coeff n else 0) = y.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
hx : select P z = x
n : ℕ
⊢ (if ¬P n then if P n then x.coeff n else y.coeff n else 0) = y.coeff n
have pos : ∀ (hn : P n), 0 = y.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
hx : select P z = x
n : ℕ
pos : ∀ (hn : P n), 0 = y.coeff n
⊢ (if ¬P n then if P n then x.coeff n else y.coeff n else 0) = y.coeff n
have neg : ∀ (hn : ¬P n), y.coeff n = y.coeff n
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (hypothesis)
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
hx : select P z = x
⊢ (x + y).coeff n = x.coeff n + y.coeff n
have hy : select (fun (i : ℕ) ↦ ¬P i) z = y
Tactic: 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
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
⊢ (x + y).coeff n = z.coeff n
have rw : (select P z + y).coeff n = z.coeff n
Tactic: rw [← hx, ← hy, select_add_select_not P z]
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
rw : (select P z + y).coeff n = z.coeff n
⊢ (x + y).coeff n = z.coeff n
have rw₁ : (select P z + select (fun (i : ℕ) ↦ ¬P i) z).coeff n = z.coeff n
Tactic: rw [← hx, ← hy, select_add_select_not P z]
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
rw : (select P z + y).coeff n = z.coeff n
rw₁ : (select P z + select (fun (i : ℕ) ↦ ¬P i) z).coeff n = z.coeff n
⊢ (x + y).coeff n = z.coeff n
have rw₂ : z.coeff n = z.coeff n
Tactic: rw [← hx, ← hy, select_add_select_not P z]
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
⊢ z.coeff n = x.coeff n + y.coeff n
have simp : (if P n then x.coeff n else y.coeff n) = x.coeff n + y.coeff n
Tactic: simp only [z, mk.eq_1]
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
⊢ (if P n then x.coeff n else y.coeff n) = x.coeff n + y.coeff n
have pos : ∀ (y0 : P n), x.coeff n = x.coeff n + y.coeff n
Tactic: split_ifs with y0
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
pos : ∀ (y0 : P n), x.coeff n = x.coeff n + y.coeff n
⊢ (if P n then x.coeff n else y.coeff n) = x.coeff n + y.coeff n
have neg : ∀ (y0 : ¬P n), y.coeff n = x.coeff n + y.coeff n
Tactic: split_ifs with y0
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
y0 : P n
⊢ x.coeff n = x.coeff n + y.coeff n
have pos : x.coeff n = x.coeff n + 0
Tactic: rw [y0, add_zero]
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
y0 : P n
pos : x.coeff n = x.coeff n + 0
⊢ x.coeff n = x.coeff n + y.coeff n
have pos₁ : x.coeff n = x.coeff n
Tactic: rw [y0, add_zero]
-- 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
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
y0 : ¬P n
⊢ y.coeff n = x.coeff n + y.coeff n
have neg : y.coeff n = 0 + y.coeff n
Tactic: rw [h n |>.resolve_right y0, 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
this : DecidablePred P
z : 𝕎 R := mk p fun (n : ℕ) ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
y0 : ¬P n
neg : y.coeff n = 0 + y.coeff n
⊢ y.coeff n = x.coeff n + y.coeff n
have neg₁ : y.coeff n = y.coeff n
Tactic: rw [h n |>.resolve_right y0, 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
this : DecidablePred P
z : 𝕎 R := mk p fun (n : ℕ) ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
⊢ (x + y).coeff n = x.coeff n + y.coeff n
have n₁ : (x + y).coeff n = z.coeff n
Tactic: 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 only [z, mk.eq_1]
      split_ifs with y0
      · rw [y0, add_zero]
      · rw [h n |>.resolve_right y0, 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
this : DecidablePred P
z : 𝕎 R := mk p fun (n : ℕ) ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun (i : ℕ) ↦ ¬P i) z = y
n₁ : (x + y).coeff n = z.coeff n
⊢ (x + y).coeff n = x.coeff n + y.coeff n
have n₂ : z.coeff n = x.coeff n + y.coeff n
Tactic: 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 only [z, mk.eq_1]
      split_ifs with y0
      · rw [y0, add_zero]
      · rw [h n |>.resolve_right y0, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ init n (init n x) = init n x
have init_ring : ∀ (n_1 : ℕ), (init n (init n x)).coeff n_1 = (init n x).coeff n_1
Tactic: init_ring
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (init n x)).coeff i = (init n x).coeff i
⊢ init n (init n x) = init n x
have init_ring₆ : ∀ (i : ℕ), (if i < n then if i < n then x.coeff i else 0 else 0) = if i < n then x.coeff i else 0
Tactic: init_ring
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
⊢ init n (x + y) = init n (init n x + init n y)
have init_ring : ∀ (n_1 : ℕ), (init n (x + y)).coeff n_1 = (init n (init n x + init n y)).coeff n_1
Tactic: init_ring using wittAdd_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (x + y)).coeff i = (init n (init n x + init n y)).coeff i
⊢ init n (x + y) = init n (init n x + init n y)
have init_ring₆ : ∀ (i : ℕ),
  (if i < n then (x + y).coeff i else 0) =
    if i < n then
      (HAdd.hAdd (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
            (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
        i
    else 0
Tactic: init_ring using wittAdd_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (x + y)).coeff i = (init n (init n x + init n y)).coeff i
init_ring₆ init_ring₇ :
  ∀ (i : ℕ),
    (if i < n then (x + y).coeff i else 0) =
      if i < n then
        (HAdd.hAdd (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
              (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
          i
      else 0
⊢ init n (x + y) = init n (init n x + init n y)
have pos : ∀ (i : ℕ) (hi : i < n),
  (x + y).coeff i =
    (HAdd.hAdd (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
          (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
      i
Tactic: init_ring using wittAdd_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
⊢ init n (x * y) = init n (init n x * init n y)
have init_ring : ∀ (n_1 : ℕ), (init n (x * y)).coeff n_1 = (init n (init n x * init n y)).coeff n_1
Tactic: init_ring using wittMul_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (x * y)).coeff i = (init n (init n x * init n y)).coeff i
⊢ init n (x * y) = init n (init n x * init n y)
have init_ring₆ : ∀ (i : ℕ),
  (if i < n then (x * y).coeff i else 0) =
    if i < n then
      (HMul.hMul (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
            (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
        i
    else 0
Tactic: init_ring using wittMul_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (x * y)).coeff i = (init n (init n x * init n y)).coeff i
init_ring₆ init_ring₇ :
  ∀ (i : ℕ),
    (if i < n then (x * y).coeff i else 0) =
      if i < n then
        (HMul.hMul (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
              (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
          i
      else 0
⊢ init n (x * y) = init n (init n x * init n y)
have pos : ∀ (i : ℕ) (hi : i < n),
  (x * y).coeff i =
    (HMul.hMul (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
          (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
      i
Tactic: init_ring using wittMul_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ init n (-x) = init n (-init n x)
have init_ring : ∀ (n_1 : ℕ), (init n (-x)).coeff n_1 = (init n (-init n x)).coeff n_1
Tactic: init_ring using wittNeg_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (-x)).coeff i = (init n (-init n x)).coeff i
⊢ init n (-x) = init n (-init n x)
have init_ring₆ : ∀ (i : ℕ),
  (if i < n then (-x).coeff i else 0) =
    if i < n then coeff (-mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0) i else 0
Tactic: init_ring using wittNeg_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (-x)).coeff i = (init n (-init n x)).coeff i
init_ring₆ init_ring₇ :
  ∀ (i : ℕ),
    (if i < n then (-x).coeff i else 0) =
      if i < n then coeff (-mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0) i else 0
⊢ init n (-x) = init n (-init n x)
have pos : ∀ (i : ℕ) (hi : i < n), (-x).coeff i = coeff (-mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0) i
Tactic: init_ring using wittNeg_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
⊢ init n (x - y) = init n (init n x - init n y)
have init_ring : ∀ (n_1 : ℕ), (init n (x - y)).coeff n_1 = (init n (init n x - init n y)).coeff n_1
Tactic: init_ring using wittSub_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (x - y)).coeff i = (init n (init n x - init n y)).coeff i
⊢ init n (x - y) = init n (init n x - init n y)
have init_ring₆ : ∀ (i : ℕ),
  (if i < n then (x - y).coeff i else 0) =
    if i < n then
      (HSub.hSub (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
            (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
        i
    else 0
Tactic: init_ring using wittSub_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (x - y)).coeff i = (init n (init n x - init n y)).coeff i
init_ring₆ init_ring₇ :
  ∀ (i : ℕ),
    (if i < n then (x - y).coeff i else 0) =
      if i < n then
        (HSub.hSub (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
              (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
          i
      else 0
⊢ init n (x - y) = init n (init n x - init n y)
have pos : ∀ (i : ℕ) (hi : i < n),
  (x - y).coeff i =
    (HSub.hSub (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)
          (mk p fun (n_1 : ℕ) ↦ if n_1 < n then y.coeff n_1 else 0)).coeff
      i
Tactic: init_ring using wittSub_vars
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
n : ℕ
⊢ init n (m • x) = init n (m • init n x)
have init_ring : ∀ (n_1 : ℕ), (init n (m • x)).coeff n_1 = (init n (m • init n x)).coeff n_1
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittNSMul_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (m • x)).coeff i = (init n (m • init n x)).coeff i
⊢ init n (m • x) = init n (m • init n x)
have init_ring₆ : ∀ (i : ℕ),
  (if i < n then (m • x).coeff i else 0) =
    if i < n then (HSMul.hSMul (β := 𝕎 R) m (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)).coeff i else 0
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittNSMul_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (m • x)).coeff i = (init n (m • init n x)).coeff i
init_ring₆ init_ring₇ :
  ∀ (i : ℕ),
    (if i < n then (m • x).coeff i else 0) =
      if i < n then (HSMul.hSMul (β := 𝕎 R) m (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)).coeff i else 0
⊢ init n (m • x) = init n (m • init n x)
have pos : ∀ (i : ℕ) (hi : i < n),
  (m • x).coeff i = (HSMul.hSMul (β := 𝕎 R) m (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)).coeff i
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittNSMul_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
n : ℕ
⊢ init n (m • x) = init n (m • init n x)
have init_ring : ∀ (n_1 : ℕ), (init n (m • x)).coeff n_1 = (init n (m • init n x)).coeff n_1
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittZSMul_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (m • x)).coeff i = (init n (m • init n x)).coeff i
⊢ init n (m • x) = init n (m • init n x)
have init_ring₆ : ∀ (i : ℕ),
  (if i < n then (m • x).coeff i else 0) =
    if i < n then (HSMul.hSMul (β := 𝕎 R) m (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)).coeff i else 0
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittZSMul_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (m • x)).coeff i = (init n (m • init n x)).coeff i
init_ring₆ init_ring₇ :
  ∀ (i : ℕ),
    (if i < n then (m • x).coeff i else 0) =
      if i < n then (HSMul.hSMul (β := 𝕎 R) m (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)).coeff i else 0
⊢ init n (m • x) = init n (m • init n x)
have pos : ∀ (i : ℕ) (hi : i < n),
  (m • x).coeff i = (HSMul.hSMul (β := 𝕎 R) m (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0)).coeff i
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittZSMul_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
n : ℕ
⊢ init n (x ^ m) = init n (init n x ^ m)
have init_ring : ∀ (n_1 : ℕ), (init n (x ^ m)).coeff n_1 = (init n (init n x ^ m)).coeff n_1
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (x ^ m)).coeff i = (init n (init n x ^ m)).coeff i
⊢ init n (x ^ m) = init n (init n x ^ m)
have init_ring₆ : ∀ (i : ℕ),
  (if i < n then (x ^ m).coeff i else 0) =
    if i < n then (HPow.hPow (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0) m).coeff i else 0
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.InitTail (goal)
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
n : ℕ
init_ring init_ring₁ init_ring₂ init_ring₃ init_ring₄ init_ring₅ :
  ∀ (i : ℕ), (init n (x ^ m)).coeff i = (init n (init n x ^ m)).coeff i
init_ring₆ init_ring₇ :
  ∀ (i : ℕ),
    (if i < n then (x ^ m).coeff i else 0) =
      if i < n then (HPow.hPow (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0) m).coeff i else 0
⊢ init n (x ^ m) = init n (init n x ^ m)
have pos : ∀ (i : ℕ) (hi : i < n),
  (x ^ m).coeff i = (HPow.hPow (α := 𝕎 R) (mk p fun (n_1 : ℕ) ↦ if n_1 < n then x.coeff n_1 else 0) m).coeff i
Tactic: init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
idx : Type u_1
inst : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial (idx × ℕ) ℤ
h :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ f : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n) : MvPolynomial (idx × ℕ) ℤ)
      ((bind₁ g : (a : MvPolynomial ℕ ℤ) → MvPolynomial (idx × ℕ) ℤ) (wittPolynomial p ℤ n) : MvPolynomial (idx × ℕ) ℤ)
⊢ f = g
have h₁ : ∀ (n : ℕ), f n = g n
Tactic: ext1 n