awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
n m : ℕ
hm : m ≥ n
⊢ (↑n : ℕ∞) < (-HPow.hPow (α := R⟦X⟧) X (m + 1)).order
have h : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(m + 1) : ℕ∞)
Tactic: rw [order_neg, order_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
n m : ℕ
hm : m ≥ n
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(m + 1) : ℕ∞)
have h : n < m + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
inst_3 : Nontrivial R
h : Eq.{u_2 + 1} (α := R⟦X⟧) (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1))) 0
⊢ False
have h₁ : Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : R⟦X⟧) → R) (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1))) : R)
  ((coeff 0 : (a : R⟦X⟧) → R) 0 : R)
Tactic: obtain h := PowerSeries.ext_iff.mp h 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
⊢ HasSum (fun (d : ℕ) ↦ (monomial d : (a : R) → R⟦X⟧) ((coeff d : (a : R⟦X⟧) → R) f : R)) f
have rw : HasSum (β := Unit →₀ ℕ)
  ((fun (d : ℕ) ↦ (monomial d : (a : R) → R⟦X⟧) ((coeff d : (a : R⟦X⟧) → R) f : R)) ∘
    (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) : (a : Unit →₀ ℕ) → ℕ))
  f
Tactic: rw [← (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.hasSum_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
⊢ HasSum (β := Unit →₀ ℕ)
    ((fun (d : ℕ) ↦ (monomial d : (a : R) → R⟦X⟧) ((coeff d : (a : R⟦X⟧) → R) f : R)) ∘
      (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) : (a : Unit →₀ ℕ) → ℕ))
    f
have h : ∀ (x : Unit →₀ ℕ),
  Eq (α := R⟦X⟧)
    (((fun (d : ℕ) ↦ (monomial d : (a : R) → R⟦X⟧) ((coeff d : (a : R⟦X⟧) → R) f : R)) ∘
          (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
            (a : Unit →₀ ℕ) → ℕ))
        x :
      R⟦X⟧)
    ((MvPowerSeries.monomial x : (a : R) → MvPowerSeries Unit R)
        ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R) :
      MvPowerSeries Unit R)
Tactic: convert MvPowerSeries.WithPiTopology.hasSum_of_monomials_self f
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
⊢ Eq (α := R⟦X⟧)
    (((fun (d : ℕ) ↦ (monomial d : (a : R) → R⟦X⟧) ((coeff d : (a : R⟦X⟧) → R) f : R)) ∘
          (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
            (a : Unit →₀ ℕ) → ℕ))
        x :
      R⟦X⟧)
    ((MvPowerSeries.monomial x : (a : R) → MvPowerSeries Unit R)
        ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R) :
      MvPowerSeries Unit R)
have h : Eq (α := R⟦X⟧)
  ((MvPowerSeries.monomial (Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x)) :
        (a : R) → R⟦X⟧)
      ((MvPowerSeries.coeff (Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x)) :
            (a : R⟦X⟧) → R)
          f :
        R) :
    R⟦X⟧)
  ((MvPowerSeries.monomial x : (a : R) → MvPowerSeries Unit R)
      ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R) :
    MvPowerSeries Unit R)
Tactic: simp only [LinearEquiv.coe_toEquiv, comp_apply, monomial, coeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
⊢ Eq (α := R⟦X⟧)
    ((MvPowerSeries.monomial (Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x)) :
          (a : R) → R⟦X⟧)
        ((MvPowerSeries.coeff (Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x)) :
              (a : R⟦X⟧) → R)
            f :
          R) :
      R⟦X⟧)
    ((MvPowerSeries.monomial x : (a : R) → MvPowerSeries Unit R)
        ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R) :
      MvPowerSeries Unit R)
have h : Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) = x
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
⊢ Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) = x
have h : Eq (α := ℕ)
  (((Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) : Unit →₀ ℕ) : (a : Unit) → ℕ)
      default :
    ℕ)
  ((x : (a : Unit) → ℕ) default : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
⊢ Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) = x
have h : Eq (α := ℕ)
  (((Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) : Unit →₀ ℕ) : (a : Unit) → ℕ)
      default :
    ℕ)
  ((x : (a : Unit) → ℕ) default : ℕ)
Tactic: { ext; simp }
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
⊢ IsRestricted.{u_1} (R := R) c 1
have simp : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < ε
Tactic: simp only [isRestricted_iff, coeff_one, norm_mul, norm_pow, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
⊢ ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < ε
have refine : ∀ (x : ℝ), 0 < x → ∀ (n : ℕ) (hn : 1 ≤ n), |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < x
Tactic: refine fun _ _ ↦ ⟨1, fun n hn ↦ ?_ ⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c x : ℝ
h : 0 < x
n : ℕ
hn : 1 ≤ n
⊢ |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < x
have isTrue : n = 0 → |norm.{u_1} (E := R) 1| * |c| ^ n < x
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c x : ℝ
h : 0 < x
n : ℕ
hn : 1 ≤ n
isTrue : n = 0 → |norm.{u_1} (E := R) 1| * |c| ^ n < x
⊢ |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < x
have isFalse : ¬n = 0 → |norm.{u_1} (E := R) 0| * |c| ^ n < x
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
n : ℕ
a : R
⊢ IsRestricted.{u_1} (R := R) c ((PowerSeries.monomial n : (a : R) → R⟦X⟧) a)
have simp : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n_1 : ℕ), N ≤ n_1 → ‖if n_1 = n then a else 0‖ * |c| ^ n_1 < ε
Tactic: simp only [monomial_eq_mk, isRestricted_iff, coeff_mk, norm_mul, norm_pow,
    Real.norm_eq_abs, abs_norm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
n : ℕ
a : R
⊢ ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n_1 : ℕ), N ≤ n_1 → ‖if n_1 = n then a else 0‖ * |c| ^ n_1 < ε
have refine : ∀ (x : ℝ), 0 < x → ∀ (x_2 : ℕ), n + 1 ≤ x_2 → ‖if x_2 = n then a else 0‖ * |c| ^ x_2 < x
Tactic: refine fun _ _ ↦ ⟨n + 1, fun _ _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
n : ℕ
a : R
x : ℝ
h : 0 < x
x_1 : ℕ
h_1 : n + 1 ≤ x_1
⊢ ‖if x_1 = n then a else 0‖ * |c| ^ x_1 < x
have isTrue : x_1 = n → ‖a‖ * |c| ^ x_1 < x
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
n : ℕ
a : R
x : ℝ
h : 0 < x
x_1 : ℕ
h_1 : n + 1 ≤ x_1
isTrue : x_1 = n → ‖a‖ * |c| ^ x_1 < x
⊢ ‖if x_1 = n then a else 0‖ * |c| ^ x_1 < x
have isFalse : ¬x_1 = n → norm.{u_1} (E := R) 0 * |c| ^ x_1 < x
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : IsRestricted c f
hg : IsRestricted c g
⊢ IsRestricted c (f + g)
have simp : ∀
  (hf :
    ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε)
  (hg :
    ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε)
  (ε : ℝ),
  0 < ε →
    ∃ (N : ℕ),
      ∀ (n : ℕ),
        N ≤ n →
          |‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖| *
              |c| ^ n <
            ε
Tactic: simp only [isRestricted_iff, map_add, norm_mul, norm_pow, Real.norm_eq_abs] at ⊢ hf hg
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        |‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖| *
            |c| ^ n <
          ε
have obtain : ∀ (fN : ℕ) (hfN : ∀ (n : ℕ), fN ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε / 2),
  ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        |‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖| *
            |c| ^ n <
          ε
Tactic: obtain ⟨fN, hfN⟩ := hf (ε / 2) (by positivity)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε / 2
⊢ ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        |‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖| *
            |c| ^ n <
          ε
have obtain : ∀ (gN : ℕ) (hgN : ∀ (n : ℕ), gN ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε / 2),
  ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        |‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖| *
            |c| ^ n <
          ε
Tactic: obtain ⟨gN, hgN⟩ := hg (ε / 2) (by positivity)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε / 2
gN : ℕ
hgN : ∀ (n : ℕ), gN ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε / 2
⊢ ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        |‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖| *
            |c| ^ n <
          ε
have simp : ∀ (hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2)
  (hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2),
  ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n <
          ε
Tactic: simp only [abs_norm] at hfN hgN ⊢
Cleared hypotheses: hfN, hgN
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
⊢ ∃ (N : ℕ),
    ∀ (n : ℕ),
      N ≤ n →
        ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n <
          ε
have refine : ∀ (n : ℕ) (hn : max fN gN ≤ n),
  ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n < ε
Tactic: refine ⟨max fN gN, fun n hn ↦ ?_ ⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
n : ℕ
hn : max fN gN ≤ n
⊢ ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n ≤
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
have h₁ : 0 ≤ |c| ^ n
Tactic: grw [norm_add_le, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
n : ℕ
hn : max fN gN ≤ n
h₁ : 0 ≤ |c| ^ n
⊢ ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n ≤
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
have grw : (norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) + norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)) * |c| ^ n ≤
  norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
Tactic: grw [norm_add_le, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
n : ℕ
hn : max fN gN ≤ n
h₁ : 0 ≤ |c| ^ n
grw :
  (norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) + norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)) * |c| ^ n ≤
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
⊢ ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n ≤
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
have grw₁ : norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n ≤
  norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
Tactic: grw [norm_add_le, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
n : ℕ
hn : max fN gN ≤ n
⊢ norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n <
    ε / 2 + ε / 2
have h₁ : norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
n : ℕ
hn : max fN gN ≤ n
h₁ : norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
⊢ norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n <
    ε / 2 + ε / 2
have h₂ : norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
n : ℕ
hn : max fN gN ≤ n
⊢ ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n < ε
have calc : ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n ≤
  norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
Tactic: calc _ ≤ ‖(coeff n) f‖ * |c| ^ n + ‖(coeff n) g‖ * |c| ^ n := by grw [norm_add_le, add_mul]
       _ < ε / 2 + ε / 2 := by gcongr <;> grind
       _ = ε := by ring
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
n : ℕ
hn : max fN gN ≤ n
calc :
  ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n ≤
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
⊢ ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n < ε
have calc₁ : norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n <
  ε / 2 + ε / 2
Tactic: calc _ ≤ ‖(coeff n) f‖ * |c| ^ n + ‖(coeff n) g‖ * |c| ^ n := by grw [norm_add_le, add_mul]
       _ < ε / 2 + ε / 2 := by gcongr <;> grind
       _ = ε := by ring
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R)| * |c| ^ n < ε
hg : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R)| * |c| ^ n < ε
ε : ℝ
hε : 0 < ε
fN gN : ℕ
hfN : ∀ (n : ℕ), fN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε / 2
hgN : ∀ (n : ℕ), gN ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n < ε / 2
n : ℕ
hn : max fN gN ≤ n
calc :
  ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n ≤
    norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n
calc₁ :
  norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n +
      norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : R) * |c| ^ n <
    ε / 2 + ε / 2
⊢ ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)‖ * |c| ^ n < ε
have calc₂ : ε / 2 + ε / 2 = ε
Tactic: calc _ ≤ ‖(coeff n) f‖ * |c| ^ n + ‖(coeff n) g‖ * |c| ^ n := by grw [norm_add_le, add_mul]
       _ < ε / 2 + ε / 2 := by gcongr <;> grind
       _ = ε := by ring
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf : IsRestricted c f
r : R
h : ¬r = 0
⊢ IsRestricted c (r • f)
have simp_rw : ∀ (hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε)
  (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ n < ε
Tactic: simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
r : R
h : ¬r = 0
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
ε : ℝ
h_1 : 0 < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ n < ε
have obtain : ∀ (n : ℕ) (hn : ∀ (n_1 : ℕ), n ≤ n_1 → norm (E := R) ((coeff n_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ n_1 < ε / ‖r‖),
  ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ n < ε
Tactic: obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Restricted (goal)
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
r : R
h : ¬r = 0
hf : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * |c| ^ n < ε
ε : ℝ
h_1 : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → norm (E := R) ((coeff n_1 : (a : R⟦X⟧) → R) f : R) * |c| ^ n_1 < ε / ‖r‖
⊢ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ n < ε
have refine : ∀ (N : ℕ) (hN : n ≤ N), norm (E := R) ((coeff N : (a : R⟦X⟧) → R) (r • f) : R) * |c| ^ N < ε
Tactic: refine ⟨n, fun N hN ↦ ?_⟩