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 : ℕ
x y_1 : 𝕎 k
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
y : 𝕎 k
rw : HPow.hPow (α := k) (β := ℕ) 0 0 * y.coeff 0 ^ p ^ (n + 1 - 0) = y.coeff 0 ^ p ^ (n + 1)
h : 0 ∈ range (n + 1 + 1)
h₀ : ∀ b ∈ range (n + 1 + 1), b ≠ 0 → HPow.hPow (α := k) 0 b * y.coeff b ^ p ^ (n + 1 - b) = 0
⊢ ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)

Tactic:
rw [Finset.sum_eq_single_of_mem 0]

Premises used: Finset.sum_eq_single_of_mem, OfNat.ofNat
-- 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_1 : 𝕎 k
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
y : 𝕎 k
⊢ HPow.hPow (α := k) (β := ℕ) 0 0 * y.coeff 0 ^ p ^ (n + 1 - 0) = y.coeff 0 ^ p ^ (n + 1)

Tactic:
simp +contextual
-- 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_1 : 𝕎 k
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
y : 𝕎 k
⊢ 0 ∈ range (n + 1 + 1)

Tactic:
simp +contextual
-- 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_1 : 𝕎 k
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
y : 𝕎 k
⊢ ∀ b ∈ range (n + 1 + 1), b ≠ 0 → HPow.hPow (α := k) 0 b * y.coeff b ^ p ^ (n + 1 - b) = 0

Tactic:
simp +contextual
-- 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
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
⊢ ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)

Tactic:
have sum_zero_pow_mul_pow_p (y : 𝕎 k) : ∑ x ∈ range (n + 1 + 1),
      (0 : k) ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1) := by
    rw [Finset.sum_eq_single_of_mem 0] <;> simp +contextual
-- 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
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
e_a : ∑ x_1 ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) = x.coeff 0 ^ p ^ (n + 1)
e_a₁ : ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ (x * y).coeff (n + 1) -
        y.coeff (n + 1) * ∑ x_1 ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) -
      x.coeff (n + 1) * ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) =
    (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:
congr
-- 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
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ ∑ x_1 ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) = x.coeff 0 ^ p ^ (n + 1)

Tactic:
apply sum_zero_pow_mul_pow_p
-- 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
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)

Tactic:
apply sum_zero_pow_mul_pow_p
-- 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 : ℕ
simp :
  ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k),
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]
⊢ ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k),
    ∀ (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)

Tactic:
simp only [← peval_polyOfInterest']

Premises used: WittVector.peval_polyOfInterest'
-- 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₀ : ((↑(↑(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),
      ∀ (x y : 𝕎 k),
        f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
          peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]
⊢ ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k),
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]

Tactic:
obtain ⟨f₀, hf₀⟩ := exists_restrict_to_vars (s := SetLike.coe (univ ×ˢ range (n + 1))) k
    (polyOfInterest_vars p n)

Premises used: WittVector.polyOfInterest_vars, MvPolynomial.exists_restrict_to_vars
-- 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)
x y : TruncatedWittVector p (n + 1) k
apply : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type) → k
⊢ k

Tactic:
apply 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₀ : ((↑(↑(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)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))
apply : Fin (Nat.succ 0).succ × Fin (n + 1)
⊢ k

Tactic:
apply Function.uncurry ![x, y]

Premises used: Matrix.vecEmpty, Function.uncurry, Matrix.vecCons
-- 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)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))
S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n}
⊢ a ∈ S

Tactic:
grind
-- 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)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))
S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n}
⊢ a ∈ S

Tactic:
have ha' : a ∈ S := by grind
-- 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)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))
S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n}
ha' : a ∈ S
refine : a.2 < n + 1
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)

Tactic:
refine ⟨a.fst, ⟨a.snd, ?_⟩⟩
-- 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)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))
S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n}
ha' : a ∈ S
inl :
  ∀ (f₀ : ((↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (a.2 + 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 (a.2 + 1))) : Set (Fin 2 × ℕ)))) =
          ((aeval (R := ℤ) x : 𝕄 →ₐ[ℤ] k) : (a : 𝕄) → k) (polyOfInterest p a.2))
    (x y : TruncatedWittVector p (a.2 + 1) k)
    (ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (a.2 + 1))) : Set (Fin 2 × ℕ))), a.2 < a.2 + 1
inr : a.2 < n → a.2 < n + 1
⊢ a.2 < n + 1

Tactic:
obtain ⟨ha, ha⟩ := ha'
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst : CommRing k
inst_1 : CharP k p
a : Fin 2 × ℕ
f₀ : ((↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (a.2 + 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 (a.2 + 1))) : Set (Fin 2 × ℕ)))) =
      ((aeval (R := ℤ) x : 𝕄 →ₐ[ℤ] k) : (a : 𝕄) → k) (polyOfInterest p a.2)
x y : TruncatedWittVector p (a.2 + 1) k
ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (a.2 + 1))) : Set (Fin 2 × ℕ))
S : Set (Fin 2 × ℕ) := {a_1 : Fin 2 × ℕ | a_1.2 = a.2 ∨ a_1.2 < a.2}
⊢ a.2 < a.2 + 1

Tactic:
lia
-- 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)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ (↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ))
S : Set (Fin 2 × ℕ) := {a : Fin 2 × ℕ | a.2 = n ∨ a.2 < n}
h : a.2 < n
⊢ a.2 < n + 1

Tactic:
lia
-- 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, ⋯⟩))
h :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]
⊢ ∃ (f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k),
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]

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₀ : ((↑(↑(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
h :
  (f₀ 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, ⋯⟩ : Fin (n + 1))) =
    ((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
            (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
          𝕄 →ₐ[ℤ] k) :
        (a : 𝕄) → k)
      (polyOfInterest p n)
⊢ f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
    peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]

Tactic:
dsimp [f, peval]

Premises used: WittVector.peval
-- 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
h :
  (f₀ 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, ⋯⟩ : Fin (n + 1))) =
    f₀
      (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 × ℕ))))
⊢ (f₀ 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, ⋯⟩ : Fin (n + 1))) =
    ((aeval.{0, u_1, 0} (R := ℤ) (S₁ := k) (σ := Fin 2 × ℕ)
            (Function.uncurry ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]) :
          𝕄 →ₐ[ℤ] k) :
        (a : 𝕄) → k)
      (polyOfInterest p n)

Tactic:
rw [← hf₀]
-- 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
h :
  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 × ℕ))))
⊢ (f₀ 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, ⋯⟩ : Fin (n + 1))) =
    f₀
      (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 × ℕ))))

Tactic:
congr
-- 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
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, ⋯⟩ : 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)
⊢ 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 × ℕ))))

Tactic:
ext a