awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p q : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : PerfectRing M q
⊢ Eq (α := M ≃* M) (powMulEquiv M (p * q)) (MulEquiv.trans (powMulEquiv M p) (powMulEquiv M q))

Tactic:
MulEquiv.ext fun x ↦ pow_mul x p q

Premises used: pow_mul, MulEquiv.ext
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p q : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : PerfectRing M q
⊢ Eq (α := M ≃* M) (powMulEquiv M (p * q)) (MulEquiv.trans (powMulEquiv M q) (powMulEquiv M p))

Tactic:
MulEquiv.ext fun x ↦ pow_mul' x p q

Premises used: MulEquiv.ext, pow_mul'
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
n_1 n : ℕ
ih : powMulEquiv M (p ^ n) = HPow.hPow (α := M ≃* M) (powMulEquiv M p) n
rw : Eq (α := M ≃* M) (powMulEquiv M (p ^ n.succ)) (powMulEquiv M (p * p ^ n))
⊢ powMulEquiv M (p ^ n.succ) = HPow.hPow (α := M ≃* M) (powMulEquiv M p) n.succ

Tactic:
rw [pow_succ (powMulEquiv M p), ← ih, MulAut.mul_def, ← powMulEquiv_mul]

Premises used: pow_succ, powMulEquiv_mul, MulAut.mul_def, powMulEquiv
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
n_1 n : ℕ
ih : powMulEquiv M (p ^ n) = HPow.hPow (α := M ≃* M) (powMulEquiv M p) n
e_p : p ^ n.succ = p * p ^ n
⊢ Eq (α := M ≃* M) (powMulEquiv M (p ^ n.succ)) (powMulEquiv M (p * p ^ n))

Tactic:
congr
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
n_1 n : ℕ
ih : powMulEquiv M (p ^ n) = HPow.hPow (α := M ≃* M) (powMulEquiv M p) n
e_p e_p₁ : p * p ^ n = p * p ^ n
⊢ p ^ n.succ = p * p ^ n

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
p : ℕ
inst : CommRing R
inst_1 : ExpChar R p
inst_2 : IsReduced R
h : Surjective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
⊢ PerfectRing R p

Tactic:
⟨frobenius_inj R p, h⟩

Premises used: PerfectRing.mk, And.intro, frobenius_inj
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R_1 : Type u_1
p m n : ℕ
inst : CommSemiring R_1
inst_1 : ExpChar R_1 p
R : Type u_2
inst_2 : CommRing R
inst_3 : ExpChar R p
inst_4 : Finite R
inst_5 : IsReduced R
⊢ PerfectRing R p

Tactic:
ofSurjective _ _ <| Finite.surjective_of_injective (frobenius_inj R p)

Premises used: PerfectRing.ofSurjective, Finite.surjective_of_injective, frobenius_inj
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Bijective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)

Tactic:
PerfectRing.bijective_frobenius

Premises used: PerfectRing.bijective_frobenius
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Bijective (α := R) (β := R) (⇑(iterateFrobenius R p n) : (a : R) → R)

Tactic:
PerfectRing.bijective_frobenius

Premises used: PerfectRing.bijective_frobenius
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Injective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)

Tactic:
(bijective_frobenius R p).1

Premises used: And.left, bijective_frobenius
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Surjective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)

Tactic:
(bijective_frobenius R p).2

Premises used: And.right, bijective_frobenius
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R ≃* R) (powMulEquiv R p) (RingEquiv.toMulEquiv (frobeniusEquiv R p))

Tactic:
rfl

Premises used: MulEquiv.ofBijective, Equiv.ofBijective, powMulEquiv, rfl
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := (a : R) → R) (⇑(frobeniusEquiv R p) : (a : R) → R) (⇑(frobenius R p) : (a : R) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ (frobeniusEquiv R p : (a : R) → R) x = x ^ p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := (a : R) → R) (⇑(iterateFrobeniusEquiv R p n) : (a : R) → R) (⇑(iterateFrobenius R p n) : (a : R) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p n : (a : R) → R) x = x ^ p ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ Eq (α := R) ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R) x : R)
    ((iterateFrobeniusEquiv R p m : (a : R) → R) ((iterateFrobeniusEquiv R p n : (a : R) → R) x : R) : R)

Tactic:
iterateFrobenius_add_apply R p m n x

Premises used: iterateFrobenius_add_apply
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R ≃+* R) (iterateFrobeniusEquiv R p (m + n))
    (RingEquiv.trans (iterateFrobeniusEquiv R p n) (iterateFrobeniusEquiv R p m))

Tactic:
RingEquiv.ext (iterateFrobeniusEquiv_add_apply R p m n)

Premises used: iterateFrobeniusEquiv_add_apply, RingEquiv.ext
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw :
  x =
    (iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
rw₁ :
  x =
    (iterateFrobeniusEquiv R p (n + m) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
rw₂ :
  x =
    (iterateFrobeniusEquiv R p n : (a : R) → R)
      ((iterateFrobeniusEquiv R p m : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
              ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
            R) :
        R)
rw₃ :
  x = (iterateFrobeniusEquiv R p n : (a : R) → R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R)
rw₄ rw₅ : x = x
⊢ Eq (α := R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p (m + n)) : (a : R) → R) x : R) :
      R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
            ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
          R) :
      R)

Tactic:
rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, iterateFrobeniusEquiv_add_apply, add_comm
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R ≃+* R) (RingEquiv.symm (iterateFrobeniusEquiv R p (m + n)))
    (RingEquiv.trans (RingEquiv.symm (iterateFrobeniusEquiv R p n)) (RingEquiv.symm (iterateFrobeniusEquiv R p m)))

Tactic:
RingEquiv.ext (iterateFrobeniusEquiv_symm_add_apply R p m n)

Premises used: iterateFrobeniusEquiv_symm_add_apply, RingEquiv.ext
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 0 = x
rw₁ : HPow.hPow (β := ℕ) x 1 = x
rw₂ rw₃ : x = x
⊢ (iterateFrobeniusEquiv R p 0 : (a : R) → R) x = x

Tactic:
rw [iterateFrobeniusEquiv_def, pow_zero, pow_one]

Premises used: iterateFrobeniusEquiv_def, pow_zero, pow_one
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 1 = x ^ p
rw₁ rw₂ : x ^ p = x ^ p
⊢ (iterateFrobeniusEquiv R p 1 : (a : R) → R) x = x ^ p

Tactic:
rw [iterateFrobeniusEquiv_def, pow_one]

Premises used: iterateFrobeniusEquiv_def, pow_one
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R ≃+* R) (iterateFrobeniusEquiv R p 0) (RingEquiv.refl R)

Tactic:
RingEquiv.ext (iterateFrobeniusEquiv_zero_apply R p)

Premises used: RingEquiv.ext, iterateFrobeniusEquiv_zero_apply
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R ≃+* R) (iterateFrobeniusEquiv R p 1) (frobeniusEquiv R p)

Tactic:
RingEquiv.ext (iterateFrobeniusEquiv_one_apply R p)

Premises used: iterateFrobeniusEquiv_one_apply, RingEquiv.ext
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
rw :
  Eq (α := (a : R) → R) (⇑(iterateFrobeniusEquiv R p n) : (a : R) → R)
    (⇑((RingAut.toPerm R : (a : RingAut R) → Equiv.Perm R) (frobeniusEquiv R p) : Equiv.Perm R) : (a : R) → R)^[n]
⊢ Eq (α := (a : R) → R) (⇑(iterateFrobeniusEquiv R p n) : (a : R) → R)
    (⇑((RingAut.toPerm R : (a : RingAut R) → Equiv.Perm R) (HPow.hPow (α := R ≃+* R) (frobeniusEquiv R p) n) :
          Equiv.Perm R) :
      (a : R) → R)

Tactic:
rw [map_pow, Equiv.Perm.coe_pow]

Premises used: map_pow, Equiv.Perm.coe_pow
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := (a : R) → R) (⇑(iterateFrobeniusEquiv R p n) : (a : R) → R)
    (⇑((RingAut.toPerm R : (a : RingAut R) → Equiv.Perm R) (frobeniusEquiv R p) : Equiv.Perm R) : (a : R) → R)^[n]

Tactic:
(pow_iterate p n).symm

Premises used: pow_iterate, Eq.symm
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := (a : R) → R) (⇑(iterateFrobeniusEquiv R p n) : (a : R) → R)
    (⇑((RingAut.toPerm R : (a : RingAut R) → Equiv.Perm R) (frobeniusEquiv R p) : Equiv.Perm R) : (a : R) → R)^[n]

Tactic:
exact (pow_iterate p n).symm

Premises used: pow_iterate, Eq.symm
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
rw :
  (HPow.hPow (α := R ≃+* R) (frobeniusEquiv R p) n).symm =
    HPow.hPow (α := R ≃+* R) (RingEquiv.symm (frobeniusEquiv R p)) n
⊢ RingEquiv.symm (iterateFrobeniusEquiv R p n) = HPow.hPow (α := R ≃+* R) (RingEquiv.symm (frobeniusEquiv R p)) n

Tactic:
rw [iterateFrobeniusEquiv_eq_pow]

Premises used: iterateFrobeniusEquiv_eq_pow
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ (HPow.hPow (α := R ≃+* R) (frobeniusEquiv R p) n).symm =
    HPow.hPow (α := R ≃+* R) (RingEquiv.symm (frobeniusEquiv R p)) n

Tactic:
(inv_pow _ _).symm

Premises used: inv_pow, Eq.symm
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ (HPow.hPow (α := R ≃+* R) (frobeniusEquiv R p) n).symm =
    HPow.hPow (α := R ≃+* R) (RingEquiv.symm (frobeniusEquiv R p)) n

Tactic:
exact (inv_pow _ _).symm

Premises used: inv_pow, Eq.symm
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ (RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) ((frobenius R p : (a : R) → R) x : R) = x

Tactic:
(frobeniusEquiv R p).symm_apply_apply x

Premises used: frobeniusEquiv, RingEquiv.symm_apply_apply
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ (frobenius R p : (a : R) → R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) = x

Tactic:
(frobeniusEquiv R p).apply_symm_apply x

Premises used: RingEquiv.apply_symm_apply, frobeniusEquiv
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
a :
  ∀ (x : R),
    Eq (α := R) ((RingHom.comp (frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R) x : R)
      ((RingHom.id R : (a : R) → R) x : R)
⊢ Eq (α := R →+* R) (RingHom.comp (frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R)) (RingHom.id R)

Tactic:
ext
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ Eq (α := R) ((RingHom.comp (frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R) x : R)
    ((RingHom.id R : (a : R) → R) x : R)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
a :
  ∀ (x : R),
    Eq (α := R) ((RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) (frobenius R p) : (a : R) → R) x : R)
      ((RingHom.id R : (a : R) → R) x : R)
⊢ Eq (α := R →+* R) (RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) (frobenius R p)) (RingHom.id R)

Tactic:
ext
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ Eq (α := R) ((RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) (frobenius R p) : (a : R) → R) x : R)
    ((RingHom.id R : (a : R) → R) x : R)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
h :
  ∀ (x : R),
    Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) x =
      id x
⊢ Eq (α := R → R)
    (Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)) id

Tactic:
ext
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) x =
    id x

Tactic:
simp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
h :
  ∀ (x : R),
    Function.comp (β := R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) (⇑(frobenius R p) : (a : R) → R) x =
      id x
⊢ Eq (α := R → R)
    (Function.comp (β := R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) (⇑(frobenius R p) : (a : R) → R)) id

Tactic:
ext
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ Function.comp (β := R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) (⇑(frobenius R p) : (a : R) → R) x =
    id x

Tactic:
simp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ HPow.hPow (α := R) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) p = x

Tactic:
frobenius_apply_frobeniusEquiv_symm R p x

Premises used: frobenius_apply_frobeniusEquiv_symm
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ (RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) (x ^ p) = x

Tactic:
(frobeniusEquiv R p).symm_apply_apply x

Premises used: frobeniusEquiv, RingEquiv.symm_apply_apply
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[0] x ^ HPow.hPow (β := ℕ) p 0 = x

Tactic:
simp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
n : ℕ
ih : ∀ (x : R), (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x ^ p ^ n = x
x : R
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n + 1] x ^ p ^ (n + 1) = x

Tactic:
simp [pow_succ, pow_mul, ih]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
n : ℕ
zero : ∀ (x : R), (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[0] x ^ HPow.hPow (β := ℕ) p 0 = x
succ :
  ∀ (n : ℕ) (ih : ∀ (x : R), (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x ^ p ^ n = x) (x : R),
    (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n + 1] x ^ p ^ (n + 1) = x
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x ^ p ^ n = x

Tactic:
induction n generalizing x with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
x : R
apply_fun :
  Eq (α := S)
    ((frobeniusEquiv S p : (a : S) → S)
        ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S) :
      S)
    ((frobeniusEquiv S p : (a : S) → S)
        ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S) :
      S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S)
    ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S)

Tactic:
apply_fun (frobeniusEquiv S p)

Premises used: frobeniusEquiv
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
x : R
⊢ Eq (α := S)
    ((frobeniusEquiv S p : (a : S) → S)
        ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S) :
      S)
    ((frobeniusEquiv S p : (a : S) → S)
        ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S) :
      S)

Tactic:
simp [← MonoidHom.map_frobenius]

Premises used: MonoidHom.map_frobenius
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →+* S
x : R
apply_fun :
  Eq (α := S)
    ((frobeniusEquiv S p : (a : S) → S)
        ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S) :
      S)
    ((frobeniusEquiv S p : (a : S) → S)
        ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S) :
      S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S)
    ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S)

Tactic:
apply_fun (frobeniusEquiv S p)

Premises used: frobeniusEquiv
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →+* S
x : R
⊢ Eq (α := S)
    ((frobeniusEquiv S p : (a : S) → S)
        ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S) :
      S)
    ((frobeniusEquiv S p : (a : S) → S)
        ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S) :
      S)

Tactic:
simp [← RingHom.map_frobenius]

Premises used: RingHom.map_frobenius
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
apply_fun :
  Eq (α := S)
    ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
        ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)
inj : Injective (α := S) (⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x) : S)
    ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x) : S)

Tactic:
apply_fun (frobeniusEquiv S p)^[n]

Premises used: frobeniusEquiv
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
simp :
  Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobenius S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)
⊢ Eq (α := S)
    ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
        ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)

Tactic:
simp only [coe_frobeniusEquiv, ← map_iterate_frobenius]

Premises used: MonoidHom.map_iterate_frobenius, coe_frobeniusEquiv
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
rw :
  Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R)
              (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R))^[n]
          x) :
      S)
    ((Function.comp (β := S) (⇑(frobenius S p) : (a : S) → S)
            (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S))^[n]
        ((f : (a : R) → S) x) :
      S)
h : Function.Commute (α := S) (⇑(frobenius S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)
h₁ : Function.Commute (α := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)
⊢ Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobenius S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)

Tactic:
rw [← Function.comp_apply (f := (⇑(frobenius R p))^[n]),
          ← Function.comp_apply (f := (⇑(frobenius S p))^[n]),
          ← Function.Commute.comp_iterate, ← Function.Commute.comp_iterate]

Premises used: Function.Commute.comp_iterate, Function.comp_apply
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R)
              (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R))^[n]
          x) :
      S)
    ((Function.comp (β := S) (⇑(frobenius S p) : (a : S) → S)
            (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S))^[n]
        ((f : (a : R) → S) x) :
      S)

Tactic:
simp