awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
n m : σ →₀ ℕ
h : n ≤ m
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
rw :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          (↑((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) :
      MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          (↑((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) :
      MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
              ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
          MvPowerSeries σ R) :
      MvPolynomial σ R)
have rw₂ : Eq (α := MvPolynomial σ R)
  ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) :
    MvPolynomial σ R)
  ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        (↑((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) :
    MvPolynomial σ R)
Tactic: rw [← expand_eq_expand p hp, trunc'_expand, ← trunc'_trunc' h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
⊢ (map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p
have rw : ∀ (a : σ →₀ ℕ),
  ∃ b ≥ a,
    Eq (α := MvPolynomial σ R)
      ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
        MvPolynomial σ R)
      ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: rw [eq_iff_frequently_trunc'_eq, Filter.frequently_atTop]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∃ b ≥ n,
    Eq (α := MvPolynomial σ R)
      ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
        MvPolynomial σ R)
      ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
have h : p • n ≥ n ∧
  Eq (α := MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: use (p • n)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ p • n ≥ n ∧
    Eq (α := MvPolynomial σ R)
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
        MvPolynomial σ R)
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
have h : Eq (α := MvPolynomial σ R)
  ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
    MvPolynomial σ R)
  ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: refine ⟨le_self_nsmul zero_le hp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq (α := MvPowerSeries σ R)
    (↑((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))) :
      MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
        MvPowerSeries σ R))
have simp : Eq (α := MvPowerSeries σ R)
  ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      (↑((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
        MvPowerSeries σ R) :
    MvPowerSeries σ R)
  ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        (↑((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) :
    MvPowerSeries σ R)
Tactic: simp only [MvPolynomial.map_expand, ← expand_eq_expand p hp, map_expand]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
have this : Eq (α := MvPowerSeries σ R)
  (↑((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))) :
    MvPowerSeries σ R)
  ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
    (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
      MvPowerSeries σ R))
Tactic: have : (((trunc' R (p • n) f).expand p).map (frobenius R p)).toMvPowerSeries =
      MvPowerSeries.map (frobenius R p) ((trunc' R (p • n) f).expand p) := by
      simp only [MvPolynomial.map_expand, ← expand_eq_expand p hp, map_expand]
      congr
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  Eq (α := MvPowerSeries σ R)
    (↑((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))) :
      MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
        MvPowerSeries σ R))
⊢ Eq (α := MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
have h : Eq (α := MvPolynomial σ R)
  ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
    MvPolynomial σ R)
  ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  Eq (α := MvPowerSeries σ R)
    (↑((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))) :
      MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
        MvPowerSeries σ R))
h :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
have h₁ : Eq (α := MvPolynomial σ R)
  ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
    MvPolynomial σ R)
  ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  Eq (α := MvPowerSeries σ R)
    (↑((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f))) :
      MvPowerSeries σ R)
    ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      (↑((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
            ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
        MvPowerSeries σ R))
h :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
h₁ :
  Eq (α := MvPolynomial σ R)
    ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
have h₂ : Eq (α := MvPolynomial σ R)
  ((MvPolynomial.map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f)) :
    MvPolynomial σ R)
  ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
      (HPow.hPow (α := MvPowerSeries σ R)
        (↑((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) p) :
    MvPolynomial σ R)
Tactic: rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
⊢ (map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p
have rw : ∃ᶠ (m : σ →₀ ℕ) in Filter.atTop,
  Eq (α := MvPolynomial σ R)
    ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: classical
  rw [eq_iff_frequently_trunc'_eq, Filter.frequently_atTop]
  intro n
  use (p • n)
  refine ⟨le_self_nsmul zero_le hp, ?_⟩
  · have : (((trunc' R (p • n) f).expand p).map (frobenius R p)).toMvPowerSeries =
      MvPowerSeries.map (frobenius R p) ((trunc' R (p • n) f).expand p) := by
      simp only [MvPolynomial.map_expand, ← expand_eq_expand p hp, map_expand]
      congr
    rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
rw :
  ∃ᶠ (m : σ →₀ ℕ) in Filter.atTop,
    Eq (α := MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
        MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
⊢ (map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p
have rw₁ : ∀ (a : σ →₀ ℕ),
  ∃ b ≥ a,
    Eq (α := MvPolynomial σ R)
      ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
        MvPolynomial σ R)
      ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: classical
  rw [eq_iff_frequently_trunc'_eq, Filter.frequently_atTop]
  intro n
  use (p • n)
  refine ⟨le_self_nsmul zero_le hp, ?_⟩
  · have : (((trunc' R (p • n) f).expand p).map (frobenius R p)).toMvPowerSeries =
      MvPowerSeries.map (frobenius R p) ((trunc' R (p • n) f).expand p) := by
      simp only [MvPolynomial.map_expand, ← expand_eq_expand p hp, map_expand]
      congr
    rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
rw :
  ∃ᶠ (m : σ →₀ ℕ) in Filter.atTop,
    Eq (α := MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
        MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
rw₁ rw₂ rw₃ rw₄ :
  ∀ (n : σ →₀ ℕ),
    ∃ b ≥ n,
      Eq (α := MvPolynomial σ R)
        ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R)
            ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
              ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
          MvPolynomial σ R)
        ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
⊢ (map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p
have h : ∀ (n : σ →₀ ℕ),
  p • n ≥ n ∧
    Eq (α := MvPolynomial σ R)
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
        MvPolynomial σ R)
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: classical
  rw [eq_iff_frequently_trunc'_eq, Filter.frequently_atTop]
  intro n
  use (p • n)
  refine ⟨le_self_nsmul zero_le hp, ?_⟩
  · have : (((trunc' R (p • n) f).expand p).map (frobenius R p)).toMvPowerSeries =
      MvPowerSeries.map (frobenius R p) ((trunc' R (p • n) f).expand p) := by
      simp only [MvPolynomial.map_expand, ← expand_eq_expand p hp, map_expand]
      congr
    rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
rw :
  ∃ᶠ (m : σ →₀ ℕ) in Filter.atTop,
    Eq (α := MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
            ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
        MvPolynomial σ R)
      ((trunc' R m : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
rw₁ rw₂ rw₃ rw₄ :
  ∀ (n : σ →₀ ℕ),
    ∃ b ≥ n,
      Eq (α := MvPolynomial σ R)
        ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R)
            ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
              ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
          MvPolynomial σ R)
        ((trunc' R b : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
h :
  ∀ (n : σ →₀ ℕ),
    p • n ≥ n ∧
      Eq (α := MvPolynomial σ R)
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
            ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
              ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
          MvPolynomial σ R)
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
⊢ (map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p
have h₁ : ∀ (n : σ →₀ ℕ),
  Eq (α := MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)) :
      MvPolynomial σ R)
    ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R) (f ^ p) : MvPolynomial σ R)
Tactic: classical
  rw [eq_iff_frequently_trunc'_eq, Filter.frequently_atTop]
  intro n
  use (p • n)
  refine ⟨le_self_nsmul zero_le hp, ?_⟩
  · have : (((trunc' R (p • n) f).expand p).map (frobenius R p)).toMvPowerSeries =
      MvPowerSeries.map (frobenius R p) ((trunc' R (p • n) f).expand p) := by
      simp only [MvPolynomial.map_expand, ← expand_eq_expand p hp, map_expand]
      congr
    rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ k
⊢ (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ (k + 1)
have succ : f ^ p ^ (k + 1) =
  (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
    ((expand (p ^ (k + 1)) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Expand (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ k
| f ^ p ^ (k + 1)
have rw : HPow.hPow (α := MvPowerSeries σ R)
  ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ k) sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
    MvPowerSeries σ R)
  p
Tactic: rw [pow_succ, pow_mul, ← n_ih]