-- Module: Mathlib.RingTheory.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
succ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
succ₁ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
succ₂ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p (1 + k)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
succ₃ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (RingHom.comp (iterateFrobenius R p 1) (iterateFrobenius R p k)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
succ₄ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p 1) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)) :
      MvPolynomial σ R)
succ₅ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f))) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p 1) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)) :
      MvPolynomial σ R)
succ₆ :
  Eq (α := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)) :
      MvPolynomial σ R)
    ((map (iterateFrobenius R p 1) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p * p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)) :
      MvPolynomial σ R)
⊢ HPow.hPow (α := MvPolynomial σ R)
      ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
        MvPolynomial σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)

Tactic:
simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

Premises used: MvPolynomial.map_map, MvPolynomial.map_expand, MvPolynomial.map_frobenius_expand, add_comm, iterateFrobenius_add, MvPolynomial.expand_mul, iterateFrobenius_one, pow_succ'