awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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
⊢ ∃ (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
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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
⊢ ∃ (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:
exists z2 + (y.1 + z1)

Premises used: Prod.fst, HAdd.hAdd
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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
⊢ (⇑(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:
rw [← add_assoc, iterate_add_apply, ih1]

Premises used: Function.iterate_add_apply, add_assoc
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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
⊢ (⇑(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 [← iterate_add_apply, add_comm, iterate_add_apply, ih2]

Premises used: Function.iterate_add_apply, add_comm
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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
⊢ (⇑(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]

Premises used: Function.iterate_add_apply
-- Module: Mathlib.FieldTheory.PerfectClosure
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 + (y.1 + z2)] z.2 =
    (⇑(frobenius K p) : (a : K) → K)^[x.1 + (z2 + (y.1 + z1))] z.2

Tactic:
simp only [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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
⊢ ∃ (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]

Premises used: Function.iterate_add_apply, add_left_comm, add_assoc, add_comm, symm, refl
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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)
⊢ Eq (α := PerfectClosure K p) (mk K p x) (mk K p y)

Tactic:
obtain ⟨m, x⟩ := x
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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))
⊢ Eq (α := PerfectClosure K p) (mk K p (m, x)) (mk K p y)

Tactic:
obtain ⟨n, y⟩ := y
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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))
⊢ Eq (α := PerfectClosure K p) (mk K p (m, x)) (mk K p (n, y))

Tactic:
obtain ⟨z, H⟩ := H
-- Module: Mathlib.FieldTheory.PerfectClosure
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 (m, x)) (mk K p (n, y))

Tactic:
rw [R.sound K p (n + z) m x _ rfl, R.sound K p (m + z) n y _ rfl, H]

Premises used: HAdd.hAdd, PerfectClosure.R.sound, rfl
-- Module: Mathlib.FieldTheory.PerfectClosure
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))
mpr₂ 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))
⊢ 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]

Premises used: add_assoc, add_comm
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
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)
⊢ HPow.hPow (α := PerfectClosure K p) (β := ℕ) (mk K p x) 0 = mk K p (x.1, HPow.hPow (β := ℕ) x.2 0)

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

Premises used: pow_zero, PerfectClosure.mk_eq_iff, PerfectClosure.one_def
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
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)
⊢ 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)

Tactic:
simp_rw [← coe_iterateFrobenius, map_one]

Premises used: coe_iterateFrobenius, map_one
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
⊢ ∃ (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:
exact ⟨0, by simp_rw [← coe_iterateFrobenius, map_one]⟩
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
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
⊢ HPow.hPow (α := PerfectClosure K p) (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]

Premises used: PerfectClosure.mk_mul_mk, pow_succ, PerfectClosure.mk_eq_iff
-- Module: Mathlib.FieldTheory.PerfectClosure
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))
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

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

Premises used: mul_assoc, pow_add, pow_mul, iterate_frobenius, add_zero, mul_pow
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
⊢ ∃ (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:
exact ⟨0, by simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]⟩
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
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))
⊢ HPow.hPow (α := PerfectClosure K p) (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]⟩

Premises used: PerfectClosure.mk_mul_mk, pow_succ, pow_zero, PerfectClosure.mk_eq_iff, PerfectClosure.one_def
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
⊢ Eq (α := PerfectClosure K p) (↑0 : PerfectClosure K p) (mk K p (0, (↑0 : K)))

Tactic:
simp
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
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:
simp [Nat.cast_succ, ih, one_def]

Premises used: Nat.cast_succ, PerfectClosure.one_def
-- Module: Mathlib.FieldTheory.PerfectClosure
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)))
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)))
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))

Tactic:
induction x with
    | zero => simp
    | succ x ih => simp [Nat.cast_succ, ih, one_def]

Premises used: Nat.cast_succ, PerfectClosure.one_def
-- Module: Mathlib.FieldTheory.PerfectClosure
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)))
succ : Eq (α := PerfectClosure K p) (mk K p (n, (↑x : K))) (mk K p (n + 1, (↑x : K)))
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n + 1, (↑x : K)))

Tactic:
rw [ih]
-- Module: Mathlib.FieldTheory.PerfectClosure
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)))
succ : R K p (n, (↑x : K)) (n + 1, (↑x : K))
⊢ Eq (α := PerfectClosure K p) (mk K p (n, (↑x : K))) (mk K p (n + 1, (↑x : K)))

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : R K p (n, (↑x : K)) (n.succ, (↑x : K))), R K p (n, (↑x : K)) (n + 1, (↑x : K))
⊢ R K p (n, (↑x : K)) (n + 1, (↑x : K))

Tactic:
rwa [map_natCast] at this

Premises used: map_natCast
-- Module: Mathlib.FieldTheory.PerfectClosure
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)))
succ : 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))

Tactic:
suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by
      rwa [map_natCast] at this
-- Module: Mathlib.FieldTheory.PerfectClosure
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)) : ℕ × K) ((n.succ, (frobenius K p : (a : K) → K) (↑x : K)) : ℕ × K)

Tactic:
apply R.intro

Premises used: PerfectClosure.R.intro
-- Module: Mathlib.FieldTheory.PerfectClosure
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)))
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)))
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (n, (↑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

Premises used: Nat.cast_succ, Quot.sound, PerfectClosure.R.intro, PerfectClosure.one_def
-- Module: Mathlib.FieldTheory.PerfectClosure
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)))
negSucc :
  ∀ (a : ℕ), Eq (α := PerfectClosure K p) (↑(Int.negSucc a) : PerfectClosure K p) (mk K p (0, (↑(Int.negSucc a) : K)))
⊢ Eq (α := PerfectClosure K p) (↑x : PerfectClosure K p) (mk K p (0, (↑x : K)))

Tactic:
cases x
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
a : ℕ
⊢ Eq (α := PerfectClosure K p) (↑(Int.ofNat a) : PerfectClosure K p) (mk K p (0, (↑(Int.ofNat a) : K)))

Tactic:
simp [natCast K p 0]

Premises used: OfNat.ofNat, PerfectClosure.natCast
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
a : ℕ
⊢ Eq (α := PerfectClosure K p) (↑(Int.negSucc a) : PerfectClosure K p) (mk K p (0, (↑(Int.negSucc a) : K)))

Tactic:
simp [natCast K p 0]

Premises used: OfNat.ofNat, PerfectClosure.natCast
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
mpr :
  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} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p) ↔
    Eq.{u + 1} (α := K) (↑x : K) (↑y : K)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
⊢ ∃ (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

Premises used: PerfectClosure.mk_eq_iff, OfNat.ofNat, PerfectClosure.natCast
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
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)
⊢ Eq.{u + 1} (α := K) (↑x : K) (↑y : K)

Tactic:
obtain ⟨z, H⟩ := H
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y 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:
simpa only [zero_add, iterate_fixed (map_natCast _ _)] using H

Premises used: zero_add, map_natCast, Function.iterate_fixed