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
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
      (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)))
have H : (⇑(frobenius K p) : (a : K) → K)^[s]
    ((⇑(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) =
  (⇑(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: 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
x y : ℕ × K
⊢ Eq (α := PerfectClosure K p) (mk K p x) (mk K p y) ↔
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
have mp : Eq (α := PerfectClosure K p) (mk K p x) (mk K p y) →
  ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
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 : ℕ × K
mp :
  Eq (α := PerfectClosure K p) (mk K p x) (mk K p y) →
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
⊢ Eq (α := PerfectClosure K p) (mk K p x) (mk K p y) ↔
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
have mpr : (∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2) →
  Eq (α := PerfectClosure K p) (mk K p x) (mk K p y)
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 : ℕ × K
H : Eq (α := PerfectClosure K p) (mk K p x) (mk K p y)
⊢ ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
have H₁ : Relation.EqvGen (R K p) x y
Tactic: replace H := Quot.eqvGen_exact 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_1 y_1 x y : ℕ × K
H : R K p x y
⊢ ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
have mp : ∀ (n : ℕ) (x : K),
  ∃ (z : ℕ),
    (⇑(frobenius K p) : (a : K) → K)^[((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1 + z] (n, x).2 =
      (⇑(frobenius K p) : (a : K) → K)^[(n, x).1 + z] (n + 1, (frobenius K p : (a : K) → K) x).2
Tactic: obtain ⟨n, x⟩ := H
Cleared hypotheses: x, 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
x_1 y_1 x y : ℕ × K
H : Relation.EqvGen (R K p) x y
ih : ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
⊢ ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2
have mp : ∀ (w : ℕ) (ih : (⇑(frobenius K p) : (a : K) → K)^[y.1 + w] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + w] y.2),
  ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2
Tactic: obtain ⟨w, ih⟩ := ih
Cleared hypotheses: 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_1 y_1 x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
ih1 : ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
ih2 : ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z_1] z.2
⊢ ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z_1] z.2
have mp : ∀ (z1 : ℕ) (ih1 : (⇑(frobenius K p) : (a : K) → K)^[y.1 + z1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] y.2),
  ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z_1] z.2
Tactic: obtain ⟨z1, ih1⟩ := ih1
Cleared hypotheses: ih1
-- 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_1 x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
ih2 : ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z_1] z.2
z1 : ℕ
ih1 : (⇑(frobenius K p) : (a : K) → K)^[y.1 + z1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] y.2
⊢ ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z_1] z.2
have mp : ∀ (z2 : ℕ) (ih2 : (⇑(frobenius K p) : (a : K) → K)^[z.1 + z2] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z2] z.2),
  ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z_1] z.2
Tactic: obtain ⟨z2, ih2⟩ := ih2
Cleared hypotheses: ih2
-- 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_1 x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p) : (a : K) → K)^[y.1 + z1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p) : (a : K) → K)^[z.1 + z2] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z2] z.2
⊢ ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z_1] z.2
have mp : (⇑(frobenius K p) : (a : K) → K)^[z.1 + (z2 + (y.1 + z1))] x.2 =
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + (z2 + (y.1 + z1))] z.2
Tactic: exists z2 + (y.1 + z1)
-- 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_1 x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p) : (a : K) → K)^[y.1 + z1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p) : (a : K) → K)^[z.1 + z2] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z2] z.2
⊢ (⇑(frobenius K p) : (a : K) → K)^[z.1 + (z2 + (y.1 + z1))] x.2 =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + (z2 + (y.1 + z1))] z.2
have mp : (⇑(frobenius K p) : (a : K) → K)^[z.1 + z2] ((⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] y.2) =
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + (z2 + (y.1 + z1))] z.2
Tactic: rw [← add_assoc, iterate_add_apply, ih1]
-- 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_1 x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p) : (a : K) → K)^[y.1 + z1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p) : (a : K) → K)^[z.1 + z2] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z2] z.2
⊢ (⇑(frobenius K p) : (a : K) → K)^[z.1 + z2] ((⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] y.2) =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + (z2 + (y.1 + z1))] z.2
have mp : (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] ((⇑(frobenius K p) : (a : K) → K)^[y.1 + z2] z.2) =
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + (z2 + (y.1 + z1))] z.2
Tactic: rw [← iterate_add_apply, add_comm, iterate_add_apply, ih2]
-- 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_1 x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p) : (a : K) → K)^[y.1 + z1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p) : (a : K) → K)^[z.1 + z2] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z2] z.2
⊢ (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1] ((⇑(frobenius K p) : (a : K) → K)^[y.1 + z2] z.2) =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + (z2 + (y.1 + z1))] z.2
have mp : (⇑(frobenius K p) : (a : K) → K)^[x.1 + z1 + (y.1 + z2)] z.2 =
  (⇑(frobenius K p) : (a : K) → K)^[x.1 + (z2 + (y.1 + z1))] z.2
Tactic: rw [← iterate_add_apply]
-- 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 : ℕ × K
H : Relation.EqvGen (R K p) x y
⊢ ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
have mp : ∀ (x y : ℕ × K) (H : R K p x y),
  ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
Tactic: induction H with
    | rel x y H => obtain ⟨n, x⟩ := H; exact ⟨0, rfl⟩
    | refl H => exact ⟨0, rfl⟩
    | symm x y H ih => obtain ⟨w, ih⟩ := ih; exact ⟨w, ih.symm⟩
    | trans x y z H1 H2 ih1 ih2 =>
      obtain ⟨z1, ih1⟩ := ih1
      obtain ⟨z2, ih2⟩ := 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]
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 : ℕ × K
H : Relation.EqvGen (R K p) x y
mp :
  ∀ (x y : ℕ × K) (H : R K p x y),
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
⊢ ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
have mp₁ : ∀ (H : ℕ × K),
  ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[H.1 + z] H.2 = (⇑(frobenius K p) : (a : K) → K)^[H.1 + z] H.2
Tactic: induction H with
    | rel x y H => obtain ⟨n, x⟩ := H; exact ⟨0, rfl⟩
    | refl H => exact ⟨0, rfl⟩
    | symm x y H ih => obtain ⟨w, ih⟩ := ih; exact ⟨w, ih.symm⟩
    | trans x y z H1 H2 ih1 ih2 =>
      obtain ⟨z1, ih1⟩ := ih1
      obtain ⟨z2, ih2⟩ := 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]
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 : ℕ × K
H : Relation.EqvGen (R K p) x y
mp :
  ∀ (x y : ℕ × K) (H : R K p x y),
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
mp₁ :
  ∀ (H : ℕ × K),
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[H.1 + z] H.2 = (⇑(frobenius K p) : (a : K) → K)^[H.1 + z] H.2
⊢ ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
have mp₂ : ∀ (x y : ℕ × K) (H : Relation.EqvGen (R K p) x y)
  (ih : ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2),
  ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2
Tactic: induction H with
    | rel x y H => obtain ⟨n, x⟩ := H; exact ⟨0, rfl⟩
    | refl H => exact ⟨0, rfl⟩
    | symm x y H ih => obtain ⟨w, ih⟩ := ih; exact ⟨w, ih.symm⟩
    | trans x y z H1 H2 ih1 ih2 =>
      obtain ⟨z1, ih1⟩ := ih1
      obtain ⟨z2, ih2⟩ := 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]
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 : ℕ × K
H : Relation.EqvGen (R K p) x y
mp :
  ∀ (x y : ℕ × K) (H : R K p x y),
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
mp₁ :
  ∀ (H : ℕ × K),
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[H.1 + z] H.2 = (⇑(frobenius K p) : (a : K) → K)^[H.1 + z] H.2
mp₂ :
  ∀ (x y : ℕ × K) (H : Relation.EqvGen (R K p) x y)
    (ih : ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2),
    ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2
⊢ ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
have mp₃ : ∀ (x y z : ℕ × K) (H1 : Relation.EqvGen (R K p) x y) (H2 : Relation.EqvGen (R K p) y z)
  (ih1 : ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2)
  (ih2 :
    ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] y.2 = (⇑(frobenius K p) : (a : K) → K)^[y.1 + z_1] z.2),
  ∃ (z_1 : ℕ), (⇑(frobenius K p) : (a : K) → K)^[z.1 + z_1] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z_1] z.2
Tactic: induction H with
    | rel x y H => obtain ⟨n, x⟩ := H; exact ⟨0, rfl⟩
    | refl H => exact ⟨0, rfl⟩
    | symm x y H ih => obtain ⟨w, ih⟩ := ih; exact ⟨w, ih.symm⟩
    | trans x y z H1 H2 ih1 ih2 =>
      obtain ⟨z1, ih1⟩ := ih1
      obtain ⟨z2, ih2⟩ := 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]
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 : ℕ × K
H : ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2
⊢ Eq (α := PerfectClosure K p) (mk K p x) (mk K p y)
have mpr : ∀ (m : ℕ) (x : K)
  (H :
    ∃ (z : ℕ),
      (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1 + z] y.2),
  Eq (α := PerfectClosure K p) (mk K p (m, x)) (mk K p y)
Tactic: obtain ⟨m, x⟩ := x
Cleared hypotheses: x, 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
y : ℕ × K
m : ℕ
x : K
H : ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1 + z] y.2
⊢ Eq (α := PerfectClosure K p) (mk K p (m, x)) (mk K p y)
have mpr : ∀ (n : ℕ) (y : K)
  (H :
    ∃ (z : ℕ),
      (⇑(frobenius K p) : (a : K) → K)^[(n, y).1 + z] (m, x).2 =
        (⇑(frobenius K p) : (a : K) → K)^[(m, x).1 + z] (n, y).2),
  Eq (α := PerfectClosure K p) (mk K p (m, x)) (mk K p (n, y))
Tactic: obtain ⟨n, y⟩ := y
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
m : ℕ
x : K
n : ℕ
y : K
H :
  ∃ (z : ℕ),
    (⇑(frobenius K p) : (a : K) → K)^[(n, y).1 + z] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1 + z] (n, y).2
⊢ Eq (α := PerfectClosure K p) (mk K p (m, x)) (mk K p (n, y))
have mpr : ∀ (z : ℕ)
  (H :
    (⇑(frobenius K p) : (a : K) → K)^[(n, y).1 + z] (m, x).2 =
      (⇑(frobenius K p) : (a : K) → K)^[(m, x).1 + z] (n, y).2),
  Eq (α := PerfectClosure K p) (mk K p (m, x)) (mk K p (n, y))
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
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p) : (a : K) → K)^[n + z] x = (⇑(frobenius K p) : (a : K) → K)^[m + z] y
⊢ Eq (α := PerfectClosure K p) (mk K p (m, x)) (mk K p (n, y))
have mpr : Eq (α := PerfectClosure K p) (mk K p (n + z + m, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
  (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
Tactic: rw [R.sound K p (n + z) m x _ rfl, R.sound K p (m + z) n y _ rfl, 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
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p) : (a : K) → K)^[n + z] x = (⇑(frobenius K p) : (a : K) → K)^[m + z] y
⊢ Eq (α := PerfectClosure K p) (mk K p (n + z + m, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
    (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
have mpr : Eq (α := PerfectClosure K p) (mk K p (n + (z + m), (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
  (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
Tactic: rw [add_assoc, add_comm, add_comm z]
-- 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 : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p) : (a : K) → K)^[n + z] x = (⇑(frobenius K p) : (a : K) → K)^[m + z] y
mpr :
  Eq (α := PerfectClosure K p) (mk K p (n + (z + m), (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
    (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
⊢ Eq (α := PerfectClosure K p) (mk K p (n + z + m, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
    (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
have mpr₁ : Eq (α := PerfectClosure K p) (mk K p (z + m + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
  (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
Tactic: rw [add_assoc, add_comm, add_comm z]
-- 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 : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p) : (a : K) → K)^[n + z] x = (⇑(frobenius K p) : (a : K) → K)^[m + z] y
mpr :
  Eq (α := PerfectClosure K p) (mk K p (n + (z + m), (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
    (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
mpr₁ :
  Eq (α := PerfectClosure K p) (mk K p (z + m + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
    (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
⊢ Eq (α := PerfectClosure K p) (mk K p (n + z + m, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
    (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
have mpr₂ : Eq (α := PerfectClosure K p) (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
  (mk K p (m + z + n, (⇑(frobenius K p) : (a : K) → K)^[m + z] y))
Tactic: rw [add_assoc, add_comm, add_comm z]
-- 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
⊢ HPow.hPow (α := PerfectClosure K p) (β := ℕ) (mk K p x) 0 = mk K p (x.1, HPow.hPow (β := ℕ) x.2 0)
have zero : ∃ (z : ℕ),
  Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[(x.1, 1).1 + z] (0, 1).2)
    ((⇑(frobenius K p) : (a : K) → K)^[(0, 1).1 + z] (x.1, 1).2)
Tactic: rw [pow_zero, pow_zero, one_def, mk_eq_iff]
-- 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
⊢ Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[(x.1, 1).1 + 0] (0, 1).2)
    ((⇑(frobenius K p) : (a : K) → K)^[HAdd.hAdd (α := ℕ) (0, 1).1 0] (x.1, 1).2)
have simp_rw : Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[x.1 + 0] 1) ((⇑(frobenius K p) : (a : K) → K)^[HAdd.hAdd (α := ℕ) 0 0] 1)
Tactic: simp_rw [← coe_iterateFrobenius, map_one]
-- 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
simp_rw simp_rw₁ :
  Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[x.1 + 0] 1)
    ((⇑(frobenius K p) : (a : K) → K)^[HAdd.hAdd (α := ℕ) 0 0] 1)
⊢ Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[(x.1, 1).1 + 0] (0, 1).2)
    ((⇑(frobenius K p) : (a : K) → K)^[HAdd.hAdd (α := ℕ) (0, 1).1 0] (x.1, 1).2)
have simp_rw₂ : Eq (α := K) ((iterateFrobenius K p (x.1 + 0) : (a : K) → K) 1 : K)
  ((iterateFrobenius K p (HAdd.hAdd (α := ℕ) 0 0) : (a : K) → K) 1 : K)
Tactic: simp_rw [← coe_iterateFrobenius, map_one]
-- 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)
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) (n + 1) = mk K p (x.1, x.2 ^ (n + 1))
have succ : ∃ (z : ℕ),
  (⇑(frobenius K p) : (a : K) → K)^[(x.1, x.2 ^ n * x.2).1 + z]
      ((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 +
          z]
      (x.1, x.2 ^ n * x.2).2
Tactic: rw [pow_succ, pow_succ, ih, mk_mul_mk, mk_eq_iff]
-- 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)
⊢ (⇑(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 : (⇑(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)
Tactic: simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]