-- 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
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ k
succ :
  Eq (α := MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
      MvPowerSeries σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
succ₁ :
  Eq (α := MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
      MvPowerSeries σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p * p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
succ₂ :
  Eq (α := MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
      MvPowerSeries σ R)
    ((map (iterateFrobenius R p (1 + k)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p * p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
succ₃ :
  Eq (α := MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
      MvPowerSeries σ R)
    ((map (RingHom.comp (iterateFrobenius R p 1) (iterateFrobenius R p k)) :
          (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p * p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
⊢ HPow.hPow (α := MvPowerSeries σ R)
      ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
        MvPowerSeries σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)
have succ₄ : Eq (α := MvPowerSeries σ R)
  ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f))) :
    MvPowerSeries σ R)
  ((map (iterateFrobenius R p 1) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p * p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
    MvPowerSeries σ R)
Tactic: simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]