awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Perfection
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : MonoidHom.{u_2, u_3} M (Perfection N p)
m : M
n : ℕ
h :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
        (HPow.hPow (α := Perfection N p)
          ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p)
          (p ^ n)) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
h₁ :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p)
            (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m : M) (p ^ n)) :
          Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
h₂ :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
h₃ h₄ :
  Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
⊢ Eq (α := N)
    ((coeffMonoidHom N p 0 : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)

Tactic:
rw [← coeffMonoidHom_pow_p_pow _ 0 n, ← map_pow, powMulEquiv_symm_pow_p, zero_add]

Premises used: map_pow, zero_add, powMulEquiv_symm_pow_p, OfNat.ofNat, Perfection.coeffMonoidHom_pow_p_pow
-- Module: Mathlib.RingTheory.Perfection
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
x x_1 : M →* N
h :
  ∀ (x_2 : M) (n : ℕ),
    Eq (α := N)
      ((coeffMonoidHom N p n : (a : Perfection N p) → N)
          (({
                  toFun := fun (r : M) ↦
                    Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                      (fun (n : ℕ) ↦
                        (x * x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                      ⋯,
                  map_one' := ⋯, map_mul' := ⋯ } :
                (a : M) → Perfection N p)
              x_2 :
            Perfection N p) :
        N)
      ((coeffMonoidHom N p n : (a : Perfection N p) → N)
          ((HMul.hMul (α := MonoidHom.{u_2, u_3} M (Perfection N p))
                  {
                    toFun := fun (r : M) ↦
                      Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                        (fun (n : ℕ) ↦ (x : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                        ⋯,
                    map_one' := ⋯, map_mul' := ⋯ : MonoidHom.{u_2, u_3} M (Perfection N p) }
                  {
                    toFun := fun (r : M) ↦
                      Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                        (fun (n : ℕ) ↦
                          (x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                        ⋯,
                    map_one' := ⋯, map_mul' := ⋯ : MonoidHom.{u_2, u_3} M (Perfection N p) } :
                (a : M) → Perfection N p)
              x_2 :
            Perfection N p) :
        N)
⊢ {
      toFun := fun (r : M) ↦
        Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (x * x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
      map_one' := ⋯, map_mul' := ⋯ } =
    HMul.hMul (α := MonoidHom.{u_2, u_3} M (Perfection N p))
      {
        toFun := fun (r : M) ↦
          Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (x : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
        map_one' := ⋯, map_mul' := ⋯ : MonoidHom.{u_2, u_3} M (Perfection N p) }
      {
        toFun := fun (r : M) ↦
          Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
        map_one' := ⋯, map_mul' := ⋯ : MonoidHom.{u_2, u_3} M (Perfection N p) }

Tactic:
ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
x x_1 : M →* N
x_2 : M
n : ℕ
⊢ Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        (({
                toFun := fun (r : M) ↦
                  Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                    (fun (n : ℕ) ↦
                      (x * x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                    ⋯,
                map_one' := ⋯, map_mul' := ⋯ } :
              (a : M) → Perfection N p)
            x_2 :
          Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        ((HMul.hMul (α := MonoidHom.{u_2, u_3} M (Perfection N p))
                {
                  toFun := fun (r : M) ↦
                    Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                      (fun (n : ℕ) ↦ (x : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
                  map_one' := ⋯, map_mul' := ⋯ : MonoidHom.{u_2, u_3} M (Perfection N p) }
                {
                  toFun := fun (r : M) ↦
                    Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                      (fun (n : ℕ) ↦ (x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                      ⋯,
                  map_one' := ⋯, map_mul' := ⋯ : MonoidHom.{u_2, u_3} M (Perfection N p) } :
              (a : M) → Perfection N p)
            x_2 :
          Perfection N p) :
      N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
M : Type u_2
N : Type u_3
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : CommMonoid N
e : M →* N
x : M
⊢ Eq (α := N)
    ((coeffMonoidHom N p 0 : (a : Perfection N p) → N)
        ((((liftMonoidHom p M N : (a : M →* N) → M →* Perfection N p) e : MonoidHom.{u_2, u_3} M (Perfection N p)) :
              (a : M) → Perfection N p)
            x :
          Perfection N p) :
      N)
    ((e : (a : M) → N) x : N)

Tactic:
simp [liftMonoidHom]

Premises used: Perfection.liftMonoidHom
-- Module: Mathlib.RingTheory.Perfection
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
f : Perfection M p
n : ℕ
rw :
  Eq.{u_3 + 1} (α := N)
    ((φ : (a : M) → N) (HPow.hPow (α := M) ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M) p) : N)
    ((fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) n : N)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := N) ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)
    ((fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) n : N)
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) (n + 1)) p =
    (fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) n

Tactic:
rw [← map_pow, coeffMonoidHom_pow_p']

Premises used: map_pow, Perfection.coeffMonoidHom_pow_p'
-- Module: Mathlib.RingTheory.Perfection
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
h :
  ∀ (n : ℕ),
    Eq (α := N)
      ((coeffMonoidHom N p n : (a : Perfection N p) → N)
          (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) 1 : M)) ⋯) :
        N)
      ((coeffMonoidHom N p n : (a : Perfection N p) → N) 1 : N)
⊢ Eq.{u_3 + 1} (α := Perfection N p)
    (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
      (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) 1 : M)) ⋯)
    1

Tactic:
ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
n : ℕ
⊢ Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) 1 : M)) ⋯) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) 1 : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
x x_1 : Perfection M p
h :
  ∀ (n : ℕ),
    Eq (α := N)
      ((coeffMonoidHom N p n : (a : Perfection N p) → N)
          (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) (x * x_1) : M)) ⋯) :
        N)
      ((coeffMonoidHom N p n : (a : Perfection N p) → N)
          (HMul.hMul (α := Perfection N p)
            (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
              (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)) ⋯)
            (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
              (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x_1 : M)) ⋯)) :
        N)
⊢ Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
      (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) (x * x_1) : M)) ⋯ =
    HMul.hMul (α := Perfection N p)
      (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
        (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)) ⋯)
      (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
        (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x_1 : M)) ⋯)

Tactic:
ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
x x_1 : Perfection M p
n : ℕ
⊢ Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) (x * x_1) : M)) ⋯) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        (HMul.hMul (α := Perfection N p)
          (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)) ⋯)
          (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x_1 : M)) ⋯)) :
      N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
M : Type u_2
N : Type u_3
inst : CommMonoid M
inst_1 : CommMonoid N
φ : M →* N
f : Perfection M p
n : ℕ
⊢ Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        ((mapMonoidHom p φ : (a : Perfection M p) → Perfection N p) f : Perfection N p) :
      N)
    ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ CharP.{u_1} (Perfection R p) p

Tactic:
CharP.subsemiring _ _ (subsemiring R p)

Premises used: Perfection, Set.Mem, setOf, CharP.subsemiring, Perfection.subsemiring
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f g : Perfection R p
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) ((coeff R p n : (a : Perfection R p) → R) g : R)
⊢ f = g

Tactic:
extMonoid h

Premises used: Perfection.extMonoid
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
a :
  ∀ (x : Perfection R p),
    Eq (α := Perfection R p) ((pthRoot R p : (a : Perfection R p) → Perfection R p) x : Perfection R p)
      (((↑(RingEquiv.symm (frobeniusEquiv (Perfection R p) p)) : Perfection R p →+* Perfection R p) :
            (a : Perfection R p) → Perfection R p)
          x :
        Perfection R p)
⊢ Eq (α := Perfection R p →+* Perfection R p) (pthRoot R p)
    (↑(RingEquiv.symm (frobeniusEquiv (Perfection R p) p)) : Perfection R p →+* Perfection R p)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
x : Perfection R p
⊢ Eq (α := Perfection R p) ((pthRoot R p : (a : Perfection R p) → Perfection R p) x : Perfection R p)
    (((↑(RingEquiv.symm (frobeniusEquiv (Perfection R p) p)) : Perfection R p →+* Perfection R p) :
          (a : Perfection R p) → Perfection R p)
        x :
      Perfection R p)

Tactic:
simpa [RingEquiv.eq_symm_apply] using ext <| coeffMonoidHom_pow_p' _

Premises used: Perfection.coeffMonoidHom_pow_p', Perfection.ext, RingEquiv.eq_symm_apply
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ Eq (α := (a : Perfection R p) → Perfection R p) (⇑(pthRoot R p) : (a : Perfection R p) → Perfection R p)
    (⇑(RingEquiv.symm (frobeniusEquiv (Perfection R p) p)) : (a : Perfection R p) → Perfection R p)

Tactic:
congr($pthRoot_eq_symm_frobeniusEquiv)

Premises used: congrArg, id, Perfection.pthRoot_eq_symm_frobeniusEquiv, DFunLike.coe
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
n : ℕ
⊢ Eq (α := (a : Perfection R p) → R) (⇑(coeffMonoidHom R p n) : (a : Perfection R p) → R)
    (⇑(coeff R p n) : (a : Perfection R p) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ Eq (α := (a : Perfection R p) → Perfection R p) (⇑(pthRootMonoidHom R p) : (a : Perfection R p) → Perfection R p)
    (⇑(pthRoot R p) : (a : Perfection R p) → Perfection R p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ Eq (α := (a : Perfection R p) → Perfection R p) (⇑(pthRootMonoidHom R p) : (a : Perfection R p) → Perfection R p)
    (⇑(↑(RingEquiv.symm (frobeniusEquiv (Perfection R p) p)) : Perfection R p →+* Perfection R p) :
      (a : Perfection R p) → Perfection R p)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
n : ℕ
⊢ Eq (α := Perfection R p →* R) (↑(coeff R p n) : Perfection R p →* R) (coeffMonoidHom R p n)

Tactic:
rfl

Premises used: Perfection.coeffMonoidHom, rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n : ℕ
⊢ (coeff R p n : (a : Perfection R p) → R) (Subtype.mk (p := fun (f : ℕ → R) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n) f hf) =
    f n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
⊢ Eq (α := R)
    ((coeff R p n : (a : Perfection R p) → R)
        ((RingEquiv.symm (frobeniusEquiv (Perfection R p) p) : (a : Perfection R p) → Perfection R p) f :
          Perfection R p) :
      R)
    ((coeff R p (n + 1) : (a : Perfection R p) → R) f : R)

Tactic:
coeffMonoidHom_symm_powMulEquiv ..

Premises used: Perfection.coeffMonoidHom_symm_powMulEquiv
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n m : ℕ
⊢ Eq (α := R)
    ((coeff R p n : (a : Perfection R p) → R)
        ((⇑(RingEquiv.symm (frobeniusEquiv (Perfection R p) p)) : (a : Perfection R p) → Perfection R p)^[m] f) :
      R)
    ((coeff R p (n + m) : (a : Perfection R p) → R) f : R)

Tactic:
coeffMonoidHom_iterate_symm_powMulEquiv ..

Premises used: Equiv.ofBijective, Perfection.coeffMonoidHom_iterate_symm_powMulEquiv
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
⊢ Eq (α := R) ((coeff R p (n + 1) : (a : Perfection R p) → R) (f ^ p) : R)
    ((coeff R p n : (a : Perfection R p) → R) f : R)

Tactic:
coeffMonoidHom_pow_p f n

Premises used: Perfection.coeffMonoidHom_pow_p
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
⊢ HPow.hPow (α := R) ((coeff R p (n + 1) : (a : Perfection R p) → R) f : R) p =
    (coeff R p n : (a : Perfection R p) → R) f

Tactic:
f.2 n

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
⊢ Eq (α := R)
    ((coeff R p (n + 1) : (a : Perfection R p) → R)
        ((frobenius (Perfection R p) p : (a : Perfection R p) → Perfection R p) f : Perfection R p) :
      R)
    ((coeff R p n : (a : Perfection R p) → R) f : R)

Tactic:
coeffMonoidHom_powMonoidHom f n

Premises used: Perfection.coeffMonoidHom_powMonoidHom
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n m : ℕ
⊢ Eq (α := R)
    ((coeff R p (n + m) : (a : Perfection R p) → R)
        ((⇑(frobenius (Perfection R p) p) : (a : Perfection R p) → Perfection R p)^[m] f) :
      R)
    ((coeff R p n : (a : Perfection R p) → R) f : R)

Tactic:
coeffMonoidHom_iterate_powMonoidHom ..

Premises used: Perfection.coeffMonoidHom_iterate_powMonoidHom
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n m : ℕ
hmn : m ≤ n
⊢ Eq (α := R)
    ((coeff R p n : (a : Perfection R p) → R)
        ((⇑(frobenius (Perfection R p) p) : (a : Perfection R p) → Perfection R p)^[m] f) :
      R)
    ((coeff R p (n - m) : (a : Perfection R p) → R) f : R)

Tactic:
coeffMonoidHom_iterate_powMonoidHom' _ _ _ hmn

Premises used: Perfection.coeffMonoidHom_iterate_powMonoidHom'
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
a :
  ∀ (x : Perfection R p) (n : ℕ),
    Eq (α := R)
      ((coeff R p n : (a : Perfection R p) → R)
          ((RingHom.comp (pthRoot R p) (frobenius (Perfection R p) p) : (a : Perfection R p) → Perfection R p) x :
            Perfection R p) :
        R)
      ((coeff R p n : (a : Perfection R p) → R)
          ((RingHom.id (Perfection R p) : (a : Perfection R p) → Perfection R p) x : Perfection R p) :
        R)
⊢ Eq (α := Perfection R p →+* Perfection R p) (RingHom.comp (pthRoot R p) (frobenius (Perfection R p) p))
    (RingHom.id (Perfection R p))

Tactic:
ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
x : Perfection R p
n : ℕ
⊢ Eq (α := R)
    ((coeff R p n : (a : Perfection R p) → R)
        ((RingHom.comp (pthRoot R p) (frobenius (Perfection R p) p) : (a : Perfection R p) → Perfection R p) x :
          Perfection R p) :
      R)
    ((coeff R p n : (a : Perfection R p) → R)
        ((RingHom.id (Perfection R p) : (a : Perfection R p) → Perfection R p) x : Perfection R p) :
      R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ Eq (α := Perfection R p →+* Perfection R p) (RingHom.comp (frobenius (Perfection R p) p) (pthRoot R p))
    (RingHom.id (Perfection R p))

Tactic:
pthRoot_frobenius

Premises used: Perfection.pthRoot_frobenius, Set.Mem, setOf, Perfection.pthRoot, frobenius, Perfection.pthRootMonoidHom, powMonoidHom
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
hfn : Ne (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) (0 : R)
k_1 k : ℕ
ih : Ne (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
h : Eq (α := R) ((coeff R p (n + k.succ) : (a : Perfection R p) → R) f : R) (0 : R)
⊢ Eq (α := R) ((coeff R p (n + k).succ : (a : Perfection R p) → R) f : R) (0 : R)

Tactic:
rw [Nat.add_succ] at h

Premises used: Nat.add_succ
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
hfn : Ne (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) (0 : R)
k_1 k : ℕ
ih : Ne (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
h : Eq (α := R) ((coeff R p (n + k).succ : (a : Perfection R p) → R) f : R) (0 : R)
rw : Eq (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) (f ^ p) : R) (0 : R)
rw₁ : HPow.hPow (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) f : R) p = 0
rw₂ : HPow.hPow (α := R) 0 p = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)

Tactic:
rw [← coeff_pow_p, map_pow, h, zero_pow hp.1.ne_zero]

Premises used: map_pow, Nat.Prime.ne_zero, Perfection.coeff_pow_p, zero_pow, Fact.out
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
m n : ℕ
hfm : Ne (α := R) ((coeff R p m : (a : Perfection R p) → R) f : R) (0 : R)
hmn : m ≤ n
⊢ Ne (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) (0 : R)

Tactic:
let ⟨k, hk⟩ := Nat.exists_eq_add_of_le hmn
  hk.symm ▸ coeff_add_ne_zero hfm k

Premises used: Nat.exists_eq_add_of_le, Eq.rec, Ne, _private.0.Perfection.coeff_ne_zero_of_le.match_1, Perfection.coeff_add_ne_zero, Perfection.coeff, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Function.Surjective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
n : ℕ
x : R
⊢ ∃ (a : Perfection R p), (coeff R p n : (a : Perfection R p) → R) a = x

Tactic:
⟨⟨fun m ↦ if h : n ≤ m then ?_ else x ^ p ^ (n - m), ?_⟩, ?_⟩

Premises used: HSub.hSub, LE.le, dite, Subtype.mk, HPow.hPow, Exists.intro