awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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
⊢ Eq.{u_1 + 1} (α := (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type) → k)
    (fun (a : ↥(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))) ↦
      ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑a : Fin 2 × ℕ).1 ⟨(↑a : Fin 2 × ℕ).2, ⋯⟩)
    (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 × ℕ))))
have h : ∀ (a : ↥(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1)))),
  Eq (α := k) (![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑a : Fin 2 × ℕ).1 ⟨(↑a : Fin 2 × ℕ).2, sorry⟩ : 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: ext a
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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)))
⊢ 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)
have 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,
          sorry⟩ :
      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 ⟨a, ha⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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))
⊢ 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)
have 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,
          sorry⟩ :
      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)
Tactic: obtain ⟨i, m⟩ := a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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),
    ∀ (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)
have 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)
Tactic: obtain ⟨f, hf⟩ := nth_mul_coeff' p k n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use f
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (goal)
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) +
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
have 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))
Tactic: rw [hf x y]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
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 : ℕ
⊢ (x * (↑(n + 1) : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p (n + 1) k)
have 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)
Tactic: rw [wittMulN, Nat.cast_add, Nat.cast_one, mul_add, mul_one, aeval_bind₁, add_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
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 : ℕ
⊢ 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)
have 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))
Tactic: ext1 ⟨b, i⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
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 : ℕ
⊢ 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))
have h : Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2), i) =
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
    (Function.uncurry ![wittMulN p n, X] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2), i))
Tactic: fin_cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
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))
⊢ 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))
have h₁ : Function.uncurry ![(x * (↑n : 𝕎 R)).coeff, x.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2), i) =
  ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R)
    (Function.uncurry ![wittMulN p n, X] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2), i))
Tactic: fin_cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
Goal:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst : CommRing R
n : ℕ
x : 𝕎 R
k : ℕ
⊢ (x * (↑n : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
have zero : ∀ (k : ℕ),
  (x * (↑0 : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p 0 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]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
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)
⊢ (x * (↑n : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
have 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)
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]
Cleared hypotheses: n, k
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
⊢ (x * (↑n : 𝕎 R)).coeff = fun (n_1 : ℕ) ↦
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n n_1)
have h : ∀ (k : ℕ),
  (x * (↑n : 𝕎 R)).coeff k =
    ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R) : (a : MvPolynomial ℕ ℤ) → R) (wittMulN p n k)
Tactic: funext k
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih :
  (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
⊢ (bind₁ (wittMulN p (n + 1)) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑(n + 1) : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
have succ : (bind₁ (Function.uncurry ![wittMulN p n, X]) : (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
    ((bind₁ fun (i : Fin 2) ↦
          (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
        (a : MvPolynomial (Fin 2) ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ)
      (HAdd.hAdd (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) =
  HMul.hMul (α := MvPolynomial ℕ ℤ) (↑(n + 1) : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
Tactic: rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih :
  (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
⊢ (bind₁ (Function.uncurry ![wittMulN p n, X]) : (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
      ((bind₁ fun (i : Fin 2) ↦
            (rename (Prod.mk i) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k) :
          (a : MvPolynomial (Fin 2) ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ)
        (HAdd.hAdd (α := MvPolynomial (Fin 2) ℤ) (X 0) (X 1))) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑(n + 1) : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
have succ : HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
    ((bind₁ (Function.uncurry ![wittMulN p n, X]) : (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
        ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k)) :
      MvPolynomial ℕ ℤ)
    ((bind₁ (Function.uncurry ![wittMulN p n, X]) : (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
        ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k)) :
      MvPolynomial ℕ ℤ) =
  HAdd.hAdd (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) 1 * wittPolynomial p ℤ k
Tactic: simp only [map_add, Nat.cast_succ, bind₁_X_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
ih :
  (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
⊢ HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X]) :
            (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
          ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k)) :
        MvPolynomial ℕ ℤ)
      ((bind₁ (Function.uncurry ![wittMulN p n, X]) :
            (a : MvPolynomial (Fin (Nat.succ 0).succ × ℕ) ℤ) → MvPolynomial ℕ ℤ)
          ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (wittPolynomial p ℤ k)) :
        MvPolynomial ℕ ℤ) =
    HAdd.hAdd (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) 1 * wittPolynomial p ℤ k
have succ : HAdd.hAdd (α := MvPolynomial ℕ ℤ) (β := MvPolynomial ℕ ℤ)
    ((bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
        (wittPolynomial p ℤ k) :
      MvPolynomial ℕ ℤ)
    ((bind₁ (Function.uncurry ![wittMulN p n, X] ∘ Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ)
        (wittPolynomial p ℤ k) :
      MvPolynomial ℕ ℤ) =
  HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) + wittPolynomial p ℤ k
Tactic: rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulP (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n k : ℕ
⊢ (bind₁ (wittMulN p n) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
    HMul.hMul (α := MvPolynomial ℕ ℤ) (↑n : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
have zero : (bind₁ (wittMulN p 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k) =
  HMul.hMul (α := MvPolynomial ℕ ℤ) (↑0 : MvPolynomial ℕ ℤ) (wittPolynomial p ℤ k)
Tactic: induction n with
  | zero => simp [wittMulN, zero_mul, bind₁_zero_wittPolynomial]
  | succ n ih =>
    rw [wittMulN, ← bind₁_bind₁, wittAdd, wittStructureInt_prop]
    simp only [map_add, Nat.cast_succ, bind₁_X_right]
    rw [add_mul, one_mul, bind₁_rename, bind₁_rename]
    simp only [ih, Function.uncurry, Function.comp_def, bind₁_X_left, AlgHom.id_apply,
      Matrix.cons_val_zero, Matrix.cons_val_one]
Cleared hypotheses: n