-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : K →+* L
x_1 : PerfectClosure K p
n : ℕ
x : K
y_1 : PerfectClosure K p
m : ℕ
y : K
this :
  ∀ (n : ℕ),
    LeftInverse (α := L) (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] (⇑(frobenius L p) : (a : L) → L)^[n]
mk :
  HMul.hMul (α := L) (β := L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m]
            ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x))) :
        L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HMul.hMul (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
mk₁ :
  HMul.hMul (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HMul.hMul (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
mk₂ :
  HMul.hMul (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m + n]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HMul.hMul (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
⊢ HMul.hMul (α := L) (β := L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x)) :
        L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HMul.hMul (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
have mk₃ : HMul.hMul (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y))) :
      L) =
  HMul.hMul (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
Tactic: rw [iterate_add_apply, this _ _, add_comm, iterate_add_apply, this _ _]