awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.InitTail
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 : ℕ
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))
⊢ ∀ 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:
refine fun m _ => mul_eq_mul_left_iff.mpr (Or.inl ?_)

Premises used: Iff.mpr, mul_eq_mul_left_iff, Or.inl
-- Module: Mathlib.RingTheory.WittVector.InitTail
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)
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))
⊢ 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:
rw [ite_pow, zero_pow (pow_ne_zero _ hp.out.ne_zero)]

Premises used: ite_pow, pow_ne_zero, Nat.Prime.ne_zero, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.WittVector.InitTail
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))
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))
⊢ (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
-- Module: Mathlib.RingTheory.WittVector.InitTail
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))
pos₃ pos₄ :
  HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (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))

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

Premises used: not_not_intro, if_pos, LT.lt.ne', Fin.pos', add_zero, if_neg, zero_pow
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
neg₃ : HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) = HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
neg₄ : ¬P m
neg₅ : HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m)) = HPow.hPow (α := MvPolynomial ℕ ℤ) (X m) (p ^ (n - m))
neg₆ neg₇ 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))

Tactic:
rwa [if_neg Pm, if_pos, zero_add]

Premises used: if_pos, zero_add, if_neg
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
haveI : ∀ (this : DecidablePred P), (x + y).coeff n = x.coeff n + y.coeff n
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Tactic:
haveI : DecidablePred P := Classical.decPred P
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
h₁ : ∀ (n : ℕ), (select P z).coeff n = x.coeff n
⊢ select P z = x

Tactic:
ext1 n
-- Module: Mathlib.RingTheory.WittVector.InitTail
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 : ℕ
h₁ : (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n
⊢ (select P z).coeff n = x.coeff n

Tactic:
rw [select, coeff_mk, coeff_mk]

Premises used: WittVector.select, WittVector.coeff_mk
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
neg : ∀ (hn : ¬P n), 0 = x.coeff n
⊢ (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n

Tactic:
split_ifs with hn
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
⊢ x.coeff n = x.coeff n

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
neg neg₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 = x.coeff n

Tactic:
rw [(h n).resolve_right hn]

Premises used: Or.resolve_right
-- Module: Mathlib.RingTheory.WittVector.InitTail
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

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]
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
h₁ : ∀ (n : ℕ), (select (fun (i : ℕ) ↦ ¬P i) z).coeff n = y.coeff n
⊢ select (fun (i : ℕ) ↦ ¬P i) z = y

Tactic:
ext1 n
-- Module: Mathlib.RingTheory.WittVector.InitTail
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 : ℕ
h₁ : (if ¬P n then if P n then x.coeff n else y.coeff n else 0) = y.coeff n
⊢ (select (fun (i : ℕ) ↦ ¬P i) z).coeff n = y.coeff n

Tactic:
rw [select, coeff_mk, coeff_mk]

Premises used: WittVector.select, WittVector.coeff_mk
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
neg : ∀ (hn : ¬P n), y.coeff n = y.coeff n
⊢ (if ¬P n then if P n then x.coeff n else y.coeff n else 0) = y.coeff n

Tactic:
split_ifs with hn
-- Module: Mathlib.RingTheory.WittVector.InitTail
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 : ℕ
hn : P n
⊢ 0 = y.coeff n

Tactic:
hn.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.WittVector.InitTail
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 : ℕ
hn : P n
⊢ 0 = y.coeff n

Tactic:
exact hn.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.WittVector.InitTail
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 : ℕ
hn : ¬P n
⊢ y.coeff n = y.coeff n

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.InitTail
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

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
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
rw₂ rw₃ : z.coeff n = z.coeff n
⊢ (x + y).coeff n = z.coeff n

Tactic:
rw [← hx, ← hy, select_add_select_not P z]

Premises used: WittVector.select_add_select_not
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
simp : (if P n then x.coeff n else y.coeff n) = x.coeff n + y.coeff n
⊢ z.coeff n = x.coeff n + y.coeff n

Tactic:
simp only [z, mk.eq_1]

Premises used: WittVector.mk.eq_1
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
neg : ∀ (y0 : ¬P n), y.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

Tactic:
split_ifs with y0
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
pos₁ pos₂ : x.coeff n = x.coeff n
⊢ x.coeff n = x.coeff n + y.coeff n

Tactic:
rw [y0, add_zero]

Premises used: add_zero
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
neg₁ neg₂ : y.coeff n = y.coeff n
⊢ y.coeff n = x.coeff n + y.coeff n

Tactic:
rw [h n |>.resolve_right y0, zero_add]

Premises used: zero_add, Or.resolve_right
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
n₂ : z.coeff n = x.coeff n + y.coeff n
⊢ (x + y).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]

Premises used: HAdd.hAdd, WittVector.coeff
-- Module: Mathlib.RingTheory.WittVector.InitTail
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ init n x + tail n x = x

Tactic:
simp only [init, tail, ← not_lt, select_add_select_not]

Premises used: WittVector.init, WittVector.tail, not_lt, WittVector.select_add_select_not
-- Module: Mathlib.RingTheory.WittVector.InitTail
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_ring₆ 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
⊢ init n (init n x) = init n x

Tactic:
init_ring
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
pos 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
⊢ init n (x + y) = init n (init n x + init n y)

Tactic:
init_ring using wittAdd_vars

Premises used: WittVector.wittAdd_vars
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
pos 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
⊢ init n (x * y) = init n (init n x * init n y)

Tactic:
init_ring using wittMul_vars

Premises used: WittVector.wittMul_vars
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
pos 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
⊢ init n (-x) = init n (-init n x)

Tactic:
init_ring using wittNeg_vars

Premises used: WittVector.wittNeg_vars
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
pos 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
⊢ init n (x - y) = init n (init n x - init n y)

Tactic:
init_ring using wittSub_vars

Premises used: WittVector.wittSub_vars
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
pos 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
⊢ init n (m • x) = init n (m • init n x)

Tactic:
init_ring using fun p [Fact (Nat.Prime p)] n => wittNSMul_vars p m n

Premises used: WittVector.wittNSMul_vars
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
pos 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
⊢ init n (m • x) = init n (m • init n x)

Tactic:
init_ring using fun p [Fact (Nat.Prime p)] n => wittZSMul_vars p m n

Premises used: WittVector.wittZSMul_vars
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
pos 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
⊢ init n (x ^ m) = init n (init n x ^ m)

Tactic:
init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n

Premises used: WittVector.wittPow_vars
-- Module: Mathlib.RingTheory.WittVector.InitTail
Goal:
p n : ℕ
⊢ IsPoly.{u_2} p fun (x : Type u_2) (x_1 : CommRing x) ↦ init n

Tactic:
select_isPoly (P := fun i => i < n)

Premises used: WittVector.init, WittVector.select_isPoly
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 × ℕ) ℤ)
h₁ : ∀ (n : ℕ), f n = g n
⊢ f = g

Tactic:
ext1 n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
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 × ℕ) ℤ)
n : ℕ
h₁ :
  Eq (α := MvPolynomial (idx × ℕ) ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (f n) :
      MvPolynomial (idx × ℕ) ℚ)
    ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial (idx × ℕ) ℤ) → MvPolynomial (idx × ℕ) ℚ) (g n) :
      MvPolynomial (idx × ℕ) ℚ)
⊢ f n = g n

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Premises used: Rat, MvPolynomial.map_injective, Int.castRingHom, Int.cast_injective