awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1 : (m : ℕ) → (h : n ≤ m) → R
refine_2 :
  ∀ (n_1 : ℕ),
    HPow.hPow (α := R)
        ((fun (m : ℕ) ↦
            (if h_1 : n ≤ m then
                Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                  (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                    (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                      (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                  h_1
              else x ^ p ^ (n - m) :
              R))
          (n_1 + 1))
        p =
      (fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (n - m) :
            R))
        n_1
refine_3 :
  (coeff R p n : (a : Perfection R p) → R)
      (Subtype.mk (p := fun (f : ℕ → R) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
        (fun (m : ℕ) ↦
          if h_1 : n ≤ m then
            Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
              h_1
          else x ^ p ^ (n - m))
        ⋯) =
    x
⊢ ∃ (a : Perfection R p), (coeff R p n : (a : Perfection R p) → R) a = x

Tactic:
refine ⟨⟨fun m ↦ if h : n ≤ m then ?_ else x ^ p ^ (n - m), ?_⟩, ?_⟩
-- 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
m : ℕ
⊢ R

Tactic:
exact x
-- 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
m k : ℕ
hle : n ≤ k
xk : R
refine_1 : (x : R) → (hx : (frobenius R p : (a : R) → R) x = xk) → R
⊢ R

Tactic:
choose x hx using h xk
-- 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_1 : R
m k : ℕ
hle : n ≤ k
xk x : R
hx : (frobenius R p : (a : R) → R) x = xk
⊢ R

Tactic:
use x
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h_1 : Function.Surjective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
n : ℕ
x : R
m : ℕ
h : n ≤ m
refine_1 : R
refine_1₁ : ⦃k : ℕ⦄ → (hle : n ≤ k) → (xk : R) → R
⊢ R

Tactic:
induction h using Nat.leRec with
    | refl =>
      exact x
    | le_succ_of_le hle xk =>
      choose x hx using h xk
      use x

Premises used: refl
-- 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
m : ℕ
⊢ n ≤ m ∨ n = m + 1 ∨ ¬n ≤ m + 1

Tactic:
lia
-- 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
m : ℕ
h1 : n ≤ m
⊢ n ≤ m + 1

Tactic:
lia
-- 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
m : ℕ
h1 : n ≤ m
⊢ n ≤ m + 1

Tactic:
have h1' : n ≤ m + 1 := by lia
-- 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
m : ℕ
h1 : n ≤ m
h1' : n ≤ m + 1
refine_2 :
  Eq (α := R)
    ((frobenius R p : (a : R) → R)
        (Classical.choose (p := fun (a : R) ↦
          Eq (α := R) ((frobenius R p : (a : R) → R) a : R)
            (Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯)
                h1 :
              R))
          ⋯) :
      R)
    (Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
        (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
          Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯)
        ⋯ :
      R)
⊢ HPow.hPow (α := R)
      ((fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (n - m) :
            R))
        (m + 1))
      p =
    (fun (m : ℕ) ↦
        (if h_1 : n ≤ m then
            Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
              h_1
          else x ^ p ^ (n - m) :
          R))
      m

Tactic:
simp only [h1', ↓reduceDIte, h1, Nat.leRec_succ, ← frobenius_def]

Premises used: reduceDIte, frobenius_def, Nat.leRec_succ
-- 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
m : ℕ
h1 : n ≤ m
h1' : n ≤ m + 1
⊢ Eq (α := R)
    ((frobenius R p : (a : R) → R)
        (Classical.choose (p := fun (a : R) ↦
          Eq (α := R) ((frobenius R p : (a : R) → R) a : R)
            (Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯)
                h1 :
              R))
          ⋯) :
      R)
    (Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
        (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
          Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯)
        ⋯ :
      R)

Tactic:
Classical.choose_spec (h _)

Premises used: Classical.choose_spec
-- 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
m : ℕ
h1 : n ≤ m
h1' : n ≤ m + 1
⊢ Eq (α := R)
    ((frobenius R p : (a : R) → R)
        (Classical.choose (p := fun (a : R) ↦
          Eq (α := R) ((frobenius R p : (a : R) → R) a : R)
            (Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯)
                h1 :
              R))
          ⋯) :
      R)
    (Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
        (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
          Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯)
        ⋯ :
      R)

Tactic:
exact Classical.choose_spec (h _)

Premises used: Classical.choose_spec
-- 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
m : ℕ
h1 : n = m + 1
refine_2 :
  HPow.hPow (α := R)
      ((fun (m_1 : ℕ) ↦
          (if h_1 : m + 1 ≤ m_1 then
              Nat.leRec (motive := fun (m_2 : ℕ) (h : m + 1 ≤ m_2) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : m + 1 ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (m + 1 - m_1) :
            R))
        (m + 1))
      p =
    (fun (m_1 : ℕ) ↦
        (if h_1 : m + 1 ≤ m_1 then
            Nat.leRec (motive := fun (m_2 : ℕ) (h : m + 1 ≤ m_2) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : m + 1 ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
              h_1
          else x ^ p ^ (m + 1 - m_1) :
          R))
      m
⊢ HPow.hPow (α := R)
      ((fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (n - m) :
            R))
        (m + 1))
      p =
    (fun (m : ℕ) ↦
        (if h_1 : n ≤ m then
            Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
              h_1
          else x ^ p ^ (n - m) :
          R))
      m

Tactic:
subst h1
-- 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)
x : R
m : ℕ
⊢ HPow.hPow (α := R)
      ((fun (m_1 : ℕ) ↦
          (if h_1 : m + 1 ≤ m_1 then
              Nat.leRec (motive := fun (m_2 : ℕ) (h : m + 1 ≤ m_2) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : m + 1 ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (m + 1 - m_1) :
            R))
        (m + 1))
      p =
    (fun (m_1 : ℕ) ↦
        (if h_1 : m + 1 ≤ m_1 then
            Nat.leRec (motive := fun (m_2 : ℕ) (h : m + 1 ≤ m_2) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : m + 1 ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
              h_1
          else x ^ p ^ (m + 1 - m_1) :
          R))
      m

Tactic:
simp [← frobenius_def]

Premises used: frobenius_def
-- 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
m : ℕ
h1 : ¬n ≤ m + 1
⊢ ¬n ≤ m

Tactic:
lia
-- 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
m : ℕ
h1 : ¬n ≤ m + 1
⊢ ¬n ≤ m

Tactic:
have h1' : ¬ n ≤ m := by lia
-- 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
m : ℕ
h1 : ¬n ≤ m + 1
h1' : ¬n ≤ m
⊢ n - m = n - (m + 1) + 1

Tactic:
lia
-- 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
m : ℕ
h1 : ¬n ≤ m + 1
h1' : ¬n ≤ m
⊢ n - m = n - (m + 1) + 1

Tactic:
have : n - m = (n - (m + 1)) + 1 := by lia
-- 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
m : ℕ
h1 : ¬n ≤ m + 1
h1' : ¬n ≤ m
this : n - m = n - (m + 1) + 1
⊢ HPow.hPow (α := R)
      ((fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
                h_1
            else x ^ p ^ (n - m) :
            R))
        (m + 1))
      p =
    (fun (m : ℕ) ↦
        (if h_1 : n ≤ m then
            Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
              h_1
          else x ^ p ^ (n - m) :
          R))
      m

Tactic:
simp [h1, h1', this, pow_succ, pow_mul]

Premises used: pow_succ, pow_mul
-- 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
⊢ (coeff R p n : (a : Perfection R p) → R)
      (Subtype.mk (p := fun (f : ℕ → R) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
        (fun (m : ℕ) ↦
          if h_1 : n ≤ m then
            Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) ⋯) ⋯)
              h_1
          else x ^ p ^ (n - m))
        ⋯) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R_1 p
R : Type u₁
inst_2 : CommSemiring R
inst_3 : CharP R p
inst_4 : PerfectRing R p
S : Type u₂
inst_5 : CommSemiring S
inst_6 : CharP S p
f : R →+* S
r : R
n : ℕ
rw :
  Eq.{u₂ + 1} (α := S)
    ((f : (a : R) → S) ((⇑(↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R)^[n + 1] r ^ p) : S)
    ((fun (n : ℕ) ↦ ((f : (a : R) → S) ((⇑(↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R)^[n] r) : S))
        n :
      S)
rw₁ :
  Eq.{u₂ + 1} (α := S)
    ((f : (a : R) → S)
        (HPow.hPow (α := R)
          (((↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R)
              ((⇑(↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R)^[n] r) :
            R)
          p) :
      S)
    ((fun (n : ℕ) ↦ ((f : (a : R) → S) ((⇑(↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R)^[n] r) : S))
        n :
      S)
rw₂ :
  Eq.{u₂ + 1} (α := S)
    ((f : (a : R) → S)
        (HPow.hPow (α := R)
          ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R)
              ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r) :
            R)
          p) :
      S)
    ((fun (n : ℕ) ↦ ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r) : S)) n : S)
rw₃ rw₄ :
  Eq.{u₂ + 1} (α := S) ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r) : S)
    ((fun (n : ℕ) ↦ ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r) : S)) n : S)
⊢ HPow.hPow (α := S)
      ((fun (n : ℕ) ↦
          ((f : (a : R) → S) ((⇑(↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R)^[n] r) : S))
        (n + 1))
      p =
    (fun (n : ℕ) ↦ ((f : (a : R) → S) ((⇑(↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R)^[n] r) : S))
      n

Tactic:
rw [← f.map_pow, Function.iterate_succ_apply', RingHom.coe_coe,
          frobeniusEquiv_symm_pow_p]

Premises used: Function.iterate_succ_apply', RingHom.coe_coe, frobeniusEquiv_symm_pow_p, RingHom.map_pow
-- Module: Mathlib.RingTheory.Perfection
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R_1 p
R : Type u₁
inst_2 : CommSemiring R
inst_3 : CharP R p
inst_4 : PerfectRing R p
S : Type u₂
inst_5 : CommSemiring S
inst_6 : CharP S p
f : RingHom.{u₁, u₂} R (Perfection S p)
r : R
n : ℕ
rw :
  Eq (α := S)
    ((coeff S p (0 + n) : (a : Perfection S p) → S)
        ((⇑(frobenius (Perfection S p) p) : (a : Perfection S p) → Perfection S p)^[n]
            ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
rw₁ :
  Eq (α := S)
    ((coeff S p n : (a : Perfection S p) → S)
        ((⇑(frobenius (Perfection S p) p) : (a : Perfection S p) → Perfection S p)^[n]
            ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
rw₂ :
  Eq (α := S)
    ((coeff S p n : (a : Perfection S p) → S)
        ((f : (a : R) → Perfection S p)
            ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
rw₃ rw₄ :
  Eq (α := S) ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
⊢ Eq (α := S)
    ((coeff S p 0 : (a : Perfection S p) → S)
        ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)

Tactic:
rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← RingHom.map_iterate_frobenius,
        Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n]

Premises used: Function.RightInverse.iterate, RingHom.map_iterate_frobenius, Perfection.coeff_iterate_frobenius, zero_add, frobenius_apply_frobeniusEquiv_symm, OfNat.ofNat
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u₁
inst : CommSemiring R
inst_1 : CharP R p
inst_2 : PerfectRing R p
S : Type u₂
inst_3 : CommSemiring S
inst_4 : CharP S p
f g : RingHom.{u₁, u₂} R (Perfection S p)
hfg :
  ∀ (x : R),
    Eq (α := S) ((coeff S p 0 : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) x : Perfection S p) : S)
      ((coeff S p 0 : (a : Perfection S p) → S) ((g : (a : R) → Perfection S p) x : Perfection S p) : S)
⊢ f = g

Tactic:
(lift p R S).symm.injective <| RingHom.ext hfg

Premises used: RingHom.ext, Equiv.injective, Equiv.symm, Perfection.lift
-- Module: Mathlib.RingTheory.Perfection
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
S : Type u₂
inst_2 : CommSemiring S
inst_3 : CharP S p
φ : R →+* S
f : Perfection R p
n : ℕ
⊢ Eq (α := S)
    ((coeff S p n : (a : Perfection S p) → S)
        (((map p φ : RingHom.{u_1, u₂} (Perfection R p) (Perfection S p)) : (a : Perfection R p) → Perfection S p) f :
          Perfection S p) :
      S)
    ((φ : (a : R) → S) ((coeff R p n : (a : Perfection R p) → R) f : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
M : Type u_1
N : Type u_2
inst_1 : CommMonoid M
inst_2 : CommRing N
inst_3 : CharP N p
e : M →* N
n : ℕ
x : Perfection M p
⊢ Eq (α := N)
    ((coeff N p n : (a : Perfection N p) → N)
        ((mapMonoidHom p e : (a : Perfection M p) → Perfection N p) x : Perfection N p) :
      N)
    ((e : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P : Type u₃
inst_3 : CommSemiring P
inst_4 : CharP P p
inst_5 : PerfectRing P p
f : P →+* R
g : RingEquiv.{u₃, u₁} P (Perfection R p)
hfg :
  Eq (α := RingHom.{u₃, u₁} P (Perfection R p))
    ((Perfection.lift p P R : (a : P →+* R) → P →+* Perfection R p) f : RingHom.{u₃, u₁} P (Perfection R p))
    ((↑g : RingHom.{u₃, u₁} P (Perfection R p)) : RingHom.{u₃, u₁} P (Perfection R p))
y : ℕ → R
hy : ∀ (n : ℕ), y (n + 1) ^ p = y n
x : P
hx :
  Eq.{u₁ + 1} (α := Perfection R p) ((g : (a : P) → Perfection R p) x : Perfection R p)
    (Subtype.mk (p := fun (f : ℕ → R) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n) y hy :
      { f : ℕ → R // ∀ (n : ℕ), f (n + 1) ^ p = f n })
n : ℕ
⊢ Eq (α := R)
    ((Perfection.coeff R p n : (a : Perfection R p) → R)
        ((((Perfection.lift p P R : (a : P →+* R) → P →+* Perfection R p) f : RingHom.{u₃, u₁} P (Perfection R p)) :
              (a : P) → Perfection R p)
            x :
          Perfection R p) :
      R)
    ((Perfection.coeff R p n : (a : Perfection R p) → R)
        (Subtype.mk (p := fun (f : ℕ → R) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n) y hy) :
      R)

Tactic:
simp [hfg, hx]
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
⊢ PerfectionMap p (Perfection.coeff R p 0)

Tactic:
mk' (RingEquiv.refl _) <| (Equiv.apply_eq_iff_eq_symm_apply _).2 rfl

Premises used: Iff.mpr, RingEquiv.refl, PerfectionMap.mk', rfl, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
inst_3 : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n_1 n : ℕ
ih : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n
rw :
  HPow.hPow (α := R)
      ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R)
          ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0)) :
        R)
      p =
    f n.succ ^ p
rw₁ : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n.succ ^ p
rw₂ : f n = f n.succ ^ p
rw₃ rw₄ : f n = f n
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n.succ] (f 0) ^ p = f n.succ ^ p

Tactic:
rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]

Premises used: Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P : Type u₃
inst_3 : CommSemiring P
inst_4 : CharP P p
inst_5 : PerfectRing P p
π : P →+* R
m : PerfectionMap p π
x : P
⊢ Eq.{u₁ + 1} (α := Perfection R p) ((m.equiv : (a : P) → Perfection R p) x : Perfection R p)
    ((((Perfection.lift p P R : (a : P →+* R) → P →+* Perfection R p) π : RingHom.{u₃, u₁} P (Perfection R p)) :
          (a : P) → Perfection R p)
        x :
      Perfection R p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P : Type u₃
inst_3 : CommSemiring P
inst_4 : CharP P p
inst_5 : PerfectRing P p
π : P →+* R
m : PerfectionMap p π
x : P
⊢ Eq (α := R)
    ((Perfection.coeff R p 0 : (a : Perfection R p) → R) ((m.equiv : (a : P) → Perfection R p) x : Perfection R p) : R)
    ((π : (a : P) → R) x : R)

Tactic:
rfl

Premises used: Nat.iterate, rfl