awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
calc_6 calc_6₁ :
  (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x) =
    (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
      ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
k : ℕ
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff k = x.coeff k ^ HPow.hPow (β := ℕ) p 0

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] x).coeff k = x.coeff k ^ p ^ i
succ : (x.coeff k ^ p ^ i) ^ p = x.coeff k ^ p ^ (i + 1)
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] x).coeff k = x.coeff k ^ p ^ (i + 1)

Tactic:
rw [iterate_succ_apply', coeff_frobenius_charP, ih]

Premises used: Function.iterate_succ_apply', WittVector.coeff_frobenius_charP
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
k i : ℕ
ih : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] x).coeff k = x.coeff k ^ p ^ i
⊢ (x.coeff k ^ p ^ i) ^ p = x.coeff k ^ p ^ (i + 1)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
i k : ℕ
zero : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[0] x).coeff k = x.coeff k ^ HPow.hPow (β := ℕ) p 0
succ :
  ∀ (i : ℕ) (ih : ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] x).coeff k = x.coeff k ^ p ^ i),
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i + 1] x).coeff k = x.coeff k ^ p ^ (i + 1)
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] x).coeff k = x.coeff k ^ p ^ i

Tactic:
induction i with
  | zero => simp
  | succ i ih => rw [iterate_succ_apply', coeff_frobenius_charP, ih]; ring_nf

Premises used: Function.iterate_succ_apply', WittVector.coeff_frobenius_charP
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j)

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j) =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Tactic:
?_
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
calc_1 :
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j)
calc_2 :
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j) =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0
calc_3 :
  ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0
calc_4 :
  ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Tactic:
calc
    _ = (verschiebung^[i + j] (frobenius^[j] x * frobenius^[i] y)).coeff (i + j) := ?_
    _ = (frobenius^[j] x * frobenius^[i] y).coeff 0 := ?_
    _ = (frobenius^[j] x).coeff 0 * (frobenius^[i] y).coeff 0 := ?_
    _ = _ := ?_

Premises used: HMul.hMul, WittVector.frobenius, Nat.iterate, HAdd.hAdd, WittVector.coeff, OfNat.ofNat, DFunLike.coe, WittVector.verschiebung
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
calc_1 calc_1₁ :
  ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j) =
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j)
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i] x * (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[j] y).coeff (i + j) =
    ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j)

Tactic:
rw [iterate_verschiebung_mul]

Premises used: WittVector.iterate_verschiebung_mul
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (0 + (i + j)) =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0

Tactic:
iterate_verschiebung_coeff (p := p) (R := R) _ _ _

Premises used: WittVector.iterate_verschiebung_coeff
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
h : i + j = 0 + (i + j)
⊢ ((⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[i + j]
          ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y)).coeff
      (i + j) =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0

Tactic:
convert! iterate_verschiebung_coeff (p := p) (R := R) _ _ _ using 2

Premises used: WittVector.iterate_verschiebung_coeff
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
h h₁ : i + j = i + j
⊢ i + j = 0 + (i + j)

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x * (⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
    ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0

Tactic:
apply mul_coeff_zero

Premises used: WittVector.mul_coeff_zero
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x y : 𝕎 R
i j : ℕ
⊢ ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[j] x).coeff 0 * ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[i] y).coeff 0 =
    x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i

Tactic:
simp only [iterate_frobenius_coeff]

Premises used: WittVector.iterate_frobenius_coeff
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
rw :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
⊢ (⇑verschiebung : (a : 𝕎 R) → 𝕎 R)^[n] ((⇑frobenius : (a : 𝕎 R) → 𝕎 R)^[n] x) = x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n

Tactic:
rw [← comp_apply (f := verschiebung^[n]),
      ← Function.Commute.comp_iterate verschiebung_frobenius_comm]

Premises used: Function.Commute.comp_iterate, WittVector.verschiebung_frobenius_comm, Function.comp_apply
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[0] x =
    x * HPow.hPow (α := 𝕎 R) (β := ℕ) (↑p : 𝕎 R) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Identities
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
inst_1 : CharP R p
x : 𝕎 R
n : ℕ
ih :
  (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n
succ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      ((comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₁ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)
succ₂ :
  comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R)
      (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) =
    x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
succ₃ :
  (verschiebung : (a : 𝕎 R) → 𝕎 R) ((frobenius : (a : 𝕎 R) → 𝕎 R) (x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n) : 𝕎 R) =
    x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
succ₄ : x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R) = x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
succ₅ succ₆ :
  x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R)) = x * (HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n * (↑p : 𝕎 R))
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n + 1] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) (n + 1)

Tactic:
rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]

Premises used: Function.iterate_succ_apply', pow_succ, mul_assoc, WittVector.verschiebung_frobenius, Function.comp_apply
-- Module: Mathlib.RingTheory.WittVector.Identities
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
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)
⊢ (comp (β := 𝕎 R) (⇑verschiebung : (a : 𝕎 R) → 𝕎 R) (⇑frobenius : (a : 𝕎 R) → 𝕎 R))^[n] x =
    x * HPow.hPow (α := 𝕎 R) (↑p : 𝕎 R) n

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]

Premises used: Function.iterate_succ_apply', pow_succ, mul_assoc, WittVector.verschiebung_frobenius, Function.comp_apply
-- Module: Mathlib.RingTheory.WittVector.InitTail
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
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)
⊢ (select P x).coeff n =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (selectPoly P n)

Tactic:
dsimp [select, selectPoly]

Premises used: WittVector.select, WittVector.selectPoly
-- Module: Mathlib.RingTheory.WittVector.InitTail
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)
neg :
  ∀ (hi : ¬P n),
    Eq (α := R) (0 : R) (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) 0 : R)
⊢ (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:
split_ifs with hi
-- Module: Mathlib.RingTheory.WittVector.InitTail
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ x.coeff n = ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (X n)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.InitTail
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ Eq (α := R) (0 : R) (((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.InitTail
Goal:
p n : ℕ
R : Type u_1
inst : CommRing R
P_1 P : ℕ → Prop
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)
⊢ IsPoly.{u_2} p fun (x : Type u_2) (x_1 : CommRing x) (x_2 : 𝕎 x) ↦ select P x_2

Tactic:
use selectPoly P

Premises used: WittVector.selectPoly
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
h :
  ∀ (i : ℕ),
    (select P x).coeff i =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (selectPoly P i)
⊢ (select P x).coeff = fun (n : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (selectPoly P n)

Tactic:
funext i
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
i : ℕ
⊢ (select P x).coeff i =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (selectPoly P i)

Tactic:
apply coeff_select

Premises used: WittVector.coeff_select
-- Module: Mathlib.RingTheory.WittVector.InitTail
Goal:
p : ℕ
R : Type u_1
inst : CommRing R
P : ℕ → Prop
hp : Fact (Nat.Prime p)
⊢ 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)
-- Module: Mathlib.RingTheory.WittVector.InitTail
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
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)
⊢ ∀ (x : 𝕎 R), select P x + select (fun (i : ℕ) ↦ ¬P i) x = x

Tactic:
ghost_calc x
-- 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 :
  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
⊢ 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:
simp only [map_add]

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

Premises used: MvPolynomial.aeval, WittVector.coeff
-- Module: Mathlib.RingTheory.WittVector.InitTail
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 :
  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)
⊢ 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:
simpa only [map_add, aeval_bind₁, ← coeff_select]

Premises used: map_add, MvPolynomial.aeval_bind₁, WittVector.coeff_select
-- 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 :
  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

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]
-- 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 :
  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)))
⊢ 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:
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]

Premises used: Finset.sum_add_distrib, MvPolynomial.bind₁_C_right, map_pow, WittVector.selectPoly, map_sum, map_mul, mul_add, MvPolynomial.bind₁_X_right, wittPolynomial_eq_sum_C_mul_X_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 : ℕ
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))
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- 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 : ℕ
⊢ ∀ 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:
fun m _ => mul_eq_mul_left_iff.mpr (Or.inl ?_)

Premises used: Iff.mpr, mul_eq_mul_left_iff, Or.inl