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 : ℕ
x y : 𝕎 k
⊢ peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i] =
    (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)
have rw : (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
      y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
    x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i) =
  (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 [peval_polyOfInterest]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (hypothesis)
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) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i) =
    (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)
have this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
Tactic: have : (p : k) = 0 := CharP.cast_eq_zero k p
-- 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 : ℕ
x y : 𝕎 k
this : Eq.{u_1 + 1} (α := k) (↑p : k) 0
⊢ (x * y).coeff (n + 1) + HPow.hPow (α := k) (↑p : k) (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), HPow.hPow (α := k) (↑p : k) i * y.coeff i ^ p ^ (n + 1 - i) =
    (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)
have simp : (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: simp only [this, ne_eq, add_eq_zero, and_false, zero_pow, zero_mul, add_zero,
    not_false_eq_true, reduceCtorEq]
-- 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 : ℕ
x y_1 : 𝕎 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)
have rw : HPow.hPow (α := k) (β := ℕ) 0 0 * y.coeff 0 ^ p ^ (n + 1 - 0) = y.coeff 0 ^ p ^ (n + 1)
Tactic: rw [Finset.sum_eq_single_of_mem 0]
-- 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 : ℕ
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)
⊢ ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
have h : 0 ∈ range (n + 1 + 1)
Tactic: rw [Finset.sum_eq_single_of_mem 0]
-- 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 : ℕ
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)
⊢ ∑ x ∈ range (n + 1 + 1), HPow.hPow (α := k) 0 x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
have h₀ : ∀ b ∈ range (n + 1 + 1), b ≠ 0 → HPow.hPow (α := k) 0 b * y.coeff b ^ p ^ (n + 1 - b) = 0
Tactic: rw [Finset.sum_eq_single_of_mem 0]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (hypothesis)
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
⊢ (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)
have 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)
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
-- 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 : ℕ
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 * 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)
have 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)
Tactic: congr
-- 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 : ℕ
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)
⊢ (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)
have 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)
Tactic: congr
-- 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),
      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)
have 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]
Tactic: simp only [← peval_polyOfInterest']
-- 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),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]
have 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]
Tactic: obtain ⟨f₀, hf₀⟩ := exists_restrict_to_vars (s := SetLike.coe (univ ×ˢ range (n + 1))) k
    (polyOfInterest_vars p 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₀ : ((↑(↑(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
⊢ k
have apply : (↑(↑(SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))) : Set (Fin 2 × ℕ)) : Type) → k
Tactic: apply 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₀ : ((↑(↑(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 × ℕ))
⊢ k
have apply : Fin (Nat.succ 0).succ × Fin (n + 1)
Tactic: apply Function.uncurry ![x, y]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.MulCoeff (hypothesis)
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}
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)
have ha' : a ∈ S
Tactic: have ha' : a ∈ S := by grind
-- 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)
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
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)
have refine : a.2 < n + 1
Tactic: refine ⟨a.fst, ⟨a.snd, ?_⟩⟩
-- 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)
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
⊢ a.2 < n + 1
have 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
Tactic: obtain ⟨ha, ha⟩ := ha'
Cleared hypotheses: n, f₀, hf₀, x, y, ha, S, 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₀ : ((↑(↑(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
⊢ a.2 < n + 1
have inr : a.2 < n → a.2 < n + 1
Tactic: obtain ⟨ha, ha⟩ := ha'
Cleared hypotheses: 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₀ : ((↑(↑(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, ⋯⟩))
⊢ ∃ (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]
have 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]
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₀ : ((↑(↑(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
⊢ f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
    peval (polyOfInterest p n) ![fun (i : ℕ) ↦ x.coeff i, fun (i : ℕ) ↦ y.coeff i]
have 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, sorry⟩ : 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: dsimp [f, peval]
-- 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
⊢ (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)
have 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, sorry⟩ : 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: rw [← hf₀]
-- 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
⊢ (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 × ℕ))))
have 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, sorry⟩)
  (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