awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Perfect
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
rw₂ rw₃ : 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

Tactic:
rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
    (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']

Premises used: Polynomial.roots, Finset.image_toFinset, Multiset.toFinset_nsmul, LT.lt.ne', Polynomial.roots_expand_pow_map_iterateFrobenius, expChar_pow_pos
-- Module: Mathlib.FieldTheory.Perfect
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
rw₂ rw₃ : 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

Tactic:
rw [Finset.image_toFinset, roots_expand_map_frobenius,
      (roots f).toFinset_nsmul _ (expChar_pos R p).ne']

Premises used: Polynomial.roots, Finset.image_toFinset, Multiset.toFinset_nsmul, Polynomial.roots_expand_map_frobenius, LT.lt.ne', expChar_pos
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : DecidableEq R
x : ↥(toFinset (roots ((expand R p : (a : R[X]) → R[X]) f)))
⊢ (↑((rootsExpandToRoots p f : (a : ↥((expand R p : (a : R[X]) → R[X]) f).roots.toFinset) → ↥f.roots.toFinset) x) : R) =
    (↑x : R) ^ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Perfect
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
x : ↥(toFinset (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))
⊢ (↑((rootsExpandPowToRoots p n f :
            (a : ↥((expand R (p ^ n) : (a : R[X]) → R[X]) f).roots.toFinset) → ↥f.roots.toFinset)
          x) :
      R) =
    (↑x : R) ^ p ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Perfect
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
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)
⊢ (⇑(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)

Tactic:
rw [← roots_expand_image_frobenius (p := p) (f := f)]

Premises used: Polynomial.roots_expand_image_frobenius
-- Module: Mathlib.FieldTheory.Perfect
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) =
    (↑(Finset.image (α := R) (⇑(frobenius R p) : (a : R) → R) (toFinset (roots ((expand R p : (a : R[X]) → R[X]) f)))) :
      Set R)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : DecidableEq R
inst_4 : PerfectRing R p
x : ↥(toFinset (roots ((expand R p : (a : R[X]) → R[X]) f)))
⊢ (↑((rootsExpandEquivRoots p f : (a : ↥((expand R p : (a : R[X]) → R[X]) f).roots.toFinset) → ↥f.roots.toFinset) x) :
      R) =
    (↑x : R) ^ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Perfect
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 : ℕ
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)
⊢ (⇑(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)

Tactic:
rw [← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := n)]

Premises used: Polynomial.roots_expand_image_iterateFrobenius
-- Module: Mathlib.FieldTheory.Perfect
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) =
    (↑(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:
simp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
inst_2 : ExpChar R p
f : R[X]
inst_3 : DecidableEq R
inst_4 : PerfectRing R p
n : ℕ
x : ↥(toFinset (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))
⊢ (↑((rootsExpandPowEquivRoots p f n :
            (a : ↥((expand R (p ^ n) : (a : R[X]) → R[X]) f).roots.toFinset) → ↥f.roots.toFinset)
          x) :
      R) =
    (↑x : R) ^ p ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
⊢ Surjective (β := PerfectClosure K p) (mk K p)

Tactic:
Quot.mk_surjective

Premises used: PerfectClosure.mk, Quot.mk_surjective, PerfectClosure
-- 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
⊢ Eq (α := PerfectClosure K p) (mk K p (m + 1, x ^ p)) (mk K p (m, x))

Tactic:
Eq.symm <| Quot.sound (R.intro m x)

Premises used: Quot.sound, PerfectClosure.R.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 : ℕ × K
⊢ Quot.mk (R K p) x = mk K p x

Tactic:
rfl

Premises used: PerfectClosure.mk, rfl
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type u_1
f : ℕ × K → L
hf : ∀ (x y : ℕ × K), R K p x y → f x = f y
x : ℕ × K
⊢ liftOn (mk K p x) f hf = f x

Tactic:
rfl

Premises used: PerfectClosure.liftOn, 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 : PerfectClosure K p
q : PerfectClosure K p → Prop
h : ∀ (x : ℕ × K), q (mk K p x)
⊢ q x

Tactic:
Quot.inductionOn x h

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
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
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))
⊢ 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))

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_mul,
        Nat.succ_add]

Premises used: Function.iterate_succ_apply', map_mul, Function.iterate_succ_apply, 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
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 + 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:
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
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
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))
⊢ 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))

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_mul]

Premises used: Function.iterate_succ_apply', map_mul, Function.iterate_succ_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 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,
      (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:
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
x y : ℕ × K
⊢ HMul.hMul (α := PerfectClosure K p) (mk K p x) (mk K p y) =
    mk K p (x.1 + y.1, (⇑(frobenius K p) : (a : K) → K)^[y.1] x.2 * (⇑(frobenius K p) : (a : K) → K)^[x.1] y.2)

Tactic:
rfl

Premises used: rfl
-- 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 [mul_assoc, iterate_map_mul, ← iterate_add_apply,
              add_comm, add_left_comm]

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

Tactic:
simp only [iterate_map_one, iterate_zero_apply, one_mul, zero_add]

Premises used: iterate_map_one, zero_add, Function.iterate_zero_apply, one_mul
-- 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, 1).1,
      (⇑(frobenius K p) : (a : K) → K)^[(0, 1).1] (n, x).2 * (⇑(frobenius K p) : (a : K) → K)^[(n, x).1] (0, 1).2) =
    (n, x)

Tactic:
simp only [iterate_map_one, iterate_zero_apply, mul_one, add_zero]

Premises used: iterate_map_one, mul_one, 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 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, mul_comm]

Premises used: add_comm, mul_comm
-- 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) 1 (mk K p (0, 1))

Tactic:
rfl

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

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_add,
        Nat.succ_add]

Premises used: Function.iterate_succ_apply', map_add, Function.iterate_succ_apply, 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
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 + 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:
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
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
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))
⊢ 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))

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_add]

Premises used: Function.iterate_succ_apply', map_add, Function.iterate_succ_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 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,
      (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:
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
x y : ℕ × K
⊢ HAdd.hAdd (α := PerfectClosure K p) (mk K p x) (mk K p y) =
    mk K p (x.1 + y.1, (⇑(frobenius K p) : (a : K) → K)^[y.1] x.2 + (⇑(frobenius K p) : (a : K) → K)^[x.1] y.2)

Tactic:
rfl

Premises used: 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
H : R K p x_1 y
n : ℕ
x : K
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))
⊢ 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)

Tactic:
rw [← map_neg]

Premises used: map_neg
-- 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
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, (frobenius K p : (a : K) → K) (-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
x : ℕ × K
⊢ Eq (α := PerfectClosure K p) (-mk K p x) (mk K p (x.1, -x.2))

Tactic:
rfl

Premises used: rfl
-- 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 (mk K p (0, 0))

Tactic:
rfl

Premises used: rfl
-- 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) (mk K p 0) 0

Tactic:
rfl

Premises used: rfl
-- 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) (mk K p (0, 0)) 0

Tactic:
rfl
-- Module: Mathlib.FieldTheory.PerfectClosure
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
succ : Eq (α := PerfectClosure K p) (mk K p (n + 1, 0)) (mk K p (n, 0))
⊢ Eq (α := PerfectClosure K p) (mk K p (n + 1, 0)) 0

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
n : ℕ
ih : Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0
apply : R K p (n, 0) (n + 1, 0)
⊢ Eq (α := PerfectClosure K p) (mk K p (n + 1, 0)) (mk K p (n, 0))

Tactic:
apply (Quot.sound _).symm

Premises used: Quot.sound, 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
n : ℕ
ih : Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0
⊢ 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)
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : R K p (n, 0) (n + 1, 0)), R K p (n, 0) (n + 1, 0)
⊢ R K p (n, 0) (n + 1, 0)

Tactic:
rwa [map_zero] at this

Premises used: map_zero
-- Module: Mathlib.FieldTheory.PerfectClosure
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
succ :
  ∀ (n : ℕ) (ih : Eq (α := PerfectClosure K p) (mk K p (n, 0)) 0), Eq (α := PerfectClosure K p) (mk K p (n + 1, 0)) 0
⊢ Eq (α := PerfectClosure K p) (mk K p (n, 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

Premises used: Quot.sound, map_zero, 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
m n : ℕ
x y : K
H : (⇑(frobenius K p) : (a : K) → K)^[m] x = y
subst : 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 + n, y))

Tactic:
subst H
-- 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
⊢ Eq (α := PerfectClosure K p) (mk K p (n, x)) (mk K p (0 + n, (⇑(frobenius K p) : (a : K) → K)^[0] x))

Tactic:
simp only [zero_add, iterate_zero_apply]

Premises used: zero_add, Function.iterate_zero_apply