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)
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)
simp only [frobenius_def]
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)
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)
cases' x with n x
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)
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)
dsimp only
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')
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)
suffices ∀ p' : ℕ, mk K p (n, x) ^ p' = mk K p (n, x ^ p') by apply this
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)
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')
intro p
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)
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)
induction' p with p ih
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)
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)
case zero => apply R.sound; rw [(frobenius _ _).iterate_map_one, pow_zero]
no goals
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)
case succ =>
  rw [pow_succ, ih]
  symm
  apply R.sound
  simp only [pow_succ, (frobenius _ _).iterate_map_mul]
no goals
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)
apply this
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
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)
apply R.sound
no goals
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
rw [(frobenius _ _).iterate_map_one, pow_zero]
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)
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)
rw [pow_succ, ih]
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)
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)
symm
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
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)
apply R.sound
no goals
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
simp only [pow_succ, (frobenius _ _).iterate_map_mul]