awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
f₀ : ((↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type) → k) → k
hf₀ :
  ∀ (x : Fin 2 × ℕ → k),
    f₀
        (x ∘
          Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
            x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)))) =
      ((aeval (R := ℤ) x : 𝕄 →ₐ[ℤ] k) : (a : 𝕄) → k) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun (x y : TruncatedWittVector p (n + 1) k) ↦
    f₀ fun (a : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type)) ↦
      Subtype.casesOn (p := fun (x : Fin 2 × ℕ) ↦
        x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))) (motive :=
        fun (x : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type)) ↦ k) a
        fun (a : Fin 2 × ℕ) (ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))) ↦
        Function.uncurry ![x, y]
          (let S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
a : ↥(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))
h :
  ∀ (a : Fin 2 × ℕ) (ha : a ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))),
    Eq (α := k)
      (![truncateFun (n + 1) x, truncateFun (n + 1) y]
          (↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) a ha) :
              Fin 2 × ℕ).1
          ⟨(↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) a ha) :
                Fin 2 × ℕ).2,
            ⋯⟩ :
        k)
      ((Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] ∘
            Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
              x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))))
          (Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) a ha) :
        k)
⊢ Eq (α := k) (![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑a : Fin 2 × ℕ).1 ⟨(↑a : Fin 2 × ℕ).2, ⋯⟩ : k)
    ((Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] ∘
          Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
            x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))))
        a :
      k)

Tactic:
obtain ⟨a, ha⟩ := a
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
f₀ : ((↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type) → k) → k
hf₀ :
  ∀ (x : Fin 2 × ℕ → k),
    f₀
        (x ∘
          Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
            x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)))) =
      ((aeval (R := ℤ) x : 𝕄 →ₐ[ℤ] k) : (a : 𝕄) → k) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun (x y : TruncatedWittVector p (n + 1) k) ↦
    f₀ fun (a : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type)) ↦
      Subtype.casesOn (p := fun (x : Fin 2 × ℕ) ↦
        x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))) (motive :=
        fun (x : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type)) ↦ k) a
        fun (a : Fin 2 × ℕ) (ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))) ↦
        Function.uncurry ![x, y]
          (let S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
a : Fin 2 × ℕ
ha : a ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
h :
  ∀ (i : Fin 2) (m : ℕ) (ha : (i, m) ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))),
    Eq (α := k)
      (![truncateFun (n + 1) x, truncateFun (n + 1) y]
          (↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) (i, m)
                  ha) :
              Fin 2 × ℕ).1
          ⟨(↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) (i, m)
                    ha) :
                Fin 2 × ℕ).2,
            ⋯⟩ :
        k)
      ((Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] ∘
            Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
              x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))))
          (Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) (i, m)
            ha) :
        k)
⊢ Eq (α := k)
    (![truncateFun (n + 1) x, truncateFun (n + 1) y]
        (↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) a ha) :
            Fin 2 × ℕ).1
        ⟨(↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) a ha) :
              Fin 2 × ℕ).2,
          ⋯⟩ :
      k)
    ((Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] ∘
          Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
            x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))))
        (Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) a ha) :
      k)

Tactic:
obtain ⟨i, m⟩ := a
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
f₀ : ((↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type) → k) → k
hf₀ :
  ∀ (x : Fin 2 × ℕ → k),
    f₀
        (x ∘
          Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
            x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)))) =
      ((aeval (R := ℤ) x : 𝕄 →ₐ[ℤ] k) : (a : 𝕄) → k) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun (x y : TruncatedWittVector p (n + 1) k) ↦
    f₀ fun (a : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type)) ↦
      Subtype.casesOn (p := fun (x : Fin 2 × ℕ) ↦
        x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))) (motive :=
        fun (x : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type)) ↦ k) a
        fun (a : Fin 2 × ℕ) (ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))) ↦
        Function.uncurry ![x, y]
          (let S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
m : ℕ
ha : ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, m) ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ Eq (α := k)
    (![truncateFun (n + 1) x, truncateFun (n + 1) y]
        (↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))
                ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), m) ha) :
            Fin 2 × ℕ).1
        ⟨(↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))
                  ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), m) ha) :
              Fin 2 × ℕ).2,
          ⋯⟩ :
      k)
    ((Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] ∘
          Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
            x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))))
        (Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), m) ha) :
      k)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
f₀ : ((↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type) → k) → k
hf₀ :
  ∀ (x : Fin 2 × ℕ → k),
    f₀
        (x ∘
          Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
            x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)))) =
      ((aeval (R := ℤ) x : 𝕄 →ₐ[ℤ] k) : (a : 𝕄) → k) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun (x y : TruncatedWittVector p (n + 1) k) ↦
    f₀ fun (a : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type)) ↦
      Subtype.casesOn (p := fun (x : Fin 2 × ℕ) ↦
        x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))) (motive :=
        fun (x : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type)) ↦ k) a
        fun (a : Fin 2 × ℕ) (ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))) ↦
        Function.uncurry ![x, y]
          (let S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
m : ℕ
ha : ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, m) ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ Eq (α := k)
    (![truncateFun (n + 1) x, truncateFun (n + 1) y]
        (↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))
                ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), m) ha) :
            Fin 2 × ℕ).1
        ⟨(↑(Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))
                  ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), m) ha) :
              Fin 2 × ℕ).2,
          ⋯⟩ :
      k)
    ((Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] ∘
          Subtype.val (p := fun (x : Fin 2 × ℕ) ↦
            x ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))))
        (Subtype.mk (p := fun (x : Fin 2 × ℕ) ↦ x ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), m) ha) :
      k)

Tactic:
rfl
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
obtain :
  ∀ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k)
    (hf :
      ∀ (x y : 𝕎 k),
        f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
          (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) -
            x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)),
    ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k),
      ∀ (x y : 𝕎 k),
        (x * y).coeff (n + 1) =
          x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
            f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
⊢ ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k),
    ∀ (x y : 𝕎 k),
      (x * y).coeff (n + 1) =
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
obtain ⟨f, hf⟩ := nth_mul_coeff' p k n

Premises used: WittVector.nth_mul_coeff'
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
h :
  ∀ (x y : 𝕎 k),
    (x * y).coeff (n + 1) =
      x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
        f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
⊢ ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k),
    ∀ (x y : 𝕎 k),
      (x * y).coeff (n + 1) =
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
use f
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
x y : 𝕎 k
h :
  (x * y).coeff (n + 1) =
    x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
      ((x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1))
⊢ (x * y).coeff (n + 1) =
    x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
rw [hf x y]
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
x y : 𝕎 k
⊢ (x * y).coeff (n + 1) =
    x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
      ((x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1))

Tactic:
ring
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
n : ℕ
x y : 𝕎 k
⊢ (x * y).coeff (n + 1) =
    x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
      nthRemainder p n (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
Classical.choose_spec (nth_mul_coeff p k n) _ _

Premises used: Classical.choose_spec, WittVector.nth_mul_coeff, WittVector.nthRemainder, TruncatedWittVector
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * (↑0 : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p 0 k)

Tactic:
simp only [Nat.cast_zero, mul_zero, zero_coeff, wittMulN, Pi.zero_apply, map_zero]

Premises used: Pi.zero_apply, map_zero, WittVector.zero_coeff, MulZeroClass.mul_zero, Nat.cast_zero, WittVector.wittMulN
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
ih :
  ∀ (k : ℕ),
    (x * (↑n : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
k : ℕ
succ :
  peval (wittAdd p k) ![(x * (↑n : 𝕎 R)).coeff, x.coeff] =
    ((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
            ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
              (Function.uncurry ![wittMulN p n, X] i) :
          MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ →ₐ[ℤ] R) :
        (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → R)
      (wittAdd p k)
⊢ (x * (↑(n + 1) : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p (n + 1) k)

Tactic:
rw [wittMulN, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁, add_coeff]

Premises used: MvPolynomial.aeval_bind₁, Nat.cast_add, mul_add, mul_one, WittVector.add_coeff, Nat.cast_one, WittVector.wittMulN
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
ih :
  ∀ (k : ℕ),
    (x * (↑n : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
k : ℕ
apply :
  Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] = fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (Function.uncurry ![wittMulN p n, X] i)
⊢ peval (wittAdd p k) ![(x * (↑n : 𝕎 R)).coeff, x.coeff] =
    ((aeval.{0, u_1, 0} (R := ℤ) (S₁ := R) fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
            ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
              (Function.uncurry ![wittMulN p n, X] i) :
          MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ →ₐ[ℤ] R) :
        (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → R)
      (wittAdd p k)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
ih :
  ∀ (k : ℕ),
    (x * (↑n : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
k : ℕ
h :
  ∀ (b : Fin 2) (i : ℕ),
    Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] (b, i) =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
        (Function.uncurry ![wittMulN p n, X] (b, i))
⊢ Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] = fun (i : Fin (Nat.succ 0).succ × ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (Function.uncurry ![wittMulN p n, X] i)

Tactic:
ext1 ⟨b, i⟩
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
ih :
  ∀ (k : ℕ),
    (x * (↑n : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
k : ℕ
b : Fin 2
i : ℕ
h :
  Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), i) =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (Function.uncurry ![wittMulN p n, X] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), i))
h₁ :
  Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), i) =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (Function.uncurry ![wittMulN p n, X] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), i))
⊢ Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] (b, i) =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (Function.uncurry ![wittMulN p n, X] (b, i))

Tactic:
fin_cases b
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
ih :
  ∀ (k : ℕ),
    (x * (↑n : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), i) =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (Function.uncurry ![wittMulN p n, X] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), i))

Tactic:
simp [Function.uncurry, Matrix.cons_val_zero, ih]

Premises used: Matrix.cons_val_zero, Function.uncurry
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
x : 𝕎 R
n : ℕ
ih :
  ∀ (k : ℕ),
    (x * (↑n : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), i) =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
      (Function.uncurry ![wittMulN p n, X] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), i))

Tactic:
simp [Function.uncurry, Matrix.cons_val_one, aeval_X]

Premises used: MvPolynomial.aeval_X, Matrix.cons_val_one, Function.uncurry
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
n : ℕ
x : 𝕎 R
k : ℕ
zero :
  ∀ (k : ℕ),
    (x * (↑0 : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p 0 k)
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ (k : ℕ),
        (x * (↑n : 𝕎 R)).coeff k =
          ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k))
    (k : ℕ),
    (x * (↑(n + 1) : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p (n + 1) k)
⊢ (x * (↑n : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)

Tactic:
induction n generalizing k with
  | zero => simp only [Nat.cast_zero, mul_zero, zero_coeff, wittMulN, Pi.zero_apply, map_zero]
  | succ n ih =>
    rw [wittMulN, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁, add_coeff]
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext1 ⟨b, i⟩
    fin_cases b
    · simp [Function.uncurry, Matrix.cons_val_zero, ih]
    · simp [Function.uncurry, Matrix.cons_val_one, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.eval₂Hom_congr, Matrix.cons_val_one, Matrix.cons_val_zero, Pi.zero_apply, map_zero, MvPolynomial.aeval_bind₁, RingHom.ext_int, WittVector.zero_coeff, MulZeroClass.mul_zero, Nat.cast_add, mul_add, Nat.cast_zero, Function.uncurry, mul_one, WittVector.add_coeff, Nat.cast_one, WittVector.wittMulN, rfl
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
h :
  ∀ (k : ℕ),
    (x * (↑n : 𝕎 R)).coeff k =
      ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
⊢ (x * (↑n : 𝕎 R)).coeff = fun (n_1 : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n n_1)

Tactic:
funext k
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * (↑n : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)

Tactic:
mulN_coeff n x k

Premises used: WittVector.mulN_coeff
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * (↑n : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)

Tactic:
exact mulN_coeff n x k

Premises used: WittVector.mulN_coeff
-- Module: Mathlib.RingTheory.WittVector.MulP
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ (bind₁ (wittMulN p 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑0 : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)

Tactic:
simp [wittMulN, zero_mul, bind₁_zero_wittPolynomial]

Premises used: MulZeroClass.zero_mul, WittVector.bind₁_zero_wittPolynomial, WittVector.wittMulN