awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
rw :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff (p * m) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
have rw₁ : Eq (α := R)
  ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
  ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [coeff, coeff, expand, ← smul_eq_mul, ← Finsupp.smul_single, MvPowerSeries.coeff_expand_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
rw :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
rw₁ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff (p * m) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
have rw₂ : Eq (α := R)
  ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R)
      ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
    R)
  ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [coeff, coeff, expand, ← smul_eq_mul, ← Finsupp.smul_single, MvPowerSeries.coeff_expand_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
rw :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
rw₁ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₂ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff (p * m) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
have rw₃ : Eq (α := R)
  ((MvPowerSeries.coeff (Finsupp.single () (p • m)) : (a : R⟦X⟧) → R)
      ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
    R)
  ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [coeff, coeff, expand, ← smul_eq_mul, ← Finsupp.smul_single, MvPowerSeries.coeff_expand_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
rw :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
rw₁ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₂ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₃ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p • m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff (p * m) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
have rw₄ : Eq (α := R)
  ((MvPowerSeries.coeff (HSMul.hSMul (β := Unit →₀ ℕ) p (Finsupp.single () m)) : (a : R⟦X⟧) → R)
      ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
    R)
  ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [coeff, coeff, expand, ← smul_eq_mul, ← Finsupp.smul_single, MvPowerSeries.coeff_expand_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
rw :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
rw₁ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₂ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₃ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p • m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₄ :
  Eq (α := R)
    ((MvPowerSeries.coeff (HSMul.hSMul (β := Unit →₀ ℕ) p (Finsupp.single () m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff (p * m) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
have rw₅ : Eq (α := R) ((MvPowerSeries.coeff (Finsupp.single () m) : (a : MvPowerSeries Unit R) → R) φ : R)
  ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [coeff, coeff, expand, ← smul_eq_mul, ← Finsupp.smul_single, MvPowerSeries.coeff_expand_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
| ((constantCoeff : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
have rw : ((coeff 0 : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [← coeff_zero_eq_constantCoeff, ← mul_zero p, coeff_expand_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
have conv_lhs : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
Tactic: conv_lhs => rw [← coeff_zero_eq_constantCoeff, ← mul_zero p, coeff_expand_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R) (0 : R)
have h₁ : ¬p ∣ (Finsupp.single () m : (a : Unit) → ℕ) ()
Tactic: rw [coeff, expand, MvPowerSeries.coeff_expand_of_not_dvd (i := ())]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Subset (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
have rw : Subset (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
  ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
Tactic: rw [expand, MvPowerSeries.support_expand]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
rw :
  Subset (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
⊢ Subset (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
have rw₁ : Subset (α := Set (Unit →₀ ℕ)) ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
  ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
Tactic: rw [expand, MvPowerSeries.support_expand]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Eq (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
have rw : Eq (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
  ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
Tactic: rw [expand, MvPowerSeries.support_expand]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
rw :
  Eq (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
⊢ Eq (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
have rw₁ : Eq (α := Set (Unit →₀ ℕ)) ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
  ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
Tactic: rw [expand, MvPowerSeries.support_expand]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    (if p ∣ n then (coeff (n / p) : (a : R⟦X⟧) → R) φ else 0 : R)
have pos : ∀ (h : p ∣ n),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
pos :
  ∀ (h : p ∣ n),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
      ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    (if p ∣ n then (coeff (n / p) : (a : R⟦X⟧) → R) φ else 0 : R)
have neg : ∀ (h : ¬p ∣ n), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R) (0 : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
h : p ∣ n
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
have pos : ∀ (q : ℕ) (hq : n = p * q),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
Tactic: obtain ⟨q, hq⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n q : ℕ
hq : n = p * q
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
have pos : Eq (α := R) ((coeff (p * q) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
  ((coeff (p * q / p) : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [hq, coeff_expand_mul, Nat.mul_div_cancel_left _ (p.pos_of_ne_zero hp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n q : ℕ
hq : n = p * q
pos :
  Eq (α := R) ((coeff (p * q) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (p * q / p) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
have pos₁ : Eq (α := R) ((coeff q : (a : R⟦X⟧) → R) φ : R) ((coeff (p * q / p) : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [hq, coeff_expand_mul, Nat.mul_div_cancel_left _ (p.pos_of_ne_zero hp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n q : ℕ
hq : n = p * q
pos :
  Eq (α := R) ((coeff (p * q) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (p * q / p) : (a : R⟦X⟧) → R) φ : R)
pos₁ : Eq (α := R) ((coeff q : (a : R⟦X⟧) → R) φ : R) ((coeff (p * q / p) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
have pos₂ : Eq (α := R) ((coeff q : (a : R⟦X⟧) → R) φ : R) ((coeff q : (a : R⟦X⟧) → R) φ : R)
Tactic: rw [hq, coeff_expand_mul, Nat.mul_div_cancel_left _ (p.pos_of_ne_zero hp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ order.{u_2} (R := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) = p • φ.order
have simp_rw : order.{u_2} (R := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) = p • φ.order
Tactic: simp_rw [expand, order_eq_order, MvPowerSeries.order_expand p hp φ]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Expand (goal)
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
simp_rw : order.{u_2} (R := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) = p • φ.order
⊢ order.{u_2} (R := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) = p • φ.order
have simp_rw₁ : MvPowerSeries.order.{0, u_2} (σ := Unit) (R := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) =
  p • MvPowerSeries.order φ
Tactic: simp_rw [expand, order_eq_order, MvPowerSeries.order_expand p hp φ]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
⊢ gaussNorm v c f = ⨆ (i : ℕ), v ((coeff i : (a : R⟦X⟧) → R) f) * c ^ i
have refine : ∀ (x : Unit →₀ ℕ),
  v ((coeff ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) x) : (a : R⟦X⟧) → R) f) *
      HPow.hPow (β := ℕ) c ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) x : ℕ) =
    v ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f) *
      x.prod fun (x1 : Unit) (x2 : ℕ) ↦ HPow.hPow (α := ℝ) ((fun (x : Unit) ↦ c) x1) x2
Tactic: refine Equiv.iSup_congr (Finsupp.uniqueEquiv ()) ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
⊢ MvPowerSeries.HasGaussNorm v (fun (x : Unit) ↦ c) f
have suffices : Eq (α := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t)
  (Set.range fun (t : Unit →₀ ℕ) ↦
    v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)
Tactic: suffices (Set.range (fun (t : ℕ) ↦ (v (coeff t f) * c ^ t))) =
      Set.range fun t ↦ v ((MvPowerSeries.coeff t) f) * t.prod fun _ x2 ↦ c ^ x2 by
    simpa only [MvPowerSeries.HasGaussNorm, ← this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
⊢ Eq (α := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t)
    (Set.range fun (t : Unit →₀ ℕ) ↦
      v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)
have refine : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t) x ↔
    Membership.mem (γ := Set ℝ)
      (Set.range fun (t : Unit →₀ ℕ) ↦
        v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)
      x
Tactic: refine Set.ext (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t) x ↔
    Membership.mem (γ := Set ℝ)
      (Set.range fun (t : Unit →₀ ℕ) ↦
        v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)
      x
have simp : (∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x) ↔
  ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x
Tactic: simp only [Set.mem_range, Finsupp.prod_pow, Finset.univ_unique, PUnit.default_eq_unit,
    Finset.prod_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
⊢ (∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x) ↔
    ∃ (y : Unit →₀ ℕ),
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x
have mp : (∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x) →
  ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
mp :
  (∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x) →
    ∃ (y : Unit →₀ ℕ),
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x
⊢ (∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x) ↔
    ∃ (y : Unit →₀ ℕ),
      v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
          HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
        x
have mpr : (∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x) →
  ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h_1 : HasGaussNorm v c f
x : ℝ
h : ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
⊢ ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x
have mp : ∀ (y : ℕ) (hy : v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x),
  ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x
Tactic: obtain ⟨y, hy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
y : ℕ
hy : v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
⊢ ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x
have h₁ : v
      ((MvPowerSeries.coeff ((Equiv.symm (Finsupp.uniqueEquiv ()) : (a : ℕ) → Unit →₀ ℕ) y) :
          (a : MvPowerSeries Unit R) → R)
        f) *
    HPow.hPow (β := ℕ) c
      ((((Equiv.symm (Finsupp.uniqueEquiv ()) : (a : ℕ) → Unit →₀ ℕ) y : Unit →₀ ℕ) : (a : Unit) → ℕ) PUnit.unit : ℕ) =
  x
Tactic: use (Finsupp.uniqueEquiv ()).symm y
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h_1 : HasGaussNorm v c f
x : ℝ
h :
  ∃ (y : Unit →₀ ℕ),
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x
⊢ ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
have mpr : ∀ (y : Unit →₀ ℕ)
  (hy :
    v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
        HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
      x),
  ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
Tactic: obtain ⟨y, hy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x : ℝ
y : Unit →₀ ℕ
hy :
  v ((MvPowerSeries.coeff y : (a : MvPowerSeries Unit R) → R) f) *
      HPow.hPow (β := ℕ) c ((y : (a : Unit) → ℕ) PUnit.unit : ℕ) =
    x
⊢ ∃ (y : ℕ), v ((coeff y : (a : R⟦X⟧) → R) f) * c ^ y = x
have h₁ : v ((coeff ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) y) : (a : R⟦X⟧) → R) f) *
    HPow.hPow (β := ℕ) c ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) y : ℕ) =
  x
Tactic: use Finsupp.uniqueEquiv () y
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.GaussNorm (goal)
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
hbd : HasGaussNorm v c f
t : ℕ
⊢ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t ≤ gaussNorm v c f
have rw : v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t ≤ ⨆ (i : ℕ), v ((coeff i : (a : R⟦X⟧) → R) f) * c ^ i
Tactic: rw [gaussNorm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
⊢ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I ≤ I
have suffices : ∀ x ∈ I, Membership.mem (α := R⟦X⟧) I ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) x : R) : R⟦X⟧)
Tactic: suffices ∀ x ∈ I, C (constantCoeff x) ∈ I by simpa [Ideal.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
f : R⟦X⟧
hf : f ∈ I
⊢ Membership.mem (α := R⟦X⟧) I ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : R⟦X⟧)
have rw : f - HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) f) ∈ I
Tactic: rw [← sub_eq_iff_eq_add'.mpr f.eq_X_mul_shift_add_const]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ I = span (insert X ((⇑C : (a : R) → R⟦X⟧) '' S))
have rw : I = span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I
Tactic: rw [Ideal.span_insert, ← Ideal.map_span, hSI, Ideal.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : Eq (α := Ideal R) (span S) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I)
⊢ I = span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I
have refine : I ≤ span {X} ⊔ Ideal.map (F := R⟦X⟧ →+* R⟦X⟧) (RingHom.comp C constantCoeff) I
Tactic: refine le_antisymm ?_ (by simp [Ideal.span_le, hXI, map_constantCoeff_le_self_of_X_mem])
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
have pos : ∀ (hfg : I.FG), spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
Tactic: by_cases hfg : I.FG
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
pos : ∀ (hfg : I.FG), spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
⊢ spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
have neg : ∀ (hfg : ¬I.FG), spanFinrank I ≤ spanFinrank (R := R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff I) + 1
Tactic: by_cases hfg : I.FG