awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
inst_4 : DecidableEq R
rw :
  toFinset
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
⊢ Finset.image (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
      (toFinset (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
have rw₁ : (p ^ n • f.roots).toFinset = f.roots.toFinset
Tactic: rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
    (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
inst_4 : DecidableEq R
rw :
  toFinset
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
rw₁ : (p ^ n • f.roots).toFinset = f.roots.toFinset
⊢ Finset.image (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
      (toFinset (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
have rw₂ : f.roots.toFinset = f.roots.toFinset
Tactic: rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
    (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
inst_4 : DecidableEq R
⊢ Finset.image (α := R) (⇑(frobenius R p) : (a : R) → R) (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
have rw : toFinset (Multiset.map (α := R) (⇑(frobenius R p) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f))) =
  f.roots.toFinset
Tactic: rw [Finset.image_toFinset, roots_expand_map_frobenius,
      (roots f).toFinset_nsmul _ (expChar_pos R p).ne']
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
inst_4 : DecidableEq R
rw :
  toFinset (Multiset.map (α := R) (⇑(frobenius R p) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
⊢ Finset.image (α := R) (⇑(frobenius R p) : (a : R) → R) (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
have rw₁ : (p • f.roots).toFinset = f.roots.toFinset
Tactic: rw [Finset.image_toFinset, roots_expand_map_frobenius,
      (roots f).toFinset_nsmul _ (expChar_pos R p).ne']
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : PerfectRing R p
inst_4 : DecidableEq R
rw :
  toFinset (Multiset.map (α := R) (⇑(frobenius R p) : (a : R) → R) (roots ((expand R p : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
rw₁ : (p • f.roots).toFinset = f.roots.toFinset
⊢ Finset.image (α := R) (⇑(frobenius R p) : (a : R) → R) (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) =
    f.roots.toFinset
have rw₂ : f.roots.toFinset = f.roots.toFinset
Tactic: rw [Finset.image_toFinset, roots_expand_map_frobenius,
      (roots f).toFinset_nsmul _ (expChar_pos R p).ne']
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : DecidableEq R
inst_4 : PerfectRing R p
⊢ (⇑(RingEquiv.toEquiv (frobeniusEquiv R p)) : (a : R) → R) ''
      (↑(toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) : Set R) =
    (↑f.roots.toFinset : Set R)
have rw : (⇑(RingEquiv.toEquiv (frobeniusEquiv R p)) : (a : R) → R) ''
    (↑(toFinset (roots ((expand R p : (a : R[X]) → R[X]) f))) : Set R) =
  (↑(Finset.image (α := R) (⇑(frobenius R p) : (a : R) → R) (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f)))) :
    Set R)
Tactic: rw [← roots_expand_image_frobenius (p := p) (f := f)]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n_1 : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : DecidableEq R
inst_4 : PerfectRing R p
n : ℕ
⊢ (⇑(RingEquiv.toEquiv (iterateFrobeniusEquiv R p n)) : (a : R) → R) ''
      (↑(toFinset (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) : Set R) =
    (↑f.roots.toFinset : Set R)
have rw : (⇑(RingEquiv.toEquiv (iterateFrobeniusEquiv R p n)) : (a : R) → R) ''
    (↑(toFinset (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) : Set R) =
  (↑(Finset.image (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (toFinset (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))) :
    Set R)
Tactic: rw [← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := 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
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p
    ((n, x).1 + y.1, (⇑(frobenius K p) : (a : K) → K)^[y.1] (n, x).2 * (⇑(frobenius K p) : (a : K) → K)^[(n, x).1] y.2)
    (((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1 + y.1,
      HMul.hMul (α := K) ((⇑(frobenius K p) : (a : K) → K)^[y.1] (n + 1, (frobenius K p : (a : K) → K) x).2 : K)
        ((⇑(frobenius K p) : (a : K) → K)^[((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1] y.2))
have rw : R K p
  ((n, x).1 + y.1, (⇑(frobenius K p) : (a : K) → K)^[y.1] (n, x).2 * (⇑(frobenius K p) : (a : K) → K)^[(n, x).1] y.2)
  ((n + y.1).succ,
    (frobenius K p : (a : K) → K) ((⇑(frobenius K p) : (a : K) → K)^[y.1] x * (⇑(frobenius K p) : (a : K) → K)^[n] y.2))
Tactic: rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_mul,
        Nat.succ_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 y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p
    (x.1 + (n, y).1, (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] x.2 * (⇑(frobenius K p) : (a : K) → K)^[x.1] (n, y).2)
    (x.1 + ((n + 1, (frobenius K p : (a : K) → K) y) : ℕ × K).1,
      HMul.hMul (β := K) ((⇑(frobenius K p) : (a : K) → K)^[((n + 1, (frobenius K p : (a : K) → K) y) : ℕ × K).1] x.2)
        ((⇑(frobenius K p) : (a : K) → K)^[x.1] (n + 1, (frobenius K p : (a : K) → K) y).2 : K))
have rw : R K p
  (x.1 + (n, y).1, (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] x.2 * (⇑(frobenius K p) : (a : K) → K)^[x.1] (n, y).2)
  (x.1 + ((n + 1, (frobenius K p : (a : K) → K) y) : ℕ × K).1,
    (frobenius K p : (a : K) → K) ((⇑(frobenius K p) : (a : K) → K)^[n] x.2 * (⇑(frobenius K p) : (a : K) → K)^[x.1] y))
Tactic: rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_mul]
-- 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
e f g : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
x_2 : ℕ × K
n : ℕ
y : K
x_3 : ℕ × 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))
have apply : (((m, x).1 + (n, y).1,
          (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (m, x).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (n, y).2).1 +
      (s, z).1,
    (⇑(frobenius K p) : (a : K) → K)^[(s, z).1]
        ((m, x).1 + (n, y).1,
            (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (m, x).2 *
              (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (n, y).2).2 *
      (⇑(frobenius K p) :
            (a : K) →
              K)^[((m, x).1 + (n, y).1,
              (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (m, x).2 *
                (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (n, y).2).1]
        (s, z).2) =
  ((m, x).1 +
      ((n, y).1 + (s, z).1,
          (⇑(frobenius K p) : (a : K) → K)^[(s, z).1] (n, y).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (s, z).2).1,
    (⇑(frobenius K p) :
            (a : K) →
              K)^[((n, y).1 + (s, z).1,
              (⇑(frobenius K p) : (a : K) → K)^[(s, z).1] (n, y).2 *
                (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (s, z).2).1]
        (m, x).2 *
      (⇑(frobenius K p) : (a : K) → K)^[(m, x).1]
        ((n, y).1 + (s, z).1,
            (⇑(frobenius K p) : (a : K) → K)^[(s, z).1] (n, y).2 *
              (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (s, z).2).2)
Tactic: apply congr_arg (Quot.mk _)
-- 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
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p
    ((n, x).1 + y.1, (⇑(frobenius K p) : (a : K) → K)^[y.1] (n, x).2 + (⇑(frobenius K p) : (a : K) → K)^[(n, x).1] y.2)
    (((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1 + y.1,
      HAdd.hAdd (α := K) ((⇑(frobenius K p) : (a : K) → K)^[y.1] (n + 1, (frobenius K p : (a : K) → K) x).2 : K)
        ((⇑(frobenius K p) : (a : K) → K)^[((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1] y.2))
have rw : R K p
  ((n, x).1 + y.1, (⇑(frobenius K p) : (a : K) → K)^[y.1] (n, x).2 + (⇑(frobenius K p) : (a : K) → K)^[(n, x).1] y.2)
  ((n + y.1).succ,
    (frobenius K p : (a : K) → K) ((⇑(frobenius K p) : (a : K) → K)^[y.1] x + (⇑(frobenius K p) : (a : K) → K)^[n] y.2))
Tactic: rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_add,
        Nat.succ_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 y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p
    (x.1 + (n, y).1, (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] x.2 + (⇑(frobenius K p) : (a : K) → K)^[x.1] (n, y).2)
    (x.1 + ((n + 1, (frobenius K p : (a : K) → K) y) : ℕ × K).1,
      HAdd.hAdd (β := K) ((⇑(frobenius K p) : (a : K) → K)^[((n + 1, (frobenius K p : (a : K) → K) y) : ℕ × K).1] x.2)
        ((⇑(frobenius K p) : (a : K) → K)^[x.1] (n + 1, (frobenius K p : (a : K) → K) y).2 : K))
have rw : R K p
  (x.1 + (n, y).1, (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] x.2 + (⇑(frobenius K p) : (a : K) → K)^[x.1] (n, y).2)
  (x.1 + ((n + 1, (frobenius K p : (a : K) → K) y) : ℕ × K).1,
    (frobenius K p : (a : K) → K) ((⇑(frobenius K p) : (a : K) → K)^[n] x.2 + (⇑(frobenius K p) : (a : K) → K)^[x.1] y))
Tactic: rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_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_1 y : ℕ × K
H : R K p x_1 y
n : ℕ
x : K
⊢ R K p ((n, x).1, -(n, x).2)
    (((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1, -(n + 1, (frobenius K p : (a : K) → K) x).2)
have rw : R K p ((n, x).1, -(n, x).2) (((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1, (frobenius K p : (a : K) → K) (-x))
Tactic: rw [← map_neg]
-- 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 : ℕ
ih : Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0
⊢ Eq (α := PerfectClosure K p) (mk K p (n + 1, 0)) 0
have succ : Eq (α := PerfectClosure K p) (mk K p (n + 1, 0)) (mk K p (n, 0))
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
n : ℕ
ih : Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0
⊢ Eq (α := PerfectClosure K p) (mk K p (n + 1, 0)) (mk K p (n, 0))
have apply : R K p (n, 0) (n + 1, 0)
Tactic: apply (Quot.sound _).symm
-- 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
n : ℕ
ih : Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0
⊢ R K p (n, 0) (n + 1, 0)
have this : R K p ((n, 0) : ℕ × K) ((n + 1, (frobenius K p : (a : K) → K) 0) : ℕ × K)
Tactic: have := R.intro (p := p) n (0 : 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
n : ℕ
ih : Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0
this : R K p ((n, 0) : ℕ × K) ((n + 1, (frobenius K p : (a : K) → K) 0) : ℕ × K)
⊢ R K p (n, 0) (n + 1, 0)
have rwa : ∀ (this : R K p (n, 0) (n + 1, 0)), R K p (n, 0) (n + 1, 0)
Tactic: rwa [map_zero] 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
n : ℕ
⊢ Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0
have zero : Eq (α := PerfectClosure K p) (mk K p (0, 0)) 0
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [← ih]
    apply (Quot.sound _).symm
    have := R.intro (p := p) n (0 : K)
    rwa [map_zero] at this
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 : ℕ
zero : Eq (α := PerfectClosure K p) (mk K p (0, 0)) 0
⊢ Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0
have succ : ∀ (n : ℕ) (ih : Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0), Eq (α := PerfectClosure K p) (mk K p (n + 1, 0)) 0
Tactic: induction n with
  | zero => rfl
  | succ n ih =>
    rw [← ih]
    apply (Quot.sound _).symm
    have := R.intro (p := p) n (0 : K)
    rwa [map_zero] at this
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
m n : ℕ
x y : K
H : (⇑(frobenius K p) : (a : K) → K)^[m] x = y
⊢ Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + n, y))
have subst : Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x))
Tactic: subst H
Cleared hypotheses: y, 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
n : ℕ
x : K
m : ℕ
ih : Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x))
⊢ Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + 1 + n, (⇑(frobenius K p) : (a : K) → K)^[m + 1] x))
have succ : Eq (α := PerfectClosure K p) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x))
  (mk K p ((m + n).succ, ((⇑(frobenius K p) : (a : K) → K) ∘ (⇑(frobenius K p) : (a : K) → K)^[m]) x))
Tactic: rw [ih, Nat.succ_add, iterate_succ']
-- 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 : K
m : ℕ
ih : Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x))
⊢ Eq (α := PerfectClosure K p) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x))
    (mk K p ((m + n).succ, ((⇑(frobenius K p) : (a : K) → K) ∘ (⇑(frobenius K p) : (a : K) → K)^[m]) x))
have succ : R K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x)
  ((m + n).succ, ((⇑(frobenius K p) : (a : K) → K) ∘ (⇑(frobenius K p) : (a : K) → K)^[m]) x)
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
m n : ℕ
x : K
⊢ Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x))
have zero : Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (0 + n, (⇑(frobenius K p) : (a : K) → K)^[0] x))
Tactic: induction m with
  | zero => simp only [zero_add, iterate_zero_apply]
  | succ m ih =>
    rw [ih, Nat.succ_add, iterate_succ']
    apply Quot.sound
    apply R.intro
Cleared hypotheses: m
-- 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
m n : ℕ
x : K
zero : Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (0 + n, (⇑(frobenius K p) : (a : K) → K)^[0] x))
⊢ Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x))
have succ : ∀ (m : ℕ) (ih : Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] x))),
  Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + 1 + n, (⇑(frobenius K p) : (a : K) → K)^[m + 1] x))
Tactic: induction m with
  | zero => simp only [zero_add, iterate_zero_apply]
  | succ m ih =>
    rw [ih, Nat.succ_add, iterate_succ']
    apply Quot.sound
    apply R.intro
Cleared hypotheses: m
-- 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
e f g : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
x_2 : ℕ × K
n : ℕ
y : K
x_3 : ℕ × 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))
have apply : (((m, x).1 + (n, y).1,
          (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (m, x).2 +
            (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (n, y).2).1 +
      (s, z).1,
    (⇑(frobenius K p) : (a : K) → K)^[(s, z).1]
        ((m, x).1 + (n, y).1,
            (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (m, x).2 +
              (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (n, y).2).2 +
      (⇑(frobenius K p) :
            (a : K) →
              K)^[((m, x).1 + (n, y).1,
              (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (m, x).2 +
                (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (n, y).2).1]
        (s, z).2) =
  ((m, x).1 +
      ((n, y).1 + (s, z).1,
          (⇑(frobenius K p) : (a : K) → K)^[(s, z).1] (n, y).2 +
            (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (s, z).2).1,
    (⇑(frobenius K p) :
            (a : K) →
              K)^[((n, y).1 + (s, z).1,
              (⇑(frobenius K p) : (a : K) → K)^[(s, z).1] (n, y).2 +
                (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (s, z).2).1]
        (m, x).2 +
      (⇑(frobenius K p) : (a : K) → K)^[(m, x).1]
        ((n, y).1 + (s, z).1,
            (⇑(frobenius K p) : (a : K) → K)^[(s, z).1] (n, y).2 +
              (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (s, z).2).2)
Tactic: apply congr_arg (Quot.mk _)
-- 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
a : PerfectClosure K p
⊢ 0 * a = 0
have refine : ∀ (x : ℕ × K) (m : ℕ) (x : K), 0 * Quot.mk (R K p) (m, x) = 0
Tactic: refine Quot.inductionOn a fun ⟨m, 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
a : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
⊢ 0 * Quot.mk (R K p) (m, x) = 0
have rw : Eq (α := PerfectClosure K p)
  (mk K p
    ((0, 0).1 + (m, x).1,
      (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2 * (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2))
  (mk K p (0, 0))
Tactic: rw [zero_def, quot_mk_eq_mk, mk_mul_mk]
-- 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
a : PerfectClosure K p
⊢ a * 0 = 0
have refine : ∀ (x : ℕ × K) (m : ℕ) (x : K), Quot.mk (R K p) (m, x) * 0 = 0
Tactic: refine Quot.inductionOn a fun ⟨m, 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
a : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
⊢ Quot.mk (R K p) (m, x) * 0 = 0
have rw : Eq (α := PerfectClosure K p)
  (mk K p
    ((m, x).1 + (0, 0).1,
      (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 * (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2))
  (mk K p (0, 0))
Tactic: rw [zero_def, quot_mk_eq_mk, mk_mul_mk]
-- 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
e f g : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
x_2 : ℕ × K
n : ℕ
y : K
x_3 : ℕ × 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)
have simp : Eq (α := PerfectClosure K p)
  (mk K p
    (m + (n + s),
      (⇑(frobenius K p) : (a : K) → K)^[n + s] x *
        (⇑(frobenius K p) : (a : K) → K)^[m]
          ((⇑(frobenius K p) : (a : K) → K)^[n] z + (⇑(frobenius K p) : (a : K) → K)^[s] y)))
  (mk K p
    (m + (m + (n + s)),
      (⇑(frobenius K p) : (a : K) → K)^[m + n]
          ((⇑(frobenius K p) : (a : K) → K)^[s] x * (⇑(frobenius K p) : (a : K) → K)^[m] z) +
        (⇑(frobenius K p) : (a : K) → K)^[m + s]
          ((⇑(frobenius K p) : (a : K) → K)^[n] x * (⇑(frobenius K p) : (a : K) → K)^[m] y)))
Tactic: simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk, add_comm, add_left_comm]
-- 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
e f g : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
x_2 : ℕ × K
n : ℕ
y : K
x_3 : ℕ × K
s : ℕ
z : K
⊢ Eq (α := PerfectClosure K p)
    (mk K p
      (m + (n + s),
        (⇑(frobenius K p) : (a : K) → K)^[n + s] x *
          (⇑(frobenius K p) : (a : K) → K)^[m]
            ((⇑(frobenius K p) : (a : K) → K)^[n] z + (⇑(frobenius K p) : (a : K) → K)^[s] y)))
    (mk K p
      (m + (m + (n + s)),
        (⇑(frobenius K p) : (a : K) → K)^[m + n]
            ((⇑(frobenius K p) : (a : K) → K)^[s] x * (⇑(frobenius K p) : (a : K) → K)^[m] z) +
          (⇑(frobenius K p) : (a : K) → K)^[m + s]
            ((⇑(frobenius K p) : (a : K) → K)^[n] x * (⇑(frobenius K p) : (a : K) → K)^[m] y)))
have H : (⇑(frobenius K p) : (a : K) → K)^[m]
    ((⇑(frobenius K p) : (a : K) → K)^[n + s] x *
      (⇑(frobenius K p) : (a : K) → K)^[m]
        ((⇑(frobenius K p) : (a : K) → K)^[n] z + (⇑(frobenius K p) : (a : K) → K)^[s] y)) =
  (⇑(frobenius K p) : (a : K) → K)^[m + n]
      ((⇑(frobenius K p) : (a : K) → K)^[s] x * (⇑(frobenius K p) : (a : K) → K)^[m] z) +
    (⇑(frobenius K p) : (a : K) → K)^[m + s]
      ((⇑(frobenius K p) : (a : K) → K)^[n] x * (⇑(frobenius K p) : (a : K) → K)^[m] y)
Tactic: apply R.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
e f g : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
x_2 : ℕ × K
n : ℕ
y : K
x_3 : ℕ × 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)
have simp : Eq (α := PerfectClosure K p)
  (mk K p
    (s + (m + n),
      (⇑(frobenius K p) : (a : K) → K)^[s]
          ((⇑(frobenius K p) : (a : K) → K)^[n] x + (⇑(frobenius K p) : (a : K) → K)^[m] y) *
        (⇑(frobenius K p) : (a : K) → K)^[m + n] z))
  (mk K p
    (s + (s + (m + n)),
      (⇑(frobenius K p) : (a : K) → K)^[s + n]
          ((⇑(frobenius K p) : (a : K) → K)^[s] x * (⇑(frobenius K p) : (a : K) → K)^[m] z) +
        (⇑(frobenius K p) : (a : K) → K)^[s + m]
          ((⇑(frobenius K p) : (a : K) → K)^[s] y * (⇑(frobenius K p) : (a : K) → K)^[n] z)))
Tactic: simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk, add_assoc, add_comm _ s,
              add_left_comm _ s]