Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case h.«0»
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
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 := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
m : ℕ
ha : ((fun i ↦ i) ⟨0, ⋯⟩, m) ∈ univ ×ˢ range (n + 1)
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑⟨((fun i ↦ i) ⟨0, ⋯⟩, m), ha⟩).1
      ⟨(↑⟨((fun i ↦ i) ⟨0, ⋯⟩, m), ha⟩).2, ⋯⟩ =
    (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val) ⟨((fun i ↦ i) ⟨0, ⋯⟩, m), ha⟩

pp: case h.«1»
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
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 := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
m : ℕ
ha : ((fun i ↦ i) ⟨1, ⋯⟩, m) ∈ univ ×ˢ range (n + 1)
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩).1
      ⟨(↑⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩).2, ⋯⟩ =
    (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val) ⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩

Tactic:
<;>

Goal state after:
case h.«0»
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
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 := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
m : ℕ
ha : ((fun i ↦ i) ⟨0, ⋯⟩, m) ∈ univ ×ˢ range (n + 1)
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑⟨((fun i ↦ i) ⟨0, ⋯⟩, m), ha⟩).1
      ⟨(↑⟨((fun i ↦ i) ⟨0, ⋯⟩, m), ha⟩).2, ⋯⟩ =
    (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val) ⟨((fun i ↦ i) ⟨0, ⋯⟩, m), ha⟩

case h.«1»
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
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 := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
m : ℕ
ha : ((fun i ↦ i) ⟨1, ⋯⟩, m) ∈ univ ×ˢ range (n + 1)
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩).1
      ⟨(↑⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩).2, ⋯⟩ =
    (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val) ⟨((fun i ↦ i) ⟨1, ⋯⟩, m), ha⟩