-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun (n : ℕ) ↦ peval (ψ n) ![x.coeff, y.coeff]
R : Type u
_Rcr : CommRing R
x_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
h₁ :
  Eq (α := ULift.{u, 0} ℤ)
    ((eval₂Hom
            (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
              (RingHom.comp (MvPolynomial.eval x) C))
            fun (i : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
              ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (φ i) : ℤ) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
⊢ Eq (α := ULift.{u, 0} ℤ)
    ((eval₂Hom
            (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
              (RingHom.comp (MvPolynomial.eval x) C))
            fun (i : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
              ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (φ i) : ℤ) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom
            (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
              (RingHom.comp (MvPolynomial.eval x) C))
            fun (i : ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
              ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (ψ i) : ℤ) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
have h₂ : Eq (α := ULift.{u, 0} ℤ)
  ((eval₂Hom
          (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ)
            (RingHom.comp (MvPolynomial.eval x) C))
          fun (i : ℕ) ↦
          ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ)
            ((MvPolynomial.eval x : (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ℤ) (ψ i) : ℤ) :
        (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
      (wittPolynomial p ℤ k) :
    ULift.{u, 0} ℤ)
  ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
          (coeff
            (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
              (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
        (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
      (wittPolynomial p ℤ k) :
    ULift.{u, 0} ℤ)
Tactic: convert! h using 1