awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
n : ℕ
ih : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)
simp_rw simp_rw₁ :
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + 0]
      ((⇑(frobenius K p) : (a : K) → K)^[x.1] (x.2 ^ n) * (⇑(frobenius K p) : (a : K) → K)^[x.1] x.2) =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + x.1 + 0] (x.2 ^ n * x.2)
⊢ (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
                (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2
have simp_rw₂ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ (x.1 + 0) = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1 + 0)
Tactic: simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
n : ℕ
ih : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)
simp_rw simp_rw₁ :
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + 0]
      ((⇑(frobenius K p) : (a : K) → K)^[x.1] (x.2 ^ n) * (⇑(frobenius K p) : (a : K) → K)^[x.1] x.2) =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + x.1 + 0] (x.2 ^ n * x.2)
simp_rw₂ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ (x.1 + 0) = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1 + 0)
⊢ (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
                (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2
have simp_rw₃ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1)
Tactic: simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
n : ℕ
ih : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)
simp_rw simp_rw₁ :
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + 0]
      ((⇑(frobenius K p) : (a : K) → K)^[x.1] (x.2 ^ n) * (⇑(frobenius K p) : (a : K) → K)^[x.1] x.2) =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + x.1 + 0] (x.2 ^ n * x.2)
simp_rw₂ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ (x.1 + 0) = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1 + 0)
simp_rw₃ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1)
⊢ (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
                (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2
have simp_rw₄ : ((x.2 ^ n) ^ p ^ x.1) ^ p ^ x.1 * (x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n) ^ p ^ (x.1 + x.1) * x.2 ^ p ^ (x.1 + x.1)
Tactic: simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
n : ℕ
ih : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)
simp_rw simp_rw₁ :
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + 0]
      ((⇑(frobenius K p) : (a : K) → K)^[x.1] (x.2 ^ n) * (⇑(frobenius K p) : (a : K) → K)^[x.1] x.2) =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + x.1 + 0] (x.2 ^ n * x.2)
simp_rw₂ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ (x.1 + 0) = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1 + 0)
simp_rw₃ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1)
simp_rw₄ :
  ((x.2 ^ n) ^ p ^ x.1) ^ p ^ x.1 * (x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n) ^ p ^ (x.1 + x.1) * x.2 ^ p ^ (x.1 + x.1)
⊢ (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
                (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2
have simp_rw₅ : x.2 ^ (n * p ^ x.1 * p ^ x.1) * x.2 ^ (p ^ x.1 * p ^ x.1) = x.2 ^ (n * p ^ (x.1 + x.1)) * x.2 ^ p ^ (x.1 + x.1)
Tactic: simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
n : ℕ
ih : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)
simp_rw simp_rw₁ :
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + 0]
      ((⇑(frobenius K p) : (a : K) → K)^[x.1] (x.2 ^ n) * (⇑(frobenius K p) : (a : K) → K)^[x.1] x.2) =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + x.1 + 0] (x.2 ^ n * x.2)
simp_rw₂ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ (x.1 + 0) = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1 + 0)
simp_rw₃ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1)
simp_rw₄ :
  ((x.2 ^ n) ^ p ^ x.1) ^ p ^ x.1 * (x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n) ^ p ^ (x.1 + x.1) * x.2 ^ p ^ (x.1 + x.1)
simp_rw₅ :
  x.2 ^ (n * p ^ x.1 * p ^ x.1) * x.2 ^ (p ^ x.1 * p ^ x.1) = x.2 ^ (n * p ^ (x.1 + x.1)) * x.2 ^ p ^ (x.1 + x.1)
⊢ (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
                (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2
have simp_rw₆ : x.2 ^ (n * p ^ x.1 * p ^ x.1 + p ^ (x.1 + x.1)) = x.2 ^ (n * p ^ (x.1 + x.1) + p ^ (x.1 + x.1))
Tactic: simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
n : ℕ
ih : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)
simp_rw simp_rw₁ :
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + 0]
      ((⇑(frobenius K p) : (a : K) → K)^[x.1] (x.2 ^ n) * (⇑(frobenius K p) : (a : K) → K)^[x.1] x.2) =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + x.1 + 0] (x.2 ^ n * x.2)
simp_rw₂ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ (x.1 + 0) = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1 + 0)
simp_rw₃ : ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1)
simp_rw₄ :
  ((x.2 ^ n) ^ p ^ x.1) ^ p ^ x.1 * (x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n) ^ p ^ (x.1 + x.1) * x.2 ^ p ^ (x.1 + x.1)
simp_rw₅ :
  x.2 ^ (n * p ^ x.1 * p ^ x.1) * x.2 ^ (p ^ x.1 * p ^ x.1) = x.2 ^ (n * p ^ (x.1 + x.1)) * x.2 ^ p ^ (x.1 + x.1)
simp_rw₆ : x.2 ^ (n * p ^ x.1 * p ^ x.1 + p ^ (x.1 + x.1)) = x.2 ^ (n * p ^ (x.1 + x.1) + p ^ (x.1 + x.1))
⊢ (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p) : (a : K) → K)^[x.1] (x.1, x.2 ^ n).2 *
                (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2
have simp_rw₇ : x.2 ^ (n * (p ^ x.1 * p ^ x.1) + p ^ (x.1 + x.1)) = x.2 ^ (n * p ^ (x.1 + x.1) + p ^ (x.1 + x.1))
Tactic: simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
n : ℕ
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)
have zero : HPow.hPow (α := PerfectClosure K p) (β := ℕ) (mk K p x) 0 = mk K p (x.1, HPow.hPow (β := ℕ) x.2 0)
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]⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
n : ℕ
zero : HPow.hPow (α := PerfectClosure K p) (β := ℕ) (mk K p x) 0 = mk K p (x.1, HPow.hPow (β := ℕ) x.2 0)
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)
have succ : ∀ (n : ℕ) (ih : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = mk K p (x.1, x.2 ^ n)),
  HPow.hPow (α := PerfectClosure K p) (mk K p x) (n + 1) = mk K p (x.1, x.2 ^ (n + 1))
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]⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))
have zero : Eq (α := PerfectClosure K p) (↑0 : PerfectClosure K p) (mk K p (0, (↑0 : K)))
Tactic: induction x with
    | zero => simp
    | succ x ih => simp [Nat.cast_succ, ih, one_def]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ
zero : Eq (α := PerfectClosure K p) (↑0 : PerfectClosure K p) (mk K p (0, (↑0 : K)))
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))
have zero₁ : ∀ (x : ℕ) (ih : Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))),
  Eq (α := PerfectClosure K p) (↑(x + 1) : PerfectClosure K p) (mk K p (0, (↑(x + 1) : K)))
Tactic: induction x with
    | zero => simp
    | succ x ih => simp [Nat.cast_succ, ih, one_def]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x n : ℕ
ih : Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n, (↑x : K)))
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n + 1, (↑x : K)))
have succ : Eq (α := PerfectClosure K p) (mk K p (n, (↑x : K))) (mk K p (n + 1, (↑x : K)))
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x n : ℕ
ih : Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n, (↑x : K)))
⊢ Eq (α := PerfectClosure K p) (mk K p (n, (↑x : K))) (mk K p (n + 1, (↑x : K)))
have succ : R K p (n, (↑x : K)) (n + 1, (↑x : K))
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x n : ℕ
ih : Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n, (↑x : K)))
this : R K p ((n, (↑x : K)) : ℕ × K) ((n.succ, (frobenius K p : (a : K) → K) (↑x : K)) : ℕ × K)
⊢ R K p (n, (↑x : K)) (n + 1, (↑x : K))
have rwa : ∀ (this : R K p (n, (↑x : K)) (n.succ, (↑x : K))), R K p (n, (↑x : K)) (n + 1, (↑x : K))
Tactic: rwa [map_natCast] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x n : ℕ
ih : Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n, (↑x : K)))
⊢ R K p (n, (↑x : K)) (n + 1, (↑x : K))
have succ : R K p ((n, (↑x : K)) : ℕ × K) ((n.succ, (frobenius K p : (a : K) → K) (↑x : K)) : ℕ × K)
Tactic: suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by
      rwa [map_natCast] at this
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
n x : ℕ
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n, (↑x : K)))
have zero : Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))
Tactic: induction n with
  | zero =>
    induction x with
    | zero => simp
    | succ x ih => simp [Nat.cast_succ, ih, one_def]
  | succ n ih =>
    rw [ih]; apply Quot.sound
    suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by
      rwa [map_natCast] at this
    apply R.intro
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
n x : ℕ
zero : Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n, (↑x : K)))
have succ : ∀ (n : ℕ) (ih : Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n, (↑x : K)))),
  Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n + 1, (↑x : K)))
Tactic: induction n with
  | zero =>
    induction x with
    | zero => simp
    | succ x ih => simp [Nat.cast_succ, ih, one_def]
  | succ n ih =>
    rw [ih]; apply Quot.sound
    suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by
      rwa [map_natCast] at this
    apply R.intro
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℤ
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))
have ofNat : ∀ (a : ℕ), Eq (α := PerfectClosure K p) (↑(Int.ofNat a) : PerfectClosure K p) (mk K p (0, (↑(Int.ofNat a) : K)))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℤ
ofNat : ∀ (a : ℕ), Eq (α := PerfectClosure K p) (↑(Int.ofNat a) : PerfectClosure K p) (mk K p (0, (↑(Int.ofNat a) : K)))
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))
have negSucc : ∀ (a : ℕ), Eq (α := PerfectClosure K p) (↑(Int.negSucc a) : PerfectClosure K p) (mk K p (0, (↑(Int.negSucc a) : K)))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y : ℕ
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p) ↔
    Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
have mp : Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p) →
  Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y : ℕ
mp :
  Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p) →
    Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p) ↔
    Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
have mpr : Eq.{u + 1} (α := K) (↑x : K) (↑y : K) →
  Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (hypothesis)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y : ℕ
H : Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p)
⊢ Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
have H₁ : ∃ (z : ℕ),
  Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[(0, (↑y : K)).1 + z] (0, (↑x : K)).2)
    ((⇑(frobenius K p) : (a : K) → K)^[(0, (↑x : K)).1 + z] (0, (↑y : K)).2)
Tactic: rw [natCast K p 0, natCast K p 0, mk_eq_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y : ℕ
H :
  ∃ (z : ℕ),
    Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[(0, (↑y : K)).1 + z] (0, (↑x : K)).2)
      ((⇑(frobenius K p) : (a : K) → K)^[(0, (↑x : K)).1 + z] (0, (↑y : K)).2)
⊢ Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
have mp : ∀ (z : ℕ)
  (H :
    Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[(0, (↑y : K)).1 + z] (0, (↑x : K)).2)
      ((⇑(frobenius K p) : (a : K) → K)^[(0, (↑x : K)).1 + z] (0, (↑y : K)).2)),
  Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
Tactic: obtain ⟨z, H⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y : ℕ
H : Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p)
have mpr : Eq (α := PerfectClosure K p) (mk K p (0, (↑x : K))) (↑y : PerfectClosure K p)
Tactic: rw [natCast K p 0, natCast K p 0, H]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y : ℕ
H : Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
mpr : Eq (α := PerfectClosure K p) (mk K p (0, (↑x : K))) (↑y : PerfectClosure K p)
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p)
have mpr₁ : Eq (α := PerfectClosure K p) (mk K p (0, (↑x : K))) (mk K p (0, (↑y : K)))
Tactic: rw [natCast K p 0, natCast K p 0, H]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y : ℕ
H : Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
mpr : Eq (α := PerfectClosure K p) (mk K p (0, (↑x : K))) (↑y : PerfectClosure K p)
mpr₁ : Eq (α := PerfectClosure K p) (mk K p (0, (↑x : K))) (mk K p (0, (↑y : K)))
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p)
have mpr₂ : Eq (α := PerfectClosure K p) (mk K p (0, (↑y : K))) (mk K p (0, (↑y : K)))
Tactic: rw [natCast K p 0, natCast K p 0, H]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
⊢ CharP.{u} (PerfectClosure K p) p
have cast_eq_zero_iff : ∀ (x : ℕ), Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ p ∣ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ p ∣ x
have cast_eq_zero_iff : Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ Eq.{u + 1} (α := K) (↑x : K) 0
Tactic: rw [← CharP.cast_eq_zero_iff K]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ Eq.{u + 1} (α := K) (↑x : K) 0
have cast_eq_zero_iff : Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑0 : PerfectClosure K p) ↔
  Eq.{u + 1} (α := K) (↑x : K) 0
Tactic: rw [← Nat.cast_zero, natCast_eq_iff, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ
cast_eq_zero_iff :
  Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑0 : PerfectClosure K p) ↔
    Eq.{u + 1} (α := K) (↑x : K) 0
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ Eq.{u + 1} (α := K) (↑x : K) 0
have cast_eq_zero_iff₁ : Eq.{u + 1} (α := K) (↑x : K) (↑0 : K) ↔ Eq.{u + 1} (α := K) (↑x : K) 0
Tactic: rw [← Nat.cast_zero, natCast_eq_iff, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ
cast_eq_zero_iff :
  Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑0 : PerfectClosure K p) ↔
    Eq.{u + 1} (α := K) (↑x : K) 0
cast_eq_zero_iff₁ : Eq.{u + 1} (α := K) (↑x : K) (↑0 : K) ↔ Eq.{u + 1} (α := K) (↑x : K) 0
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ Eq.{u + 1} (α := K) (↑x : K) 0
have cast_eq_zero_iff₂ : Eq.{u + 1} (α := K) (↑x : K) 0 ↔ Eq.{u + 1} (α := K) (↑x : K) 0
Tactic: rw [← Nat.cast_zero, natCast_eq_iff, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n : ℕ
h : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = 0
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n) = 0
have rw : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n + n) = 0
Tactic: rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),
        pow_add, h, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n : ℕ
h : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = 0
rw : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n + n) = 0
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n) = 0
have rw₁ : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n) * HPow.hPow (α := PerfectClosure K p) (mk K p x) n = 0
Tactic: rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),
        pow_add, h, mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n : ℕ
h : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = 0
rw : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n + n) = 0
rw₁ : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n) * HPow.hPow (α := PerfectClosure K p) (mk K p x) n = 0
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n) = 0
have rw₂ : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n) * 0 = 0
Tactic: rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),
        pow_add, h, mul_zero]