-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (i : (a : K) → L) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 =
    x ^ p ^ n'
h_1 :
  Membership.mem (γ := Ideal K) (RingHom.ker i)
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n')
m : ℕ
h :
  ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n') ^
      p ^ m =
    0
rw :
  Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (a : M) → M)
        ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
          M) :
      M)
    ((iterateFrobeniusEquiv M p (m + (n + n')) : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
rw₁ :
  Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (a : M) → M)
        ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
          M) :
      M)
    ((iterateFrobeniusEquiv M p (m + (n' + n)) : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
rw₂ :
  Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (a : M) → M)
        ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
          M) :
      M)
    ((iterateFrobeniusEquiv M p (m + n' + n) : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
rw₃ :
  Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (a : M) → M)
        ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
          M) :
      M)
    ((iterateFrobeniusEquiv M p (m + n') : (a : M) → M)
        ((iterateFrobeniusEquiv M p n : (a : M) → M)
            ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
          M) :
      M)
rw₄ :
  Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (a : M) → M)
        ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
          M) :
      M)
    ((iterateFrobeniusEquiv M p (m + n') : (a : M) → M) ((j : (a : K) → M) y : M) : M)
rw₅ :
  HPow.hPow (α := M)
      ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 : M)
      (p ^ (m + n)) =
    (iterateFrobeniusEquiv M p (m + n') : (a : M) → M) ((j : (a : K) → M) y : M)
⊢ Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (a : M) → M)
        ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
          M) :
      M)
    ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
have rw₆ : HPow.hPow (α := M)
    ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) sorry).2 : M)
    (p ^ (m + n)) =
  HPow.hPow (α := M) ((j : (a : K) → M) y : M) (p ^ (m + n'))
Tactic: rw [add_assoc, add_comm n n', ← add_assoc,
    iterateFrobeniusEquiv_add_apply (m := m + n'), RingEquiv.apply_symm_apply,
    iterateFrobeniusEquiv_def, iterateFrobeniusEquiv_def,
    ← sub_eq_zero, ← map_pow, ← map_pow, ← map_sub,
    add_comm m, add_comm m, pow_add, pow_mul, pow_add, pow_mul, ← sub_pow_expChar_pow, h, map_zero]