[GOAL]
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)
[PROOFSTEP]
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_mul, Nat.succ_add]
[GOAL]
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))
[PROOFSTEP]
apply R.intro
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.fst + (n, y).fst, (↑(frobenius K p))^[(n, y).fst] x.snd * (↑(frobenius K p))^[x.fst] (n, y).snd)
    (x.fst + (n + 1, ↑(frobenius K p) y).fst,
      (↑(frobenius K p))^[(n + 1, ↑(frobenius K p) y).fst] x.snd *
        (↑(frobenius K p))^[x.fst] (n + 1, ↑(frobenius K p) y).snd)
[PROOFSTEP]
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_mul]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.fst + (n, y).fst, (↑(frobenius K p))^[(n, y).fst] x.snd * (↑(frobenius K p))^[x.fst] (n, y).snd)
    (x.fst + (n + 1, ↑(frobenius K p) y).fst,
      ↑(frobenius K p) ((↑(frobenius K p))^[n] x.snd * (↑(frobenius K p))^[x.fst] y))
[PROOFSTEP]
apply R.intro
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Mul (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ Quot.mk (R K p) (m, x) * Quot.mk (R K p) (n, y) * Quot.mk (R K p) (s, z) =
    Quot.mk (R K p) (m, x) * (Quot.mk (R K p) (n, y) * Quot.mk (R K p) (s, z))
[PROOFSTEP]
simp only [quot_mk_eq_mk, mk_mul_mk]
  -- Porting note: added this line
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Mul (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ mk K p
      (m + n + s,
        (↑(frobenius K p))^[s] ((↑(frobenius K p))^[n] x * (↑(frobenius K p))^[m] y) * (↑(frobenius K p))^[m + n] z) =
    mk K p
      (m + (n + s),
        (↑(frobenius K p))^[n + s] x * (↑(frobenius K p))^[m] ((↑(frobenius K p))^[s] y * (↑(frobenius K p))^[n] z))
[PROOFSTEP]
apply congr_arg (Quot.mk _)
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Mul (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (m + n + s,
      (↑(frobenius K p))^[s] ((↑(frobenius K p))^[n] x * (↑(frobenius K p))^[m] y) * (↑(frobenius K p))^[m + n] z) =
    (m + (n + s),
      (↑(frobenius K p))^[n + s] x * (↑(frobenius K p))^[m] ((↑(frobenius K p))^[s] y * (↑(frobenius K p))^[n] z))
[PROOFSTEP]
simp only [add_assoc, mul_assoc, iterate_map_mul, ← iterate_add_apply, add_comm, add_left_comm]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Mul (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ ((0, 1).fst + (n, x).fst, (↑(frobenius K p))^[(n, x).fst] (0, 1).snd * (↑(frobenius K p))^[(0, 1).fst] (n, x).snd) =
    (n, x)
[PROOFSTEP]
simp only [RingHom.iterate_map_one, iterate_zero_apply, one_mul, zero_add]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Mul (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ ((n, x).fst + (0, 1).fst, (↑(frobenius K p))^[(0, 1).fst] (n, x).snd * (↑(frobenius K p))^[(n, x).fst] (0, 1).snd) =
    (n, x)
[PROOFSTEP]
simp only [RingHom.iterate_map_one, iterate_zero_apply, mul_one, add_zero]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Mul (PerfectClosure K p) := inferInstance
e f : PerfectClosure K p
x✝¹ : ℕ × K
m : ℕ
x : K
x✝ : ℕ × K
n : ℕ
y : K
⊢ ((m, x).fst + (n, y).fst, (↑(frobenius K p))^[(n, y).fst] (m, x).snd * (↑(frobenius K p))^[(m, x).fst] (n, y).snd) =
    ((n, y).fst + (m, x).fst, (↑(frobenius K p))^[(m, x).fst] (n, y).snd * (↑(frobenius K p))^[(n, y).fst] (m, x).snd)
[PROOFSTEP]
simp only [add_comm, mul_comm]
[GOAL]
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)
[PROOFSTEP]
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_add, Nat.succ_add]
[GOAL]
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))
[PROOFSTEP]
apply R.intro
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.fst + (n, y).fst, (↑(frobenius K p))^[(n, y).fst] x.snd + (↑(frobenius K p))^[x.fst] (n, y).snd)
    (x.fst + (n + 1, ↑(frobenius K p) y).fst,
      (↑(frobenius K p))^[(n + 1, ↑(frobenius K p) y).fst] x.snd +
        (↑(frobenius K p))^[x.fst] (n + 1, ↑(frobenius K p) y).snd)
[PROOFSTEP]
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_add]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.fst + (n, y).fst, (↑(frobenius K p))^[(n, y).fst] x.snd + (↑(frobenius K p))^[x.fst] (n, y).snd)
    (x.fst + (n + 1, ↑(frobenius K p) y).fst,
      ↑(frobenius K p) ((↑(frobenius K p))^[n] x.snd + (↑(frobenius K p))^[x.fst] y))
[PROOFSTEP]
apply R.intro
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p ((n, x).fst, -(n, x).snd) ((n + 1, ↑(frobenius K p) x).fst, -(n + 1, ↑(frobenius K p) x).snd)
[PROOFSTEP]
rw [← frobenius_neg]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p ((n, x).fst, -(n, x).snd) ((n + 1, ↑(frobenius K p) x).fst, ↑(frobenius K p) (-x))
[PROOFSTEP]
apply R.intro
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
⊢ mk K p (n, 0) = 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ mk K p (Nat.zero, 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (Nat.succ n, 0) = 0
[PROOFSTEP]
rw [← ih]
[GOAL]
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (Nat.succ n, 0) = mk K p (n, 0)
[PROOFSTEP]
symm
[GOAL]
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n, 0) = mk K p (Nat.succ n, 0)
[PROOFSTEP]
apply Quot.sound
[GOAL]
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ R K p (n, 0) (Nat.succ n, 0)
[PROOFSTEP]
have := R.intro (p := p) n (0 : K)
[GOAL]
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
this : R K p (n, 0) (n + 1, ↑(frobenius K p) 0)
⊢ R K p (n, 0) (Nat.succ n, 0)
[PROOFSTEP]
rwa [frobenius_zero K p] at this 
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m n : ℕ
x y : K
H : (↑(frobenius K p))^[m] x = y
⊢ mk K p (n, x) = mk K p (m + n, y)
[PROOFSTEP]
subst H
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m n : ℕ
x : K
⊢ mk K p (n, x) = mk K p (m + n, (↑(frobenius K p))^[m] x)
[PROOFSTEP]
induction' m with m ih
[GOAL]
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ mk K p (n, x) = mk K p (Nat.zero + n, (↑(frobenius K p))^[Nat.zero] x)
[PROOFSTEP]
simp only [Nat.zero_eq, zero_add, iterate_zero_apply]
[GOAL]
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (↑(frobenius K p))^[m] x)
⊢ mk K p (n, x) = mk K p (Nat.succ m + n, (↑(frobenius K p))^[Nat.succ m] x)
[PROOFSTEP]
rw [ih, Nat.succ_add, iterate_succ']
[GOAL]
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (↑(frobenius K p))^[m] x)
⊢ mk K p (m + n, (↑(frobenius K p))^[m] x) = mk K p (Nat.succ (m + n), (↑(frobenius K p) ∘ (↑(frobenius K p))^[m]) x)
[PROOFSTEP]
apply Quot.sound
[GOAL]
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (↑(frobenius K p))^[m] x)
⊢ R K p (m + n, (↑(frobenius K p))^[m] x) (Nat.succ (m + n), (↑(frobenius K p) ∘ (↑(frobenius K p))^[m]) x)
[PROOFSTEP]
apply R.intro
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝¹ : Add (PerfectClosure K p) := inferInstance
src✝ : Neg (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ Quot.mk (R K p) (m, x) + Quot.mk (R K p) (n, y) + Quot.mk (R K p) (s, z) =
    Quot.mk (R K p) (m, x) + (Quot.mk (R K p) (n, y) + Quot.mk (R K p) (s, z))
[PROOFSTEP]
simp only [quot_mk_eq_mk, mk_add_mk]
  -- Porting note: added this line
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝¹ : Add (PerfectClosure K p) := inferInstance
src✝ : Neg (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ mk K p
      (m + n + s,
        (↑(frobenius K p))^[s] ((↑(frobenius K p))^[n] x + (↑(frobenius K p))^[m] y) + (↑(frobenius K p))^[m + n] z) =
    mk K p
      (m + (n + s),
        (↑(frobenius K p))^[n + s] x + (↑(frobenius K p))^[m] ((↑(frobenius K p))^[s] y + (↑(frobenius K p))^[n] z))
[PROOFSTEP]
apply congr_arg (Quot.mk _)
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝¹ : Add (PerfectClosure K p) := inferInstance
src✝ : Neg (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (m + n + s,
      (↑(frobenius K p))^[s] ((↑(frobenius K p))^[n] x + (↑(frobenius K p))^[m] y) + (↑(frobenius K p))^[m + n] z) =
    (m + (n + s),
      (↑(frobenius K p))^[n + s] x + (↑(frobenius K p))^[m] ((↑(frobenius K p))^[s] y + (↑(frobenius K p))^[n] z))
[PROOFSTEP]
simp only [iterate_map_add, ← iterate_add_apply, add_assoc, add_comm s _]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝¹ : Add (PerfectClosure K p) := inferInstance
src✝ : Neg (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ ((0, 0).fst + (n, x).fst, (↑(frobenius K p))^[(n, x).fst] (0, 0).snd + (↑(frobenius K p))^[(0, 0).fst] (n, x).snd) =
    (n, x)
[PROOFSTEP]
simp only [RingHom.iterate_map_zero, iterate_zero_apply, zero_add]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝¹ : Add (PerfectClosure K p) := inferInstance
src✝ : Neg (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ ((n, x).fst + (0, 0).fst, (↑(frobenius K p))^[(0, 0).fst] (n, x).snd + (↑(frobenius K p))^[(n, x).fst] (0, 0).snd) =
    (n, x)
[PROOFSTEP]
simp only [RingHom.iterate_map_zero, iterate_zero_apply, add_zero]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝¹ : Add (PerfectClosure K p) := inferInstance
src✝ : Neg (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ -Quot.mk (R K p) (n, x) + Quot.mk (R K p) (n, x) = 0
[PROOFSTEP]
simp only [quot_mk_eq_mk, neg_mk, mk_add_mk, RingHom.iterate_map_neg, add_left_neg, mk_zero]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝¹ : Add (PerfectClosure K p) := inferInstance
src✝ : Neg (PerfectClosure K p) := inferInstance
e f : PerfectClosure K p
x✝¹ : ℕ × K
m : ℕ
x : K
x✝ : ℕ × K
n : ℕ
y : K
⊢ ((m, x).fst + (n, y).fst, (↑(frobenius K p))^[(n, y).fst] (m, x).snd + (↑(frobenius K p))^[(m, x).fst] (n, y).snd) =
    ((n, y).fst + (m, x).fst, (↑(frobenius K p))^[(m, x).fst] (n, y).snd + (↑(frobenius K p))^[(n, y).fst] (m, x).snd)
[PROOFSTEP]
simp only [add_comm]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ Quot.mk (R K p) (m, x) * (Quot.mk (R K p) (n, y) + Quot.mk (R K p) (s, z)) =
    Quot.mk (R K p) (m, x) * Quot.mk (R K p) (n, y) + Quot.mk (R K p) (m, x) * Quot.mk (R K p) (s, z)
[PROOFSTEP]
simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk]
  -- Porting note: added this line
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ mk K p
      (m + (n + s),
        (↑(frobenius K p))^[n + s] x * (↑(frobenius K p))^[m] ((↑(frobenius K p))^[s] y + (↑(frobenius K p))^[n] z)) =
    mk K p
      (m + n + (m + s),
        (↑(frobenius K p))^[m + s] ((↑(frobenius K p))^[n] x * (↑(frobenius K p))^[m] y) +
          (↑(frobenius K p))^[m + n] ((↑(frobenius K p))^[s] x * (↑(frobenius K p))^[m] z))
[PROOFSTEP]
simp only [add_assoc, add_comm, add_left_comm]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ mk K p
      (m + (n + s),
        (↑(frobenius K p))^[n + s] x * (↑(frobenius K p))^[m] ((↑(frobenius K p))^[n] z + (↑(frobenius K p))^[s] y)) =
    mk K p
      (m + (m + (n + s)),
        (↑(frobenius K p))^[m + n] ((↑(frobenius K p))^[s] x * (↑(frobenius K p))^[m] z) +
          (↑(frobenius K p))^[m + s] ((↑(frobenius K p))^[n] x * (↑(frobenius K p))^[m] y))
[PROOFSTEP]
apply R.sound
[GOAL]
case H
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (↑(frobenius K p))^[m]
      ((↑(frobenius K p))^[n + s] x * (↑(frobenius K p))^[m] ((↑(frobenius K p))^[n] z + (↑(frobenius K p))^[s] y)) =
    (↑(frobenius K p))^[m + n] ((↑(frobenius K p))^[s] x * (↑(frobenius K p))^[m] z) +
      (↑(frobenius K p))^[m + s] ((↑(frobenius K p))^[n] x * (↑(frobenius K p))^[m] y)
[PROOFSTEP]
simp only [iterate_map_mul, iterate_map_add, ← iterate_add_apply, mul_add, add_comm, add_left_comm]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (Quot.mk (R K p) (m, x) + Quot.mk (R K p) (n, y)) * Quot.mk (R K p) (s, z) =
    Quot.mk (R K p) (m, x) * Quot.mk (R K p) (s, z) + Quot.mk (R K p) (n, y) * Quot.mk (R K p) (s, z)
[PROOFSTEP]
simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk]
  -- Porting note: added this line
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ mk K p
      (m + n + s,
        (↑(frobenius K p))^[s] ((↑(frobenius K p))^[n] x + (↑(frobenius K p))^[m] y) * (↑(frobenius K p))^[m + n] z) =
    mk K p
      (m + s + (n + s),
        (↑(frobenius K p))^[n + s] ((↑(frobenius K p))^[s] x * (↑(frobenius K p))^[m] z) +
          (↑(frobenius K p))^[m + s] ((↑(frobenius K p))^[s] y * (↑(frobenius K p))^[n] z))
[PROOFSTEP]
simp only [add_assoc, add_comm _ s, add_left_comm _ s]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ mk K p
      (s + (m + n),
        (↑(frobenius K p))^[s] ((↑(frobenius K p))^[n] x + (↑(frobenius K p))^[m] y) * (↑(frobenius K p))^[m + n] z) =
    mk K p
      (s + (s + (m + n)),
        (↑(frobenius K p))^[s + n] ((↑(frobenius K p))^[s] x * (↑(frobenius K p))^[m] z) +
          (↑(frobenius K p))^[s + m] ((↑(frobenius K p))^[s] y * (↑(frobenius K p))^[n] z))
[PROOFSTEP]
apply R.sound
[GOAL]
case H
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (↑(frobenius K p))^[s]
      ((↑(frobenius K p))^[s] ((↑(frobenius K p))^[n] x + (↑(frobenius K p))^[m] y) * (↑(frobenius K p))^[m + n] z) =
    (↑(frobenius K p))^[s + n] ((↑(frobenius K p))^[s] x * (↑(frobenius K p))^[m] z) +
      (↑(frobenius K p))^[s + m] ((↑(frobenius K p))^[s] y * (↑(frobenius K p))^[n] z)
[PROOFSTEP]
simp only [iterate_map_mul, iterate_map_add, ← iterate_add_apply, add_mul, add_comm, add_left_comm]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
a : PerfectClosure K p
⊢ 0 * a = 0
[PROOFSTEP]
refine Quot.inductionOn a fun ⟨m, x⟩ => ?_
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ 0 * Quot.mk (R K p) (m, x) = 0
[PROOFSTEP]
rw [zero_def, quot_mk_eq_mk, mk_mul_mk]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p
      ((0, 0).fst + (m, x).fst,
        (↑(frobenius K p))^[(m, x).fst] (0, 0).snd * (↑(frobenius K p))^[(0, 0).fst] (m, x).snd) =
    mk K p (0, 0)
[PROOFSTEP]
simp only [zero_add, iterate_zero, id_eq, RingHom.iterate_map_zero, zero_mul, mk_zero]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
a : PerfectClosure K p
⊢ a * 0 = 0
[PROOFSTEP]
refine Quot.inductionOn a fun ⟨m, x⟩ => ?_
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ Quot.mk (R K p) (m, x) * 0 = 0
[PROOFSTEP]
rw [zero_def, quot_mk_eq_mk, mk_mul_mk]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝² : AddCommGroup (PerfectClosure K p) := addCommGroup K p
src✝¹ : AddMonoidWithOne (PerfectClosure K p) := AddMonoidWithOne.unary
src✝ : CommMonoid (PerfectClosure K p) := inferInstance
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p
      ((m, x).fst + (0, 0).fst,
        (↑(frobenius K p))^[(0, 0).fst] (m, x).snd * (↑(frobenius K p))^[(m, x).fst] (0, 0).snd) =
    mk K p (0, 0)
[PROOFSTEP]
simp only [zero_add, iterate_zero, id_eq, RingHom.iterate_map_zero, mul_zero, mk_zero]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
⊢ mk K p x = mk K p y ↔ ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
⊢ mk K p x = mk K p y → ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
[PROOFSTEP]
intro H
[GOAL]
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
H : mk K p x = mk K p y
⊢ ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
[PROOFSTEP]
replace H := Quot.exact _ H
[GOAL]
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
H : EqvGen (R K p) x y
⊢ ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
[PROOFSTEP]
induction H
[GOAL]
case mp.rel
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ y✝ : ℕ × K
a✝ : R K p x✝ y✝
⊢ ∃ z, (↑(frobenius K p))^[y✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] y✝.snd
case mp.refl
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ : ℕ × K
⊢ ∃ z, (↑(frobenius K p))^[x✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] x✝.snd
case mp.symm
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ y✝ : ℕ × K
a✝ : EqvGen (R K p) x✝ y✝
a_ih✝ : ∃ z, (↑(frobenius K p))^[y✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] y✝.snd
⊢ ∃ z, (↑(frobenius K p))^[x✝.fst + z] y✝.snd = (↑(frobenius K p))^[y✝.fst + z] x✝.snd
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ y✝ z✝ : ℕ × K
a✝¹ : EqvGen (R K p) x✝ y✝
a✝ : EqvGen (R K p) y✝ z✝
a_ih✝¹ : ∃ z, (↑(frobenius K p))^[y✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] y✝.snd
a_ih✝ : ∃ z, (↑(frobenius K p))^[z✝.fst + z] y✝.snd = (↑(frobenius K p))^[y✝.fst + z] z✝.snd
⊢ ∃ z, (↑(frobenius K p))^[z✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] z✝.snd
[PROOFSTEP]
case rel x y H => cases' H with n x; exact ⟨0, rfl⟩
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y : ℕ × K
H : R K p x y
⊢ ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
[PROOFSTEP]
case rel x y H => cases' H with n x; exact ⟨0, rfl⟩
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y : ℕ × K
H : R K p x y
⊢ ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
[PROOFSTEP]
cases' H with n x
[GOAL]
case intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
n : ℕ
x : K
⊢ ∃ z,
    (↑(frobenius K p))^[(n + 1, ↑(frobenius K p) x).fst + z] (n, x).snd =
      (↑(frobenius K p))^[(n, x).fst + z] (n + 1, ↑(frobenius K p) x).snd
[PROOFSTEP]
exact ⟨0, rfl⟩
[GOAL]
case mp.refl
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ : ℕ × K
⊢ ∃ z, (↑(frobenius K p))^[x✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] x✝.snd
case mp.symm
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ y✝ : ℕ × K
a✝ : EqvGen (R K p) x✝ y✝
a_ih✝ : ∃ z, (↑(frobenius K p))^[y✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] y✝.snd
⊢ ∃ z, (↑(frobenius K p))^[x✝.fst + z] y✝.snd = (↑(frobenius K p))^[y✝.fst + z] x✝.snd
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ y✝ z✝ : ℕ × K
a✝¹ : EqvGen (R K p) x✝ y✝
a✝ : EqvGen (R K p) y✝ z✝
a_ih✝¹ : ∃ z, (↑(frobenius K p))^[y✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] y✝.snd
a_ih✝ : ∃ z, (↑(frobenius K p))^[z✝.fst + z] y✝.snd = (↑(frobenius K p))^[y✝.fst + z] z✝.snd
⊢ ∃ z, (↑(frobenius K p))^[z✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] z✝.snd
[PROOFSTEP]
case refl H => exact ⟨0, rfl⟩
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y H : ℕ × K
⊢ ∃ z, (↑(frobenius K p))^[H.fst + z] H.snd = (↑(frobenius K p))^[H.fst + z] H.snd
[PROOFSTEP]
case refl H => exact ⟨0, rfl⟩
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y H : ℕ × K
⊢ ∃ z, (↑(frobenius K p))^[H.fst + z] H.snd = (↑(frobenius K p))^[H.fst + z] H.snd
[PROOFSTEP]
exact ⟨0, rfl⟩
[GOAL]
case mp.symm
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ y✝ : ℕ × K
a✝ : EqvGen (R K p) x✝ y✝
a_ih✝ : ∃ z, (↑(frobenius K p))^[y✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] y✝.snd
⊢ ∃ z, (↑(frobenius K p))^[x✝.fst + z] y✝.snd = (↑(frobenius K p))^[y✝.fst + z] x✝.snd
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ y✝ z✝ : ℕ × K
a✝¹ : EqvGen (R K p) x✝ y✝
a✝ : EqvGen (R K p) y✝ z✝
a_ih✝¹ : ∃ z, (↑(frobenius K p))^[y✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] y✝.snd
a_ih✝ : ∃ z, (↑(frobenius K p))^[z✝.fst + z] y✝.snd = (↑(frobenius K p))^[y✝.fst + z] z✝.snd
⊢ ∃ z, (↑(frobenius K p))^[z✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] z✝.snd
[PROOFSTEP]
case symm x y H ih => cases' ih with w ih; exact ⟨w, ih.symm⟩
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y : ℕ × K
H : EqvGen (R K p) x y
ih : ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
⊢ ∃ z, (↑(frobenius K p))^[x.fst + z] y.snd = (↑(frobenius K p))^[y.fst + z] x.snd
[PROOFSTEP]
case symm x y H ih => cases' ih with w ih; exact ⟨w, ih.symm⟩
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y : ℕ × K
H : EqvGen (R K p) x y
ih : ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
⊢ ∃ z, (↑(frobenius K p))^[x.fst + z] y.snd = (↑(frobenius K p))^[y.fst + z] x.snd
[PROOFSTEP]
cases' ih with w ih
[GOAL]
case intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y : ℕ × K
H : EqvGen (R K p) x y
w : ℕ
ih : (↑(frobenius K p))^[y.fst + w] x.snd = (↑(frobenius K p))^[x.fst + w] y.snd
⊢ ∃ z, (↑(frobenius K p))^[x.fst + z] y.snd = (↑(frobenius K p))^[y.fst + z] x.snd
[PROOFSTEP]
exact ⟨w, ih.symm⟩
[GOAL]
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y x✝ y✝ z✝ : ℕ × K
a✝¹ : EqvGen (R K p) x✝ y✝
a✝ : EqvGen (R K p) y✝ z✝
a_ih✝¹ : ∃ z, (↑(frobenius K p))^[y✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] y✝.snd
a_ih✝ : ∃ z, (↑(frobenius K p))^[z✝.fst + z] y✝.snd = (↑(frobenius K p))^[y✝.fst + z] z✝.snd
⊢ ∃ z, (↑(frobenius K p))^[z✝.fst + z] x✝.snd = (↑(frobenius K p))^[x✝.fst + z] z✝.snd
[PROOFSTEP]
case trans x y z H1 H2 ih1 ih2 =>
  cases' ih1 with z1 ih1
  cases' ih2 with z2 ih2
  exists z2 + (y.1 + z1)
  rw [← add_assoc, iterate_add_apply, ih1]
  rw [← iterate_add_apply, add_comm, iterate_add_apply, ih2]
  rw [← iterate_add_apply]
  simp only [add_comm, add_left_comm]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : EqvGen (R K p) x y
H2 : EqvGen (R K p) y z
ih1 : ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
ih2 : ∃ z_1, (↑(frobenius K p))^[z.fst + z_1] y.snd = (↑(frobenius K p))^[y.fst + z_1] z.snd
⊢ ∃ z_1, (↑(frobenius K p))^[z.fst + z_1] x.snd = (↑(frobenius K p))^[x.fst + z_1] z.snd
[PROOFSTEP]
case trans x y z H1 H2 ih1 ih2 =>
  cases' ih1 with z1 ih1
  cases' ih2 with z2 ih2
  exists z2 + (y.1 + z1)
  rw [← add_assoc, iterate_add_apply, ih1]
  rw [← iterate_add_apply, add_comm, iterate_add_apply, ih2]
  rw [← iterate_add_apply]
  simp only [add_comm, add_left_comm]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : EqvGen (R K p) x y
H2 : EqvGen (R K p) y z
ih1 : ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
ih2 : ∃ z_1, (↑(frobenius K p))^[z.fst + z_1] y.snd = (↑(frobenius K p))^[y.fst + z_1] z.snd
⊢ ∃ z_1, (↑(frobenius K p))^[z.fst + z_1] x.snd = (↑(frobenius K p))^[x.fst + z_1] z.snd
[PROOFSTEP]
cases' ih1 with z1 ih1
[GOAL]
case intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : EqvGen (R K p) x y
H2 : EqvGen (R K p) y z
ih2 : ∃ z_1, (↑(frobenius K p))^[z.fst + z_1] y.snd = (↑(frobenius K p))^[y.fst + z_1] z.snd
z1 : ℕ
ih1 : (↑(frobenius K p))^[y.fst + z1] x.snd = (↑(frobenius K p))^[x.fst + z1] y.snd
⊢ ∃ z_1, (↑(frobenius K p))^[z.fst + z_1] x.snd = (↑(frobenius K p))^[x.fst + z_1] z.snd
[PROOFSTEP]
cases' ih2 with z2 ih2
[GOAL]
case intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : EqvGen (R K p) x y
H2 : EqvGen (R K p) y z
z1 : ℕ
ih1 : (↑(frobenius K p))^[y.fst + z1] x.snd = (↑(frobenius K p))^[x.fst + z1] y.snd
z2 : ℕ
ih2 : (↑(frobenius K p))^[z.fst + z2] y.snd = (↑(frobenius K p))^[y.fst + z2] z.snd
⊢ ∃ z_1, (↑(frobenius K p))^[z.fst + z_1] x.snd = (↑(frobenius K p))^[x.fst + z_1] z.snd
[PROOFSTEP]
exists z2 + (y.1 + z1)
[GOAL]
case intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : EqvGen (R K p) x y
H2 : EqvGen (R K p) y z
z1 : ℕ
ih1 : (↑(frobenius K p))^[y.fst + z1] x.snd = (↑(frobenius K p))^[x.fst + z1] y.snd
z2 : ℕ
ih2 : (↑(frobenius K p))^[z.fst + z2] y.snd = (↑(frobenius K p))^[y.fst + z2] z.snd
⊢ (↑(frobenius K p))^[z.fst + (z2 + (y.fst + z1))] x.snd = (↑(frobenius K p))^[x.fst + (z2 + (y.fst + z1))] z.snd
[PROOFSTEP]
rw [← add_assoc, iterate_add_apply, ih1]
[GOAL]
case intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : EqvGen (R K p) x y
H2 : EqvGen (R K p) y z
z1 : ℕ
ih1 : (↑(frobenius K p))^[y.fst + z1] x.snd = (↑(frobenius K p))^[x.fst + z1] y.snd
z2 : ℕ
ih2 : (↑(frobenius K p))^[z.fst + z2] y.snd = (↑(frobenius K p))^[y.fst + z2] z.snd
⊢ (↑(frobenius K p))^[z.fst + z2] ((↑(frobenius K p))^[x.fst + z1] y.snd) =
    (↑(frobenius K p))^[x.fst + (z2 + (y.fst + z1))] z.snd
[PROOFSTEP]
rw [← iterate_add_apply, add_comm, iterate_add_apply, ih2]
[GOAL]
case intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : EqvGen (R K p) x y
H2 : EqvGen (R K p) y z
z1 : ℕ
ih1 : (↑(frobenius K p))^[y.fst + z1] x.snd = (↑(frobenius K p))^[x.fst + z1] y.snd
z2 : ℕ
ih2 : (↑(frobenius K p))^[z.fst + z2] y.snd = (↑(frobenius K p))^[y.fst + z2] z.snd
⊢ (↑(frobenius K p))^[x.fst + z1] ((↑(frobenius K p))^[y.fst + z2] z.snd) =
    (↑(frobenius K p))^[x.fst + (z2 + (y.fst + z1))] z.snd
[PROOFSTEP]
rw [← iterate_add_apply]
[GOAL]
case intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : EqvGen (R K p) x y
H2 : EqvGen (R K p) y z
z1 : ℕ
ih1 : (↑(frobenius K p))^[y.fst + z1] x.snd = (↑(frobenius K p))^[x.fst + z1] y.snd
z2 : ℕ
ih2 : (↑(frobenius K p))^[z.fst + z2] y.snd = (↑(frobenius K p))^[y.fst + z2] z.snd
⊢ (↑(frobenius K p))^[x.fst + z1 + (y.fst + z2)] z.snd = (↑(frobenius K p))^[x.fst + (z2 + (y.fst + z1))] z.snd
[PROOFSTEP]
simp only [add_comm, add_left_comm]
[GOAL]
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
⊢ (∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd) → mk K p x = mk K p y
[PROOFSTEP]
intro H
[GOAL]
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
H : ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
⊢ mk K p x = mk K p y
[PROOFSTEP]
cases' x with m x
[GOAL]
case mpr.mk
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
y : ℕ × K
m : ℕ
x : K
H : ∃ z, (↑(frobenius K p))^[y.fst + z] (m, x).snd = (↑(frobenius K p))^[(m, x).fst + z] y.snd
⊢ mk K p (m, x) = mk K p y
[PROOFSTEP]
cases' y with n y
[GOAL]
case mpr.mk.mk
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
H : ∃ z, (↑(frobenius K p))^[(n, y).fst + z] (m, x).snd = (↑(frobenius K p))^[(m, x).fst + z] (n, y).snd
⊢ mk K p (m, x) = mk K p (n, y)
[PROOFSTEP]
cases' H with z H
[GOAL]
case mpr.mk.mk.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (↑(frobenius K p))^[(n, y).fst + z] (m, x).snd = (↑(frobenius K p))^[(m, x).fst + z] (n, y).snd
⊢ mk K p (m, x) = mk K p (n, y)
[PROOFSTEP]
dsimp only at H 
[GOAL]
case mpr.mk.mk.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (↑(frobenius K p))^[n + z] x = (↑(frobenius K p))^[m + z] y
⊢ mk K p (m, x) = mk K p (n, y)
[PROOFSTEP]
rw [R.sound K p (n + z) m x _ rfl, R.sound K p (m + z) n y _ rfl, H]
[GOAL]
case mpr.mk.mk.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (↑(frobenius K p))^[n + z] x = (↑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (↑(frobenius K p))^[m + z] y) = mk K p (m + z + n, (↑(frobenius K p))^[m + z] y)
[PROOFSTEP]
rw [add_assoc, add_comm, add_comm z]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n x : ℕ
⊢ ↑x = mk K p (n, ↑x)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
⊢ ↑x = mk K p (Nat.zero, ↑x)
[PROOFSTEP]
induction' x with x ih
[GOAL]
case zero.zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ ↑Nat.zero = mk K p (Nat.zero, ↑Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case zero.succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
ih : ↑x = mk K p (Nat.zero, ↑x)
⊢ ↑(Nat.succ x) = mk K p (Nat.zero, ↑(Nat.succ x))
[PROOFSTEP]
rw [Nat.cast_succ, Nat.cast_succ, ih]
[GOAL]
case zero.succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
ih : ↑x = mk K p (Nat.zero, ↑x)
⊢ mk K p (Nat.zero, ↑x) + 1 = mk K p (Nat.zero, ↑x + 1)
[PROOFSTEP]
rfl
[GOAL]
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ ↑x = mk K p (Nat.succ n, ↑x)
[PROOFSTEP]
rw [ih]
[GOAL]
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ mk K p (n, ↑x) = mk K p (Nat.succ n, ↑x)
[PROOFSTEP]
apply Quot.sound
[GOAL]
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (Nat.succ n, ↑x)
[PROOFSTEP]
suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by rwa [frobenius_nat_cast K p x] at this 
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
this : R K p (n, ↑x) (Nat.succ n, ↑(frobenius K p) ↑x)
⊢ R K p (n, ↑x) (Nat.succ n, ↑x)
[PROOFSTEP]
rwa [frobenius_nat_cast K p x] at this 
[GOAL]
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (Nat.succ n, ↑(frobenius K p) ↑x)
[PROOFSTEP]
apply R.intro
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℤ
⊢ ↑x = mk K p (0, ↑x)
[PROOFSTEP]
induction x
[GOAL]
case ofNat
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = mk K p (0, ↑(Int.ofNat a✝))
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, Int.cast_ofNat, Int.cast_negSucc, nat_cast K p 0]
[GOAL]
case negSucc
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) = mk K p (0, ↑(Int.negSucc a✝))
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, Int.cast_ofNat, Int.cast_negSucc, nat_cast K p 0]
[GOAL]
case negSucc
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a✝ : ℕ
⊢ -mk K p (0, ↑(a✝ + 1)) = mk K p (0, -↑(a✝ + 1))
[PROOFSTEP]
rfl
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
⊢ ↑x = ↑y ↔ ↑x = ↑y
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
⊢ ↑x = ↑y → ↑x = ↑y
[PROOFSTEP]
intro H
[GOAL]
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
⊢ ↑x = ↑y → ↑x = ↑y
[PROOFSTEP]
intro H
[GOAL]
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y
[PROOFSTEP]
rw [nat_cast K p 0, nat_cast K p 0, eq_iff'] at H 
[GOAL]
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ∃ z, (↑(frobenius K p))^[(0, ↑y).fst + z] (0, ↑x).snd = (↑(frobenius K p))^[(0, ↑x).fst + z] (0, ↑y).snd
⊢ ↑x = ↑y
[PROOFSTEP]
cases' H with z H
[GOAL]
case mp.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (↑(frobenius K p))^[(0, ↑y).fst + z] (0, ↑x).snd = (↑(frobenius K p))^[(0, ↑x).fst + z] (0, ↑y).snd
⊢ ↑x = ↑y
[PROOFSTEP]
simpa only [zero_add, iterate_fixed (frobenius_nat_cast K p _)] using H
[GOAL]
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y
[PROOFSTEP]
rw [nat_cast K p 0, nat_cast K p 0, H]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ CharP (PerfectClosure K p) p
[PROOFSTEP]
constructor
[GOAL]
case cast_eq_zero_iff'
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
[PROOFSTEP]
intro x
[GOAL]
case cast_eq_zero_iff'
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff K]
[GOAL]
case cast_eq_zero_iff'
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
⊢ ↑x = 0 ↔ ↑x = 0
[PROOFSTEP]
rw [← Nat.cast_zero, nat_cast_eq_iff, Nat.cast_zero]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ ↑(frobenius (PerfectClosure K p) p) (mk K p x) = mk K p (x.fst, x.snd ^ p)
[PROOFSTEP]
simp only [frobenius_def]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ mk K p x ^ p = mk K p (x.fst, x.snd ^ p)
[PROOFSTEP]
cases' x with n x
[GOAL]
case mk
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ mk K p (n, x) ^ p = mk K p ((n, x).fst, (n, x).snd ^ p)
[PROOFSTEP]
dsimp only
[GOAL]
case mk
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ mk K p (n, x) ^ p = mk K p (n, x ^ p)
[PROOFSTEP]
suffices ∀ p' : ℕ, mk K p (n, x) ^ p' = mk K p (n, x ^ p') by apply this
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
this : ∀ (p' : ℕ), mk K p (n, x) ^ p' = mk K p (n, x ^ p')
⊢ mk K p (n, x) ^ p = mk K p (n, x ^ p)
[PROOFSTEP]
apply this
[GOAL]
case mk
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ ∀ (p' : ℕ), mk K p (n, x) ^ p' = mk K p (n, x ^ p')
[PROOFSTEP]
intro p
[GOAL]
case mk
K : Type u
inst✝² : CommRing K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : CharP K p✝
n : ℕ
x : K
p : ℕ
⊢ mk K p✝ (n, x) ^ p = mk K p✝ (n, x ^ p)
[PROOFSTEP]
induction' p with p ih
[GOAL]
case mk.zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ mk K p (n, x) ^ Nat.zero = mk K p (n, x ^ Nat.zero)
case mk.succ
K : Type u
inst✝² : CommRing K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : CharP K p✝
n : ℕ
x : K
p : ℕ
ih : mk K p✝ (n, x) ^ p = mk K p✝ (n, x ^ p)
⊢ mk K p✝ (n, x) ^ Nat.succ p = mk K p✝ (n, x ^ Nat.succ p)
[PROOFSTEP]
case zero => apply R.sound; rw [(frobenius _ _).iterate_map_one, pow_zero]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ mk K p (n, x) ^ Nat.zero = mk K p (n, x ^ Nat.zero)
[PROOFSTEP]
case zero => apply R.sound; rw [(frobenius _ _).iterate_map_one, pow_zero]
[GOAL]
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ mk K p (n, x) ^ Nat.zero = mk K p (n, x ^ Nat.zero)
[PROOFSTEP]
apply R.sound
[GOAL]
case H
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (↑(frobenius K p))^[n] 1 = x ^ Nat.zero
[PROOFSTEP]
rw [(frobenius _ _).iterate_map_one, pow_zero]
[GOAL]
case mk.succ
K : Type u
inst✝² : CommRing K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : CharP K p✝
n : ℕ
x : K
p : ℕ
ih : mk K p✝ (n, x) ^ p = mk K p✝ (n, x ^ p)
⊢ mk K p✝ (n, x) ^ Nat.succ p = mk K p✝ (n, x ^ Nat.succ p)
[PROOFSTEP]
case succ =>
  rw [pow_succ, ih]
  symm
  apply R.sound
  simp only [pow_succ, iterate_map_mul]
[GOAL]
K : Type u
inst✝² : CommRing K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : CharP K p✝
n : ℕ
x : K
p : ℕ
ih : mk K p✝ (n, x) ^ p = mk K p✝ (n, x ^ p)
⊢ mk K p✝ (n, x) ^ Nat.succ p = mk K p✝ (n, x ^ Nat.succ p)
[PROOFSTEP]
case succ =>
  rw [pow_succ, ih]
  symm
  apply R.sound
  simp only [pow_succ, iterate_map_mul]
[GOAL]
K : Type u
inst✝² : CommRing K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : CharP K p✝
n : ℕ
x : K
p : ℕ
ih : mk K p✝ (n, x) ^ p = mk K p✝ (n, x ^ p)
⊢ mk K p✝ (n, x) ^ Nat.succ p = mk K p✝ (n, x ^ Nat.succ p)
[PROOFSTEP]
rw [pow_succ, ih]
[GOAL]
K : Type u
inst✝² : CommRing K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : CharP K p✝
n : ℕ
x : K
p : ℕ
ih : mk K p✝ (n, x) ^ p = mk K p✝ (n, x ^ p)
⊢ mk K p✝ (n, x) * mk K p✝ (n, x ^ p) = mk K p✝ (n, x ^ Nat.succ p)
[PROOFSTEP]
symm
[GOAL]
K : Type u
inst✝² : CommRing K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : CharP K p✝
n : ℕ
x : K
p : ℕ
ih : mk K p✝ (n, x) ^ p = mk K p✝ (n, x ^ p)
⊢ mk K p✝ (n, x ^ Nat.succ p) = mk K p✝ (n, x) * mk K p✝ (n, x ^ p)
[PROOFSTEP]
apply R.sound
[GOAL]
case H
K : Type u
inst✝² : CommRing K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : CharP K p✝
n : ℕ
x : K
p : ℕ
ih : mk K p✝ (n, x) ^ p = mk K p✝ (n, x ^ p)
⊢ (↑(frobenius K p✝))^[(n, x).fst] (x ^ Nat.succ p) =
    (↑(frobenius K p✝))^[(n, x ^ p).fst] (n, x).snd * (↑(frobenius K p✝))^[(n, x).fst] (n, x ^ p).snd
[PROOFSTEP]
simp only [pow_succ, iterate_map_mul]
[GOAL]
K : Type u
inst✝³ : CommRing K
inst✝² : IsReduced K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
x✝ : ∃ z, (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
z : ℕ
H : (↑(frobenius K p))^[y.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
⊢ (↑(frobenius K p))^[z] ((↑(frobenius K p))^[y.fst] x.snd) = (↑(frobenius K p))^[z] ((↑(frobenius K p))^[x.fst] y.snd)
[PROOFSTEP]
simpa only [add_comm, iterate_add] using H
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p ((n, x).fst, (n, x).snd⁻¹) ((n + 1, ↑(frobenius K p) x).fst, (n + 1, ↑(frobenius K p) x).snd⁻¹)
[PROOFSTEP]
simp only [frobenius_def]
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p (n, x⁻¹) (n + 1, (x ^ p)⁻¹)
[PROOFSTEP]
rw [← inv_pow]
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p (n, x⁻¹) (n + 1, x⁻¹ ^ p)
[PROOFSTEP]
apply R.intro
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Inv (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
⊢ mk K p (m, x) * (mk K p (m, x))⁻¹ = 1
[PROOFSTEP]
have := mt (eq_iff _ _ _ _).2 H
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Inv (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬(↑(frobenius K p))^[(0, 0).fst] (m, x).snd = (↑(frobenius K p))^[(m, x).fst] (0, 0).snd
⊢ mk K p (m, x) * (mk K p (m, x))⁻¹ = 1
[PROOFSTEP]
rw [mk_inv, mk_mul_mk]
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Inv (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬(↑(frobenius K p))^[(0, 0).fst] (m, x).snd = (↑(frobenius K p))^[(m, x).fst] (0, 0).snd
⊢ mk K p
      ((m, x).fst + ((m, x).fst, (m, x).snd⁻¹).fst,
        (↑(frobenius K p))^[((m, x).fst, (m, x).snd⁻¹).fst] (m, x).snd *
          (↑(frobenius K p))^[(m, x).fst] ((m, x).fst, (m, x).snd⁻¹).snd) =
    1
[PROOFSTEP]
refine (eq_iff K p _ _).2 ?_
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Inv (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬(↑(frobenius K p))^[(0, 0).fst] (m, x).snd = (↑(frobenius K p))^[(m, x).fst] (0, 0).snd
⊢ (↑(frobenius K p))^[(0, 1).fst]
      ((m, x).fst + ((m, x).fst, (m, x).snd⁻¹).fst,
          (↑(frobenius K p))^[((m, x).fst, (m, x).snd⁻¹).fst] (m, x).snd *
            (↑(frobenius K p))^[(m, x).fst] ((m, x).fst, (m, x).snd⁻¹).snd).snd =
    (↑(frobenius K
            p))^[((m, x).fst + ((m, x).fst, (m, x).snd⁻¹).fst,
            (↑(frobenius K p))^[((m, x).fst, (m, x).snd⁻¹).fst] (m, x).snd *
              (↑(frobenius K p))^[(m, x).fst] ((m, x).fst, (m, x).snd⁻¹).snd).fst]
      (0, 1).snd
[PROOFSTEP]
simp only [(frobenius _ _).iterate_map_one, (frobenius K p).iterate_map_zero, iterate_zero_apply, ← iterate_map_mul] at
  this ⊢
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Inv (PerfectClosure K p) := inferInstance
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬x = 0
⊢ (↑(frobenius K p))^[m] (x * x⁻¹) = 1
[PROOFSTEP]
rw [mul_inv_cancel this, (frobenius _ _).iterate_map_one]
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
src✝ : Inv (PerfectClosure K p) := inferInstance
⊢ ((0, 0).fst, (0, 0).snd⁻¹) = (0, 0)
[PROOFSTEP]
rw [inv_zero]
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ Bijective ↑(frobenius (PerfectClosure K p) p)
[PROOFSTEP]
let f : PerfectClosure K p → PerfectClosure K p := fun e ↦
  liftOn e (fun x => mk K p (x.1 + 1, x.2)) fun x y H =>
    match x, y, H with
    | _, _, R.intro n x => Quot.sound (R.intro _ _)
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun e =>
    liftOn e (fun x => mk K p (x.fst + 1, x.snd))
      (_ : ∀ (x y : ℕ × K), R K p x y → (fun x => mk K p (x.fst + 1, x.snd)) x = (fun x => mk K p (x.fst + 1, x.snd)) y)
⊢ Bijective ↑(frobenius (PerfectClosure K p) p)
[PROOFSTEP]
have hl : LeftInverse f (frobenius (PerfectClosure K p) p) := fun e ↦
  induction_on e fun ⟨n, x⟩ => by
    simp only [liftOn_mk, frobenius_mk]
    exact (Quot.sound <| R.intro _ _).symm
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun e =>
    liftOn e (fun x => mk K p (x.fst + 1, x.snd))
      (_ : ∀ (x y : ℕ × K), R K p x y → (fun x => mk K p (x.fst + 1, x.snd)) x = (fun x => mk K p (x.fst + 1, x.snd)) y)
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ f (↑(frobenius (PerfectClosure K p) p) (mk K p (n, x))) = mk K p (n, x)
[PROOFSTEP]
simp only [liftOn_mk, frobenius_mk]
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun e =>
    liftOn e (fun x => mk K p (x.fst + 1, x.snd))
      (_ : ∀ (x y : ℕ × K), R K p x y → (fun x => mk K p (x.fst + 1, x.snd)) x = (fun x => mk K p (x.fst + 1, x.snd)) y)
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ mk K p (n + 1, x ^ p) = mk K p (n, x)
[PROOFSTEP]
exact (Quot.sound <| R.intro _ _).symm
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun e =>
    liftOn e (fun x => mk K p (x.fst + 1, x.snd))
      (_ : ∀ (x y : ℕ × K), R K p x y → (fun x => mk K p (x.fst + 1, x.snd)) x = (fun x => mk K p (x.fst + 1, x.snd)) y)
hl : LeftInverse f ↑(frobenius (PerfectClosure K p) p)
⊢ Bijective ↑(frobenius (PerfectClosure K p) p)
[PROOFSTEP]
have hr : RightInverse f (frobenius (PerfectClosure K p) p) := fun e ↦
  induction_on e fun ⟨n, x⟩ => by
    simp only [liftOn_mk, frobenius_mk]
    exact (Quot.sound <| R.intro _ _).symm
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun e =>
    liftOn e (fun x => mk K p (x.fst + 1, x.snd))
      (_ : ∀ (x y : ℕ × K), R K p x y → (fun x => mk K p (x.fst + 1, x.snd)) x = (fun x => mk K p (x.fst + 1, x.snd)) y)
hl : LeftInverse f ↑(frobenius (PerfectClosure K p) p)
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ ↑(frobenius (PerfectClosure K p) p) (f (mk K p (n, x))) = mk K p (n, x)
[PROOFSTEP]
simp only [liftOn_mk, frobenius_mk]
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun e =>
    liftOn e (fun x => mk K p (x.fst + 1, x.snd))
      (_ : ∀ (x y : ℕ × K), R K p x y → (fun x => mk K p (x.fst + 1, x.snd)) x = (fun x => mk K p (x.fst + 1, x.snd)) y)
hl : LeftInverse f ↑(frobenius (PerfectClosure K p) p)
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ mk K p (n + 1, x ^ p) = mk K p (n, x)
[PROOFSTEP]
exact (Quot.sound <| R.intro _ _).symm
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun e =>
    liftOn e (fun x => mk K p (x.fst + 1, x.snd))
      (_ : ∀ (x y : ℕ × K), R K p x y → (fun x => mk K p (x.fst + 1, x.snd)) x = (fun x => mk K p (x.fst + 1, x.snd)) y)
hl : LeftInverse f ↑(frobenius (PerfectClosure K p) p)
hr : Function.RightInverse f ↑(frobenius (PerfectClosure K p) p)
⊢ Bijective ↑(frobenius (PerfectClosure K p) p)
[PROOFSTEP]
exact bijective_iff_has_inverse.mpr ⟨f, hl, hr⟩
[GOAL]
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (↑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = ↑(of K p) x
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ (↑(frobenius (PerfectClosure K p) p))^[Nat.zero] (mk K p (Nat.zero, x)) = ↑(of K p) x
case succ
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
ih : (↑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = ↑(of K p) x
⊢ (↑(frobenius (PerfectClosure K p) p))^[Nat.succ n] (mk K p (Nat.succ n, x)) = ↑(of K p) x
[PROOFSTEP]
rfl
[GOAL]
case succ
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
ih : (↑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = ↑(of K p) x
⊢ (↑(frobenius (PerfectClosure K p) p))^[Nat.succ n] (mk K p (Nat.succ n, x)) = ↑(of K p) x
[PROOFSTEP]
rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]
[GOAL]
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ PerfectClosure K p → L
[PROOFSTEP]
refine' fun e => liftOn e (fun x => (frobeniusEquiv L p).symm^[x.1] (f x.2)) _
[GOAL]
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
e : PerfectClosure K p
⊢ ∀ (x y : ℕ × K),
    R K p x y →
      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y
[PROOFSTEP]
rintro - - ⟨n, x⟩
[GOAL]
case intro
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
e : PerfectClosure K p
n : ℕ
x : K
⊢ (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) (n, x) =
    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) (n + 1, ↑(frobenius K p) x)
[PROOFSTEP]
simp [f.map_frobenius]
[GOAL]
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ ∀ (x y : PerfectClosure K p),
    OneHom.toFun
        {
          toFun := fun e =>
            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
              (_ :
                ∀ (x y : ℕ × K),
                  R K p x y →
                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
          map_one' := (_ : ↑f 1 = 1) }
        (x * y) =
      OneHom.toFun
          {
            toFun := fun e =>
              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                (_ :
                  ∀ (x y : ℕ × K),
                    R K p x y →
                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
            map_one' := (_ : ↑f 1 = 1) }
          x *
        OneHom.toFun
          {
            toFun := fun e =>
              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                (_ :
                  ∀ (x y : ℕ × K),
                    R K p x y →
                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
            map_one' := (_ : ↑f 1 = 1) }
          y
[PROOFSTEP]
rintro ⟨n, x⟩ ⟨m, y⟩
[GOAL]
case mk.mk.mk.mk
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
⊢ OneHom.toFun
      {
        toFun := fun e =>
          liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
            (_ :
              ∀ (x y : ℕ × K),
                R K p x y →
                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
        map_one' := (_ : ↑f 1 = 1) }
      (Quot.mk (R K p) (n, x) * Quot.mk (R K p) (m, y)) =
    OneHom.toFun
        {
          toFun := fun e =>
            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
              (_ :
                ∀ (x y : ℕ × K),
                  R K p x y →
                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
          map_one' := (_ : ↑f 1 = 1) }
        (Quot.mk (R K p) (n, x)) *
      OneHom.toFun
        {
          toFun := fun e =>
            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
              (_ :
                ∀ (x y : ℕ × K),
                  R K p x y →
                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
          map_one' := (_ : ↑f 1 = 1) }
        (Quot.mk (R K p) (m, y))
[PROOFSTEP]
simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_mul_mk, map_mul, iterate_map_mul]
[GOAL]
case mk.mk.mk.mk
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
⊢ (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n + m] ((↑(frobenius L p))^[m] (↑f x)) *
      (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n + m] ((↑(frobenius L p))^[n] (↑f y)) =
    (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n] (↑f x) * (↑(RingEquiv.symm (frobeniusEquiv L p)))^[m] (↑f y)
[PROOFSTEP]
have := LeftInverse.iterate (frobeniusEquiv_symm_apply_frobenius L p)
[GOAL]
case mk.mk.mk.mk
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
this : ∀ (n : ℕ), LeftInverse (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n] (fun x => ↑(frobenius L p) x)^[n]
⊢ (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n + m] ((↑(frobenius L p))^[m] (↑f x)) *
      (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n + m] ((↑(frobenius L p))^[n] (↑f y)) =
    (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n] (↑f x) * (↑(RingEquiv.symm (frobeniusEquiv L p)))^[m] (↑f y)
[PROOFSTEP]
rw [iterate_add_apply, this _ _, add_comm, iterate_add_apply, this _ _]
[GOAL]
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ ∀ (x y : PerfectClosure K p),
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun e =>
                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                    (_ :
                      ∀ (x y : ℕ × K),
                        R K p x y →
                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                map_one' := (_ : ↑f 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : PerfectClosure K p),
                  OneHom.toFun
                      {
                        toFun := fun e =>
                          liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                            (_ :
                              ∀ (x y : ℕ × K),
                                R K p x y →
                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                        map_one' := (_ : ↑f 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun e =>
                    liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                      (_ :
                        ∀ (x y : ℕ × K),
                          R K p x y →
                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                  map_one' := (_ : ↑f 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : PerfectClosure K p),
                    OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun e =>
                              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                (_ :
                                  ∀ (x y : ℕ × K),
                                    R K p x y →
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                            map_one' := (_ : ↑f 1 = 1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun e =>
                              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                (_ :
                                  ∀ (x y : ℕ × K),
                                    R K p x y →
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                            map_one' := (_ : ↑f 1 = 1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun e =>
                    liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                      (_ :
                        ∀ (x y : ℕ × K),
                          R K p x y →
                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                  map_one' := (_ : ↑f 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : PerfectClosure K p),
                    OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun e =>
                              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                (_ :
                                  ∀ (x y : ℕ × K),
                                    R K p x y →
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                            map_one' := (_ : ↑f 1 = 1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun e =>
                              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                (_ :
                                  ∀ (x y : ℕ × K),
                                    R K p x y →
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                            map_one' := (_ : ↑f 1 = 1) }
                          y) })
          y
[PROOFSTEP]
rintro ⟨n, x⟩ ⟨m, y⟩
[GOAL]
case mk.mk.mk.mk
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun e =>
                liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                  (_ :
                    ∀ (x y : ℕ × K),
                      R K p x y →
                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
              map_one' := (_ : ↑f 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : PerfectClosure K p),
                OneHom.toFun
                    {
                      toFun := fun e =>
                        liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                          (_ :
                            ∀ (x y : ℕ × K),
                              R K p x y →
                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                      map_one' := (_ : ↑f 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      {
                        toFun := fun e =>
                          liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                            (_ :
                              ∀ (x y : ℕ × K),
                                R K p x y →
                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                        map_one' := (_ : ↑f 1 = 1) }
                      x *
                    OneHom.toFun
                      {
                        toFun := fun e =>
                          liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                            (_ :
                              ∀ (x y : ℕ × K),
                                R K p x y →
                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                        map_one' := (_ : ↑f 1 = 1) }
                      y) })
      (Quot.mk (R K p) (n, x) + Quot.mk (R K p) (m, y)) =
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun e =>
                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                    (_ :
                      ∀ (x y : ℕ × K),
                        R K p x y →
                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                map_one' := (_ : ↑f 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : PerfectClosure K p),
                  OneHom.toFun
                      {
                        toFun := fun e =>
                          liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                            (_ :
                              ∀ (x y : ℕ × K),
                                R K p x y →
                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                        map_one' := (_ : ↑f 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        y) })
        (Quot.mk (R K p) (n, x)) +
      OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun e =>
                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                    (_ :
                      ∀ (x y : ℕ × K),
                        R K p x y →
                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                map_one' := (_ : ↑f 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : PerfectClosure K p),
                  OneHom.toFun
                      {
                        toFun := fun e =>
                          liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                            (_ :
                              ∀ (x y : ℕ × K),
                                R K p x y →
                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                        map_one' := (_ : ↑f 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        y) })
        (Quot.mk (R K p) (m, y))
[PROOFSTEP]
simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_add_mk, map_add, iterate_map_add]
[GOAL]
case mk.mk.mk.mk
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
⊢ (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n + m] ((↑(frobenius L p))^[m] (↑f x)) +
      (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n + m] ((↑(frobenius L p))^[n] (↑f y)) =
    (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n] (↑f x) + (↑(RingEquiv.symm (frobeniusEquiv L p)))^[m] (↑f y)
[PROOFSTEP]
have := LeftInverse.iterate (frobeniusEquiv_symm_apply_frobenius L p)
[GOAL]
case mk.mk.mk.mk
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
y✝ : PerfectClosure K p
m : ℕ
y : K
this : ∀ (n : ℕ), LeftInverse (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n] (fun x => ↑(frobenius L p) x)^[n]
⊢ (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n + m] ((↑(frobenius L p))^[m] (↑f x)) +
      (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n + m] ((↑(frobenius L p))^[n] (↑f y)) =
    (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n] (↑f x) + (↑(RingEquiv.symm (frobeniusEquiv L p)))^[m] (↑f y)
[PROOFSTEP]
rw [iterate_add_apply, this _ _, add_comm n, iterate_add_apply, this _ _]
[GOAL]
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ (fun f => RingHom.comp f (of K p))
      ((fun f =>
          {
            toMonoidHom :=
              {
                toOneHom :=
                  {
                    toFun := fun e =>
                      liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                        (_ :
                          ∀ (x y : ℕ × K),
                            R K p x y →
                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                    map_one' := (_ : ↑f 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : PerfectClosure K p),
                      OneHom.toFun
                          {
                            toFun := fun e =>
                              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                (_ :
                                  ∀ (x y : ℕ × K),
                                    R K p x y →
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                            map_one' := (_ : ↑f 1 = 1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun e =>
                                liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                  (_ :
                                    ∀ (x y : ℕ × K),
                                      R K p x y →
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                              map_one' := (_ : ↑f 1 = 1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun e =>
                                liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                  (_ :
                                    ∀ (x y : ℕ × K),
                                      R K p x y →
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                              map_one' := (_ : ↑f 1 = 1) }
                            y) },
            map_zero' := (_ : ↑f 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : PerfectClosure K p),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun e =>
                                liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                  (_ :
                                    ∀ (x y : ℕ × K),
                                      R K p x y →
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                              map_one' := (_ : ↑f 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : PerfectClosure K p),
                                OneHom.toFun
                                    {
                                      toFun := fun e =>
                                        liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                          (_ :
                                            ∀ (x y : ℕ × K),
                                              R K p x y →
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    x =
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    y),
                                      map_one' := (_ : ↑f 1 = 1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun e =>
                                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                    (_ :
                                      ∀ (x y : ℕ × K),
                                        R K p x y →
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                map_one' := (_ : ↑f 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : PerfectClosure K p),
                                  OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        y) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun e =>
                                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                    (_ :
                                      ∀ (x y : ℕ × K),
                                        R K p x y →
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                map_one' := (_ : ↑f 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : PerfectClosure K p),
                                  OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        y) })
                        y) })
        f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case a
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
x : K
⊢ ↑((fun f => RingHom.comp f (of K p))
          ((fun f =>
              {
                toMonoidHom :=
                  {
                    toOneHom :=
                      {
                        toFun := fun e =>
                          liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                            (_ :
                              ∀ (x y : ℕ × K),
                                R K p x y →
                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                        map_one' := (_ : ↑f 1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : PerfectClosure K p),
                          OneHom.toFun
                              {
                                toFun := fun e =>
                                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                    (_ :
                                      ∀ (x y : ℕ × K),
                                        R K p x y →
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                map_one' := (_ : ↑f 1 = 1) }
                              (x * y) =
                            OneHom.toFun
                                {
                                  toFun := fun e =>
                                    liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                      (_ :
                                        ∀ (x y : ℕ × K),
                                          R K p x y →
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                  map_one' := (_ : ↑f 1 = 1) }
                                x *
                              OneHom.toFun
                                {
                                  toFun := fun e =>
                                    liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                      (_ :
                                        ∀ (x y : ℕ × K),
                                          R K p x y →
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                  map_one' := (_ : ↑f 1 = 1) }
                                y) },
                map_zero' := (_ : ↑f 0 = 0),
                map_add' :=
                  (_ :
                    ∀ (x y : PerfectClosure K p),
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun e =>
                                    liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                      (_ :
                                        ∀ (x y : ℕ × K),
                                          R K p x y →
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                  map_one' := (_ : ↑f 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : PerfectClosure K p),
                                    OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun e =>
                                              liftOn e
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                (_ :
                                                  ∀ (x y : ℕ × K),
                                                    R K p x y →
                                                      (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          x =
                                                        (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          y),
                                            map_one' := (_ : ↑f 1 = 1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun e =>
                                              liftOn e
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                (_ :
                                                  ∀ (x y : ℕ × K),
                                                    R K p x y →
                                                      (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          x =
                                                        (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          y),
                                            map_one' := (_ : ↑f 1 = 1) }
                                          y) })
                          (x + y) =
                        OneHom.toFun
                            (↑{
                                toOneHom :=
                                  {
                                    toFun := fun e =>
                                      liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                        (_ :
                                          ∀ (x y : ℕ × K),
                                            R K p x y →
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                  y),
                                    map_one' := (_ : ↑f 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : PerfectClosure K p),
                                      OneHom.toFun
                                          {
                                            toFun := fun e =>
                                              liftOn e
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                (_ :
                                                  ∀ (x y : ℕ × K),
                                                    R K p x y →
                                                      (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          x =
                                                        (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          y),
                                            map_one' := (_ : ↑f 1 = 1) }
                                          (x * y) =
                                        OneHom.toFun
                                            {
                                              toFun := fun e =>
                                                liftOn e
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                  (_ :
                                                    ∀ (x y : ℕ × K),
                                                      R K p x y →
                                                        (fun x =>
                                                              (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst]
                                                                (↑f x.snd))
                                                            x =
                                                          (fun x =>
                                                              (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst]
                                                                (↑f x.snd))
                                                            y),
                                              map_one' := (_ : ↑f 1 = 1) }
                                            x *
                                          OneHom.toFun
                                            {
                                              toFun := fun e =>
                                                liftOn e
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                  (_ :
                                                    ∀ (x y : ℕ × K),
                                                      R K p x y →
                                                        (fun x =>
                                                              (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst]
                                                                (↑f x.snd))
                                                            x =
                                                          (fun x =>
                                                              (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst]
                                                                (↑f x.snd))
                                                            y),
                                              map_one' := (_ : ↑f 1 = 1) }
                                            y) })
                            x +
                          OneHom.toFun
                            (↑{
                                toOneHom :=
                                  {
                                    toFun := fun e =>
                                      liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                        (_ :
                                          ∀ (x y : ℕ × K),
                                            R K p x y →
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                  y),
                                    map_one' := (_ : ↑f 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : PerfectClosure K p),
                                      OneHom.toFun
                                          {
                                            toFun := fun e =>
                                              liftOn e
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                (_ :
                                                  ∀ (x y : ℕ × K),
                                                    R K p x y →
                                                      (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          x =
                                                        (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          y),
                                            map_one' := (_ : ↑f 1 = 1) }
                                          (x * y) =
                                        OneHom.toFun
                                            {
                                              toFun := fun e =>
                                                liftOn e
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                  (_ :
                                                    ∀ (x y : ℕ × K),
                                                      R K p x y →
                                                        (fun x =>
                                                              (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst]
                                                                (↑f x.snd))
                                                            x =
                                                          (fun x =>
                                                              (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst]
                                                                (↑f x.snd))
                                                            y),
                                              map_one' := (_ : ↑f 1 = 1) }
                                            x *
                                          OneHom.toFun
                                            {
                                              toFun := fun e =>
                                                liftOn e
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                  (_ :
                                                    ∀ (x y : ℕ × K),
                                                      R K p x y →
                                                        (fun x =>
                                                              (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst]
                                                                (↑f x.snd))
                                                            x =
                                                          (fun x =>
                                                              (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst]
                                                                (↑f x.snd))
                                                            y),
                                              map_one' := (_ : ↑f 1 = 1) }
                                            y) })
                            y) })
            f))
      x =
    ↑f x
[PROOFSTEP]
rfl
[GOAL]
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
⊢ (fun f =>
        {
          toMonoidHom :=
            {
              toOneHom :=
                {
                  toFun := fun e =>
                    liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                      (_ :
                        ∀ (x y : ℕ × K),
                          R K p x y →
                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                  map_one' := (_ : ↑f 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : PerfectClosure K p),
                    OneHom.toFun
                        {
                          toFun := fun e =>
                            liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                              (_ :
                                ∀ (x y : ℕ × K),
                                  R K p x y →
                                    (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                          map_one' := (_ : ↑f 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun e =>
                              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                (_ :
                                  ∀ (x y : ℕ × K),
                                    R K p x y →
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                            map_one' := (_ : ↑f 1 = 1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun e =>
                              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                (_ :
                                  ∀ (x y : ℕ × K),
                                    R K p x y →
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                            map_one' := (_ : ↑f 1 = 1) }
                          y) },
          map_zero' := (_ : ↑f 0 = 0),
          map_add' :=
            (_ :
              ∀ (x y : PerfectClosure K p),
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          {
                            toFun := fun e =>
                              liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                (_ :
                                  ∀ (x y : ℕ × K),
                                    R K p x y →
                                      (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                            map_one' := (_ : ↑f 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : PerfectClosure K p),
                              OneHom.toFun
                                  {
                                    toFun := fun e =>
                                      liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                        (_ :
                                          ∀ (x y : ℕ × K),
                                            R K p x y →
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                  y),
                                    map_one' := (_ : ↑f 1 = 1) }
                                  (x * y) =
                                OneHom.toFun
                                    {
                                      toFun := fun e =>
                                        liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                          (_ :
                                            ∀ (x y : ℕ × K),
                                              R K p x y →
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    x =
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    y),
                                      map_one' := (_ : ↑f 1 = 1) }
                                    x *
                                  OneHom.toFun
                                    {
                                      toFun := fun e =>
                                        liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                          (_ :
                                            ∀ (x y : ℕ × K),
                                              R K p x y →
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    x =
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    y),
                                      map_one' := (_ : ↑f 1 = 1) }
                                    y) })
                    (x + y) =
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun e =>
                                liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                  (_ :
                                    ∀ (x y : ℕ × K),
                                      R K p x y →
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                              map_one' := (_ : ↑f 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : PerfectClosure K p),
                                OneHom.toFun
                                    {
                                      toFun := fun e =>
                                        liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                          (_ :
                                            ∀ (x y : ℕ × K),
                                              R K p x y →
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    x =
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    y),
                                      map_one' := (_ : ↑f 1 = 1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      y) })
                      x +
                    OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun e =>
                                liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                  (_ :
                                    ∀ (x y : ℕ × K),
                                      R K p x y →
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                              map_one' := (_ : ↑f 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : PerfectClosure K p),
                                OneHom.toFun
                                    {
                                      toFun := fun e =>
                                        liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                          (_ :
                                            ∀ (x y : ℕ × K),
                                              R K p x y →
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    x =
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                    y),
                                      map_one' := (_ : ↑f 1 = 1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      y) })
                      y) })
      ((fun f => RingHom.comp f (of K p)) f) =
    f
[PROOFSTEP]
ext ⟨n, x⟩
[GOAL]
case a.mk.mk
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ ↑((fun f =>
            {
              toMonoidHom :=
                {
                  toOneHom :=
                    {
                      toFun := fun e =>
                        liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                          (_ :
                            ∀ (x y : ℕ × K),
                              R K p x y →
                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                      map_one' := (_ : ↑f 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : PerfectClosure K p),
                        OneHom.toFun
                            {
                              toFun := fun e =>
                                liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                  (_ :
                                    ∀ (x y : ℕ × K),
                                      R K p x y →
                                        (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                              map_one' := (_ : ↑f 1 = 1) }
                            (x * y) =
                          OneHom.toFun
                              {
                                toFun := fun e =>
                                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                    (_ :
                                      ∀ (x y : ℕ × K),
                                        R K p x y →
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                map_one' := (_ : ↑f 1 = 1) }
                              x *
                            OneHom.toFun
                              {
                                toFun := fun e =>
                                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                    (_ :
                                      ∀ (x y : ℕ × K),
                                        R K p x y →
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                map_one' := (_ : ↑f 1 = 1) }
                              y) },
              map_zero' := (_ : ↑f 0 = 0),
              map_add' :=
                (_ :
                  ∀ (x y : PerfectClosure K p),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun e =>
                                  liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                    (_ :
                                      ∀ (x y : ℕ × K),
                                        R K p x y →
                                          (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                map_one' := (_ : ↑f 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : PerfectClosure K p),
                                  OneHom.toFun
                                      {
                                        toFun := fun e =>
                                          liftOn e
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                            (_ :
                                              ∀ (x y : ℕ × K),
                                                R K p x y →
                                                  (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      x =
                                                    (fun x =>
                                                        (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                      y),
                                        map_one' := (_ : ↑f 1 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        y) })
                        (x + y) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun e =>
                                    liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                      (_ :
                                        ∀ (x y : ℕ × K),
                                          R K p x y →
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                  map_one' := (_ : ↑f 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : PerfectClosure K p),
                                    OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun e =>
                                              liftOn e
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                (_ :
                                                  ∀ (x y : ℕ × K),
                                                    R K p x y →
                                                      (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          x =
                                                        (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          y),
                                            map_one' := (_ : ↑f 1 = 1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun e =>
                                              liftOn e
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                (_ :
                                                  ∀ (x y : ℕ × K),
                                                    R K p x y →
                                                      (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          x =
                                                        (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          y),
                                            map_one' := (_ : ↑f 1 = 1) }
                                          y) })
                          x +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun e =>
                                    liftOn e (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                      (_ :
                                        ∀ (x y : ℕ × K),
                                          R K p x y →
                                            (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) x =
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd)) y),
                                  map_one' := (_ : ↑f 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : PerfectClosure K p),
                                    OneHom.toFun
                                        {
                                          toFun := fun e =>
                                            liftOn e
                                              (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                              (_ :
                                                ∀ (x y : ℕ × K),
                                                  R K p x y →
                                                    (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        x =
                                                      (fun x =>
                                                          (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                        y),
                                          map_one' := (_ : ↑f 1 = 1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun e =>
                                              liftOn e
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                (_ :
                                                  ∀ (x y : ℕ × K),
                                                    R K p x y →
                                                      (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          x =
                                                        (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          y),
                                            map_one' := (_ : ↑f 1 = 1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun e =>
                                              liftOn e
                                                (fun x => (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                (_ :
                                                  ∀ (x y : ℕ × K),
                                                    R K p x y →
                                                      (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          x =
                                                        (fun x =>
                                                            (↑(RingEquiv.symm (frobeniusEquiv L p)))^[x.fst] (↑f x.snd))
                                                          y),
                                            map_one' := (_ : ↑f 1 = 1) }
                                          y) })
                          y) })
          ((fun f => RingHom.comp f (of K p)) f))
      (Quot.mk (R K p) (n, x)) =
    ↑f (Quot.mk (R K p) (n, x))
[PROOFSTEP]
simp only [quot_mk_eq_mk, RingHom.comp_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, liftOn_mk]
[GOAL]
case a.mk.mk
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ (↑(RingEquiv.symm (frobeniusEquiv L p)))^[n] (↑f (↑(of K p) x)) = ↑f (mk K p (n, x))
[PROOFSTEP]
apply (injective_frobenius L p).iterate n
[GOAL]
case a.mk.mk.a
K : Type u
inst✝⁵ : Field K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ (↑(frobenius L p))^[n] ((↑(RingEquiv.symm (frobeniusEquiv L p)))^[n] (↑f (↑(of K p) x))) =
    (↑(frobenius L p))^[n] (↑f (mk K p (n, x)))
[PROOFSTEP]
rw [← f.map_iterate_frobenius, iterate_frobenius_mk, RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm L p) n]
