-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  Eq (α := MvPowerSeries σ R)
    (↑((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))) :
      MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
        MvPowerSeries σ R))
h :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
h₁ :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
h₂ :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (HPow.hPow (α := MvPowerSeries σ R)
          (↑((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) p) :
      MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
have h₃ : Eq (α := MvPolynomial σ R)
  ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
    MvPolynomial σ R)
  ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      (↑(HPow.hPow (α := MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f : MvPolynomial σ R) p) :
        MvPowerSeries σ R) :
    MvPolynomial σ R)
Tactic: rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]