-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : (i : (a : K) → L) y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : (i : (a : K) → L) y2 = x2 ^ p ^ n2
rw :
  HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
rw₁ :
  HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n2 + n1)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
rw₂ :
  HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M)
          ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M)
              (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
            M) :
        M) =
    HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
⊢ HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M)
          ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M)
              ((iterateFrobeniusEquiv M p n2 : (a : M) → M) ((j : (a : K) → M) y1 : M) : M) :
            M) :
        M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
have rw₃ : HMul.hMul (α := M) (β := M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M)
            ((iterateFrobeniusEquiv M p n1 : (a : M) → M) ((j : (a : K) → M) y2 : M) : M) :
          M) :
      M) =
  HMul.hMul (α := M) (β := M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
Tactic: rw [RingEquiv.symm_apply_apply, add_comm n1, iterateFrobeniusEquiv_symm_add_apply,
      ← iterateFrobeniusEquiv_def, RingEquiv.symm_apply_apply]