K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).fst + y.fst, (↑(frobenius K p)^[y.fst]) (n, x).snd + (↑(frobenius K p)^[(n, x).fst]) y.snd)
    (Nat.succ (n + y.fst), ↑(frobenius K p) ((↑(frobenius K p)^[y.fst]) x + (↑(frobenius K p)^[n]) y.snd))
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).fst + y.fst, (↑(frobenius K p)^[y.fst]) (n, x).snd + (↑(frobenius K p)^[(n, x).fst]) y.snd)
    ((n + 1, ↑(frobenius K p) x).fst + y.fst,
      (↑(frobenius K p)^[y.fst]) (n + 1, ↑(frobenius K p) x).snd +
        (↑(frobenius K p)^[(n + 1, ↑(frobenius K p) x).fst]) y.snd)
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_add,
  Nat.succ_add]
no goals
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).fst + y.fst, (↑(frobenius K p)^[y.fst]) (n, x).snd + (↑(frobenius K p)^[(n, x).fst]) y.snd)
    (Nat.succ (n + y.fst), ↑(frobenius K p) ((↑(frobenius K p)^[y.fst]) x + (↑(frobenius K p)^[n]) y.snd))
apply R.intro