-- Mathlib/FieldTheory/PerfectClosure.lean
theorem mk_pow (x : ℕ × K) (n : ℕ) : mk K p x ^ n = mk K p (x.1, x.2 ^ n)

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
⊢ mk K p x ^ n = mk K p (x.1, x.2 ^ n)

Tactic:
induction n with
| zero =>
  rw [pow_zero, pow_zero, one_def, mk_eq_iff]
  exact ⟨0, by simp_rw [← coe_iterateFrobenius, map_one]⟩
| succ n ih =>
  rw [pow_succ, pow_succ, ih, mk_mul_mk, mk_eq_iff]
  exact ⟨0, by simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
    ← pow_add, mul_assoc, ← pow_add]⟩

Result:
no goals

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ (⇑(frobenius K p))^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K
            p))^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2

Tactic:
simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
← pow_add, mul_assoc, ← pow_add]

Result:
no goals

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ ∃ z,
    (⇑(frobenius K p))^[(x.1, x.2 ^ n * x.2).1 + z]
        ((x.1, x.2 ^ n).1 + x.1,
            (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).2 =
      (⇑(frobenius K
              p))^[((x.1, x.2 ^ n).1 + x.1,
                (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).1 +
            z]
        (x.1, x.2 ^ n * x.2).2

Tactic:
exact ⟨0, by simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
  ← pow_add, mul_assoc, ← pow_add]⟩

Result:
no goals

Proof state:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ ∃ z, (⇑(frobenius K p))^[(x.1, 1).1 + z] (0, 1).2 = (⇑(frobenius K p))^[(0, 1).1 + z] (x.1, 1).2

Tactic:
exact ⟨0, by simp_rw [← coe_iterateFrobenius, map_one]⟩

Result:
no goals

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ (⇑(frobenius K p))^[(x.1, 1).1 + 0] (0, 1).2 = (⇑(frobenius K p))^[(0, 1).1 + 0] (x.1, 1).2

Tactic:
simp_rw [← coe_iterateFrobenius, map_one]

Result:
no goals

Proof state:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ mk K p x ^ 0 = mk K p (x.1, x.2 ^ 0)

Tactic:
rw [pow_zero, pow_zero, one_def, mk_eq_iff]

Result:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ ∃ z, (⇑(frobenius K p))^[(x.1, 1).1 + z] (0, 1).2 = (⇑(frobenius K p))^[(0, 1).1 + z] (x.1, 1).2

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ mk K p x ^ (n + 1) = mk K p (x.1, x.2 ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, ih, mk_mul_mk, mk_eq_iff]

Result:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ ∃ z,
    (⇑(frobenius K p))^[(x.1, x.2 ^ n * x.2).1 + z]
        ((x.1, x.2 ^ n).1 + x.1,
            (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).2 =
      (⇑(frobenius K
              p))^[((x.1, x.2 ^ n).1 + x.1,
                (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).1 +
            z]
        (x.1, x.2 ^ n * x.2).2