-- 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
i : Fin 2
m : ℕ
ha : (i, m) ∈ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
h :
  ∀ (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)
h₁ :
  ∀ (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)
⊢ 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)

Tactic:
fin_cases i