-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
idx : Type u_1
inst : CommRing R
inst_1 : 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 : (a : MvPolynomial ℕ ℤ) → R) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg :
  ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R),
    (g x).coeff = fun (n : ℕ) ↦ (aeval x.coeff : (a : MvPolynomial ℕ ℤ) → R) (ψ 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_1 : Type u_2
inst_2 : CommRing R_1
x y : 𝕎 R_1
n_1 : ℕ
i : Fin 2
n : ℕ
h₁ :
  Eq.{u_2 + 1} (α := R_1)
    (![fun (n : ℕ) ↦ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
          fun (n : ℕ) ↦ ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
        ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, n).2 :
      R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
        (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k), fun (k : ℕ) ↦
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, n).2) :
      R_1)
h₂ :
  Eq.{u_2 + 1} (α := R_1)
    (![fun (n : ℕ) ↦ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
          fun (n : ℕ) ↦ ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
        ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, n).2 :
      R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
        (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k), fun (k : ℕ) ↦
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), n).1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, n).2) :
      R_1)
⊢ Eq.{u_2 + 1} (α := R_1)
    (![fun (n : ℕ) ↦ ((aeval (R := ℤ) x.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (φ n),
          fun (n : ℕ) ↦ ((aeval (R := ℤ) y.coeff : MvPolynomial ℕ ℤ →ₐ[ℤ] R_1) : (a : MvPolynomial ℕ ℤ) → R_1) (ψ n)]
        (i, n).1 (i, n).2 :
      R_1)
    (((aeval.{0, u_2, 0} (R := ℤ) (S₁ := R_1) fun (a : Fin 2 × ℕ) ↦ ![x.coeff, y.coeff] a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] R_1) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → R_1)
        (![fun (k : ℕ) ↦ (rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (φ k), fun (k : ℕ) ↦
            (rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → MvPolynomial (Fin 2 × ℕ) ℤ) (ψ k)]
          (i, n).1 (i, n).2) :
      R_1)

Tactic:
fin_cases i