awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ ∃ (a : Perfection R p), (coeff R p n : (a : Perfection R p) → R) a = x
have 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) sorry) sorry)
            h_1
        else x ^ p ^ (n - m))
      sorry) =
  x
Tactic: refine ⟨⟨fun m ↦ if h : n ≤ m then ?_ else x ^ p ^ (n - m), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ R
have refine_1 : (x : R) → (hx : (frobenius R p : (a : R) → R) x = xk) → R
Tactic: choose x hx using h xk
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ R
have refine_1₁ : ⦃k : ℕ⦄ → (hle : n ≤ k) → (xk : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℕ
⊢ 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
have refine_2 : ∀ (h1 : n ≤ 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) sorry) sorry)
                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) sorry) sorry)
              h_1
          else x ^ p ^ (n - m) :
          R))
      m
Tactic: obtain (h1 | h1 | h1) : n ≤ m ∨ n = m + 1 ∨ ¬ n ≤ m + 1 := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℕ
refine_2 :
  ∀ (h1 : n ≤ 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
⊢ 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
have refine_2₁ : ∀ (h1 : n = m + 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) sorry) sorry)
                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) sorry) sorry)
              h_1
          else x ^ p ^ (n - m) :
          R))
      m
Tactic: obtain (h1 | h1 | h1) : n ≤ m ∨ n = m + 1 ∨ ¬ n ≤ m + 1 := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (hypothesis)
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
⊢ 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
have h1' : n ≤ m + 1
Tactic: have h1' : n ≤ m + 1 := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ 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
have 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) sorry)
              h1 :
            R))
        sorry) :
    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) sorry)
      sorry :
    R)
Tactic: simp only [h1', ↓reduceDIte, h1, Nat.leRec_succ, ← frobenius_def]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ 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
have 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) sorry) sorry)
              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) sorry) sorry)
            h_1
        else x ^ p ^ (m + 1 - m_1) :
        R))
    m
Tactic: subst h1
Cleared hypotheses: n, h1
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (hypothesis)
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
⊢ 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
have h1' : ¬n ≤ m
Tactic: have h1' : ¬ n ≤ m := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (hypothesis)
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
⊢ 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
have this : n - m = n - (m + 1) + 1
Tactic: have : n - m = (n - (m + 1)) + 1 := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℕ
⊢ 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
have 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)
Tactic: rw [← f.map_pow, Function.iterate_succ_apply', RingHom.coe_coe,
          frobeniusEquiv_symm_pow_p]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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
have 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)
Tactic: rw [← f.map_pow, Function.iterate_succ_apply', RingHom.coe_coe,
          frobeniusEquiv_symm_pow_p]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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
have 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)
Tactic: rw [← f.map_pow, Function.iterate_succ_apply', RingHom.coe_coe,
          frobeniusEquiv_symm_pow_p]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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
have 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)
Tactic: rw [← f.map_pow, Function.iterate_succ_apply', RingHom.coe_coe,
          frobeniusEquiv_symm_pow_p]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← RingHom.map_iterate_frobenius,
        Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n]