Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case «0»
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] ((fun i ↦ i) ⟨0, ⋯⟩, n).1
      ((fun i ↦ i) ⟨0, ⋯⟩, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] ((fun i ↦ i) ⟨0, ⋯⟩, n).1
        ((fun i ↦ i) ⟨0, ⋯⟩, n).2)

pp: case «1»
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] ((fun i ↦ i) ⟨1, ⋯⟩, n).1
      ((fun i ↦ i) ⟨1, ⋯⟩, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] ((fun i ↦ i) ⟨1, ⋯⟩, n).1
        ((fun i ↦ i) ⟨1, ⋯⟩, n).2)

Tactic:
<;>

Goal state after:
case «0»
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] ((fun i ↦ i) ⟨0, ⋯⟩, n).1
      ((fun i ↦ i) ⟨0, ⋯⟩, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] ((fun i ↦ i) ⟨0, ⋯⟩, n).1
        ((fun i ↦ i) ⟨0, ⋯⟩, n).2)

case «1»
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] ((fun i ↦ i) ⟨1, ⋯⟩, n).1
      ((fun i ↦ i) ⟨1, ⋯⟩, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] ((fun i ↦ i) ⟨1, ⋯⟩, n).1
        ((fun i ↦ i) ⟨1, ⋯⟩, n).2)