-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem nth_mul_coeff' (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)

Proof state:
case h.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha =>
        Function.uncurry ![x, y]
          (let S := fun a => a.2 = n ∨ a.2 < n;
          let_fun ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
⊢ (fun a => ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑a).1 ⟨(↑a).2, ⋯⟩) =
    Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i] ∘ Subtype.val

Tactic:
ext a

Result:
case h.e_a.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha =>
        Function.uncurry ![x, y]
          (let S := fun a => a.2 = n ∨ a.2 < n;
          let_fun ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
a : ↑(Membership.mem (univ.val ×ˢ Multiset.range (n + 1)))
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑a).1 ⟨(↑a).2, ⋯⟩ =
    (Function.uncurry ![fun i => x.coeff i, fun i => y.coeff i] ∘ Subtype.val) a

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
⊢ ∃ f,
    ∀ (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 k (polyOfInterest_vars p n)

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
⊢ ∃ f,
    ∀ (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]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
⊢ ↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k

Tactic:
rintro ⟨a, ha⟩

Result:
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ Membership.mem (univ ×ˢ range (n + 1)).val
⊢ k

Proof state:
case h.e'_4
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ Membership.mem (univ.val.product (n ::ₘ Multiset.range n))
S : Set (Fin 2 × ℕ) := fun a => a.2 = n ∨ a.2 < n
⊢ S = Membership.mem (univ.val.product (n ::ₘ Multiset.range n))

Tactic:
dsimp [S]

Result:
case h.e'_4
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ Membership.mem (univ.val.product (n ::ₘ Multiset.range n))
S : Set (Fin 2 × ℕ) := fun a => a.2 = n ∨ a.2 < n
⊢ (fun a => a.2 = n ∨ a.2 < n) = Membership.mem (univ.val.product (n ::ₘ Multiset.range n))

Proof state:
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ Membership.mem (univ.val.product (n ::ₘ Multiset.range n))
S : Set (Fin 2 × ℕ) := fun a => a.2 = n ∨ a.2 < n
ha' : a ∈ S
⊢ a.2 < n + 1

Tactic:
obtain ⟨ha, ha⟩ := ha' <;> omega

Result:
no goals

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha =>
        Function.uncurry ![x, y]
          (let S := fun a => a.2 = n ∨ a.2 < n;
          let_fun 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]

Tactic:
intro x y

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y =>
    f₀ fun a =>
      Subtype.casesOn a fun a ha =>
        Function.uncurry ![x, y]
          (let S := fun a => a.2 = n ∨ a.2 < n;
          let_fun 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]

Proof state:
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ Membership.mem (univ.val.product (n ::ₘ Multiset.range n))
S : Set (Fin 2 × ℕ) := fun a => a.2 = n ∨ a.2 < n
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)

Tactic:
have ha' : a ∈ S := by
  convert ha
  dsimp [S]
  congr!
  simp

Result:
case mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑(Membership.mem (univ ×ˢ range (n + 1)).val) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
this : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ Membership.mem (univ.val.product (n ::ₘ Multiset.range n))
S : Set (Fin 2 × ℕ) := fun a => a.2 = n ∨ a.2 < n
ha' : a ∈ S
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)