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
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))
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))
⊢ 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:
rw [ih, Nat.succ_add, iterate_succ']

Premises used: Function.iterate_succ', Nat.succ_add
-- 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 : 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))
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)
⊢ 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:
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
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))
⊢ 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 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
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))
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))
⊢ Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (m + n, (⇑(frobenius K p) : (a : K) → K)^[m] 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

Premises used: Quot.sound, PerfectClosure.R.intro, Function.iterate_succ', zero_add, Nat.succ_add, Function.iterate_zero_apply
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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)
⊢ 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))

Tactic:
apply congr_arg (Quot.mk _)

Premises used: congr_arg, Quot.mk
-- Module: Mathlib.FieldTheory.PerfectClosure
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
⊢ (((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:
simp only [iterate_map_add, ← iterate_add_apply, add_assoc, add_comm s _]

Premises used: Function.iterate_add_apply, add_assoc, iterate_map_add, 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
e : PerfectClosure K p
x_1 : ℕ × K
n : ℕ
x : K
⊢ ((0, 0).1 + (n, x).1,
      (⇑(frobenius K p) : (a : K) → K)^[(n, x).1] (0, 0).2 + (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (n, x).2) =
    (n, x)

Tactic:
simp only [iterate_map_zero, iterate_zero_apply, zero_add]

Premises used: zero_add, iterate_map_zero, Function.iterate_zero_apply
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
n : ℕ
x : K
⊢ ((n, x).1 + (0, 0).1,
      (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (n, x).2 + (⇑(frobenius K p) : (a : K) → K)^[(n, x).1] (0, 0).2) =
    (n, x)

Tactic:
simp only [iterate_map_zero, iterate_zero_apply, add_zero]

Premises used: iterate_map_zero, Function.iterate_zero_apply, add_zero
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
n : ℕ
x : K
⊢ -Quot.mk (R K p) (n, x) + Quot.mk (R K p) (n, x) = 0

Tactic:
simp only [quot_mk_eq_mk, neg_mk, mk_add_mk, iterate_map_neg, neg_add_cancel, mk_zero_right]

Premises used: PerfectClosure.quot_mk_eq_mk, PerfectClosure.mk_add_mk, PerfectClosure.neg_mk, PerfectClosure.mk_zero_right, iterate_map_neg, neg_add_cancel
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e f : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
x_2 : ℕ × K
n : ℕ
y : 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) =
    ((n, y).1 + (m, x).1,
      (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (n, y).2 + (⇑(frobenius K p) : (a : K) → K)^[(n, y).1] (m, x).2)

Tactic:
simp only [add_comm]

Premises used: 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
a : PerfectClosure K p
⊢ 0 * a = 0

Tactic:
Quot.inductionOn a fun ⟨m, x⟩ => ?_

Premises used: Quot.inductionOn
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
a : PerfectClosure K p
refine : ∀ (x : ℕ × K) (m : ℕ) (x : K), 0 * Quot.mk (R K p) (m, x) = 0
⊢ 0 * a = 0

Tactic:
refine Quot.inductionOn a fun ⟨m, 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 : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
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))
⊢ 0 * Quot.mk (R K p) (m, x) = 0

Tactic:
rw [zero_def, quot_mk_eq_mk, mk_mul_mk]

Premises used: PerfectClosure.mk_mul_mk, PerfectClosure.quot_mk_eq_mk, PerfectClosure.zero_def
-- Module: Mathlib.FieldTheory.PerfectClosure
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
⊢ 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:
simp only [zero_add, iterate_zero, id_eq, iterate_map_zero, zero_mul, mk_zero_right]

Premises used: Function.iterate_zero, MulZeroClass.zero_mul, zero_add, PerfectClosure.mk_zero_right, iterate_map_zero, id_eq
-- Module: Mathlib.FieldTheory.PerfectClosure
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

Tactic:
Quot.inductionOn a fun ⟨m, x⟩ => ?_

Premises used: Quot.inductionOn
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
a : PerfectClosure K p
refine : ∀ (x : ℕ × K) (m : ℕ) (x : K), Quot.mk (R K p) (m, x) * 0 = 0
⊢ a * 0 = 0

Tactic:
refine Quot.inductionOn a fun ⟨m, 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 : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
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))
⊢ Quot.mk (R K p) (m, x) * 0 = 0

Tactic:
rw [zero_def, quot_mk_eq_mk, mk_mul_mk]

Premises used: PerfectClosure.mk_mul_mk, PerfectClosure.quot_mk_eq_mk, PerfectClosure.zero_def
-- Module: Mathlib.FieldTheory.PerfectClosure
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
⊢ 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:
simp only [iterate_zero, id_eq, iterate_map_zero, mul_zero, mk_zero_right]

Premises used: Function.iterate_zero, PerfectClosure.mk_zero_right, MulZeroClass.mul_zero, iterate_map_zero, id_eq
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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)))
⊢ 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)

Tactic:
simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk, add_comm, add_left_comm]

Premises used: PerfectClosure.mk_mul_mk, PerfectClosure.quot_mk_eq_mk, add_left_comm, PerfectClosure.mk_add_mk, 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
e f g : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
x_2 : ℕ × K
n : ℕ
y : K
x_3 : ℕ × K
s : ℕ
z : K
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)
⊢ 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:
apply R.sound

Premises used: PerfectClosure.R.sound
-- Module: Mathlib.FieldTheory.PerfectClosure
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
⊢ (⇑(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:
simp only [iterate_map_mul, iterate_map_add, ← iterate_add_apply,
              mul_add, add_comm, add_left_comm]

Premises used: Function.iterate_add_apply, add_left_comm, iterate_map_add, add_comm, iterate_map_mul, mul_add
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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)))
⊢ (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)

Tactic:
simp only [quot_mk_eq_mk, mk_add_mk, mk_mul_mk, add_assoc, add_comm _ s,
              add_left_comm _ s]

Premises used: PerfectClosure.mk_mul_mk, PerfectClosure.quot_mk_eq_mk, add_left_comm, add_assoc, PerfectClosure.mk_add_mk, 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
e f g : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
x_2 : ℕ × K
n : ℕ
y : K
x_3 : ℕ × K
s : ℕ
z : K
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)
⊢ 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:
apply R.sound

Premises used: PerfectClosure.R.sound
-- Module: Mathlib.FieldTheory.PerfectClosure
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
⊢ (⇑(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:
simp only [iterate_map_mul, iterate_map_add, ← iterate_add_apply,
              add_mul, add_comm, add_left_comm]

Premises used: add_mul, Function.iterate_add_apply, add_left_comm, iterate_map_add, add_comm, iterate_map_mul
-- 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
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
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)
⊢ 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
-- 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 : Eq (α := PerfectClosure K p) (mk K p x) (mk K p y)
⊢ Relation.EqvGen (R K p) x y

Tactic:
replace H := Quot.eqvGen_exact 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_1 y_1 x y : ℕ × K
H : R K p x y
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
⊢ ∃ (z : ℕ), (⇑(frobenius K p) : (a : K) → K)^[y.1 + z] x.2 = (⇑(frobenius K p) : (a : K) → K)^[x.1 + z] y.2

Tactic:
obtain ⟨n, x⟩ := 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_1 y : ℕ × K
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:
⟨0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- 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 : ℕ × K
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:
exact ⟨0, rfl⟩
-- 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 : ℕ × 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:
⟨0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- 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 : ℕ × 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:
exact ⟨0, rfl⟩
-- 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 : ℕ × 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
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
⊢ ∃ (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
-- 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 : ℕ × K
H : Relation.EqvGen (R K p) x y
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:
⟨w, ih.symm⟩

Premises used: Exists.intro, Eq.symm
-- 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 : ℕ × K
H : Relation.EqvGen (R K p) x y
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:
exact ⟨w, ih.symm⟩
-- 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
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
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
⊢ ∃ (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