awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ (d : (a : σ) → ℕ) i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
not_le : ¬p • m ≤ p • n
neg :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
neg₁ :
  Eq.{u_3 + 1} (α := R)
    (if p • m ≤ p • n then
        (coeff (p • m) : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (MvPolynomial.coeff (p • m)
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)) :
      R)
neg₂ :
  Eq.{u_3 + 1} (α := R) 0
    (MvPolynomial.coeff (p • m)
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
neg₃ : Eq.{u_3 + 1} (α := R) 0 (MvPolynomial.coeff m ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ))
neg₄ : Eq.{u_3 + 1} (α := R) (0 : R) (if m ≤ n then (coeff m : (a : MvPowerSeries σ R) → R) φ else 0 : R)
neg₅ neg₆ : Eq.{u_3 + 1} (α := R) 0 0
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    (MvPolynomial.coeff d
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))

Tactic:
rw [coeff_trunc', ← hm, if_neg not_le, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc',
        if_neg h_le]

Premises used: MvPolynomial.coeff_expand_smul, MvPowerSeries.coeff_trunc', if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∃ (i : σ), ¬p ∣ (d : (a : σ) → ℕ) i
neg :
  ∀ (i : σ) (hi : ¬p ∣ (d : (a : σ) → ℕ) i),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      (MvPolynomial.coeff d
        ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    (MvPolynomial.coeff d
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
neg :
  Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    0
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    (MvPolynomial.coeff d
      ((MvPolynomial.expand p : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((trunc' R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) φ)))

Tactic:
rw [MvPolynomial.coeff_expand_of_not_dvd _ hi]

Premises used: MvPolynomial.coeff_expand_of_not_dvd
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
pos :
  ∀ (hd : d ≤ p • n),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      0
neg :
  ∀ (hd : ¬d ≤ p • n),
    Eq.{u_3 + 1} (α := R)
      (MvPolynomial.coeff d
        ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
      0
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    0

Tactic:
by_cases hd : d ≤ p • n
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
hd : d ≤ p • n
pos :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (0 : R)
pos₁ :
  Eq.{u_3 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R) :
      R)
    (0 : R)
pos₂ pos₃ : Eq.{u_3 + 1} (α := R) 0 0
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    0

Tactic:
rw [coeff_trunc', if_pos hd, coeff_expand_of_not_dvd _ hp _ hi]

Premises used: if_pos, MvPowerSeries.coeff_trunc', MvPowerSeries.coeff_expand_of_not_dvd
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
i : σ
hi : ¬p ∣ (d : (a : σ) → ℕ) i
hd : ¬d ≤ p • n
neg :
  Eq.{u_3 + 1} (α := R)
    (if d ≤ p • n then
        (coeff d : (a : MvPowerSeries σ R) → R)
          ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ : MvPowerSeries σ R)
      else 0 :
      R)
    (0 : R)
neg₁ neg₂ : Eq.{u_3 + 1} (α := R) 0 0
⊢ Eq.{u_3 + 1} (α := R)
    (MvPolynomial.coeff d
      ((trunc' R (p • n) : (a : MvPowerSeries σ R) → MvPolynomial σ R)
        ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) φ)))
    0

Tactic:
rw [coeff_trunc', if_neg hd]

Premises used: MvPowerSeries.coeff_trunc', if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [← expand_eq_expand p hp, trunc'_expand, ← trunc'_trunc' h]

Premises used: MvPowerSeries.trunc'_trunc', MvPowerSeries.expand_eq_expand, MvPowerSeries.trunc'_expand
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
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)
⊢ (map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p

Tactic:
rw [eq_iff_frequently_trunc'_eq, Filter.frequently_atTop]

Premises used: MvPowerSeries.eq_iff_frequently_trunc'_eq, Filter.frequently_atTop
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
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)
⊢ ∃ 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)

Tactic:
use (p • n)

Premises used: HSMul.hSMul
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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)

Tactic:
⟨le_self_nsmul zero_le hp, ?_⟩

Premises used: zero_le, le_self_nsmul, And.intro
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
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)
⊢ 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:
refine ⟨le_self_nsmul zero_le hp, ?_⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
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)
⊢ 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:
simp only [MvPolynomial.map_expand, ← expand_eq_expand p hp, map_expand]

Premises used: MvPolynomial.map_expand, MvPowerSeries.expand_eq_expand, MvPowerSeries.map_expand
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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)
    ((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:
congr
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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))

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
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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)
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)
⊢ (map (frobenius R p) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand p hp : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p

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)]

Premises used: Iff.mpr, zero_le, MvPowerSeries.eq_iff_frequently_trunc'_eq, MvPowerSeries.trunc'_expand_trunc', MvPolynomial.map_frobenius_expand, MvPowerSeries.trunc'_trunc'_pow, Filter.frequently_atTop, MvPowerSeries.trunc'_expand, le_self_nsmul, MvPolynomial.coe_pow, Nat.one_le_iff_ne_zero, expChar_ne_zero, MvPowerSeries.trunc'_map
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
⊢ (map (iterateFrobenius R p 0) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (HPow.hPow (β := ℕ) p 0) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ HPow.hPow (β := ℕ) p 0

Tactic:
simp [map_id]

Premises used: MvPowerSeries.map_id
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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
succ :
  f ^ p ^ (k + 1) =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)
⊢ (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)

Tactic:
symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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
rw :
  HPow.hPow (α := MvPowerSeries σ R)
    ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
      MvPowerSeries σ R)
    p
| f ^ p ^ (k + 1)

Tactic:
rw [pow_succ, pow_mul, ← n_ih]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
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
succ :
  HPow.hPow (α := MvPowerSeries σ R)
      ((map (iterateFrobenius R p k) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
          ((expand (p ^ k) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) :
        MvPowerSeries σ R)
      p =
    (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) =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ (k + 1)) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f)

Tactic:
conv_lhs => rw [pow_succ, pow_mul, ← n_ih]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Expand
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p : ℕ
hp : p ≠ 0
inst_1 : ExpChar R p
f : MvPowerSeries σ R
n : ℕ
zero :
  (map (iterateFrobenius R p 0) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (HPow.hPow (β := ℕ) p 0) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ HPow.hPow (β := ℕ) p 0
succ :
  ∀ (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)
⊢ (map (iterateFrobenius R p n) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      ((expand (p ^ n) ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f) =
    f ^ p ^ n

Tactic:
induction n with
  | zero => simp [map_id]
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

Premises used: MvPowerSeries.expand_mul, pow_succ, pow_mul, iterateFrobenius_add, MvPowerSeries.map_map, MvPowerSeries.map_id, iterateFrobenius_one, MvPowerSeries.map_frobenius_expand, MvPowerSeries.map_expand, pow_succ'
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
vZero : v 0 = 0
⊢ gaussNorm v c 0 = 0

Tactic:
simp [gaussNorm, vZero]

Premises used: MvPowerSeries.gaussNorm
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
hbd : HasGaussNorm v c f
t : σ →₀ ℕ
⊢ (v ((coeff t : (a : MvPowerSeries σ R) → R) f) * t.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2) ≤ gaussNorm v c f

Tactic:
apply le_ciSup hbd

Premises used: le_ciSup