awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
⊢ HasSum
    (fun (d : Unit →₀ ℕ) ↦
      (MvPowerSeries.monomial d : (a : R) → MvPowerSeries Unit R)
        ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R))
    f

Tactic:
MvPowerSeries.WithPiTopology.hasSum_of_monomials_self f

Premises used: MvPowerSeries.WithPiTopology.hasSum_of_monomials_self
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
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)
⊢ 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:
convert MvPowerSeries.WithPiTopology.hasSum_of_monomials_self f

Premises used: MvPowerSeries.WithPiTopology.hasSum_of_monomials_self
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
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)
⊢ 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:
simp only [LinearEquiv.coe_toEquiv, comp_apply, monomial, coeff]

Premises used: LinearEquiv.coe_toEquiv, PowerSeries.coeff, PowerSeries.monomial, Function.comp_apply
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
h h₁ : Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) = x
⊢ 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:
congr
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
h :
  Eq (α := ℕ)
    (((Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) : Unit →₀ ℕ) : (a : Unit) → ℕ)
        default :
      ℕ)
    ((x : (a : Unit) → ℕ) default : ℕ)
⊢ Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) = x

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
⊢ Eq (α := ℕ)
    (((Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) : Unit →₀ ℕ) : (a : Unit) → ℕ)
        default :
      ℕ)
    ((x : (a : Unit) → ℕ) default : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
x : Unit →₀ ℕ
h h₁ :
  Eq (α := ℕ)
    (((Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) : Unit →₀ ℕ) : (a : Unit) → ℕ)
        default :
      ℕ)
    ((x : (a : Unit) → ℕ) default : ℕ)
⊢ Finsupp.single () ((Finsupp.uniqueLinearEquiv ℕ ℕ () : (a : Unit →₀ ℕ) → ℕ) x) = x

Tactic:
{ ext; simp }
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : R⟦X⟧
⊢ f = ∑' (d : ℕ), (monomial d : (a : R) → R⟦X⟧) ((coeff d : (a : R⟦X⟧) → R) f : R)

Tactic:
(HasSum.tsum_eq (hasSum_of_monomials_self f)).symm

Premises used: PowerSeries.hasSum_of_monomials_self, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ IsRestricted c f ↔
    ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖norm (E := R) ((coeff n : (a : R⟦X⟧) → R) f : R) * c ^ n‖ < ε

Tactic:
simp [IsRestricted, NormedAddCommGroup.tendsto_atTop]

Premises used: NormedAddCommGroup.tendsto_atTop, PowerSeries.IsRestricted
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ IsRestricted c f ↔ IsRestricted |c| f

Tactic:
simp [isRestricted_iff]

Premises used: PowerSeries.IsRestricted.isRestricted_iff
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
⊢ IsRestricted.{u_1} (R := R) c 0

Tactic:
simp [IsRestricted]

Premises used: PowerSeries.IsRestricted
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
simp : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < ε
⊢ IsRestricted.{u_1} (R := R) c 1

Tactic:
simp only [isRestricted_iff, coeff_one, norm_mul, norm_pow, Real.norm_eq_abs]

Premises used: norm_pow, PowerSeries.IsRestricted.isRestricted_iff, norm_mul, PowerSeries.coeff_one, Real.norm_eq_abs
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 < ε

Tactic:
fun _ _ ↦ ⟨1, fun n hn ↦ ?_ ⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
refine : ∀ (x : ℝ), 0 < x → ∀ (n : ℕ) (hn : 1 ≤ n), |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < x
⊢ ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < ε

Tactic:
refine fun _ _ ↦ ⟨1, fun n hn ↦ ?_ ⟩
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
isFalse : ¬n = 0 → |norm.{u_1} (E := R) 0| * |c| ^ n < x
⊢ |norm.{u_1} (E := R) (if n = 0 then 1 else 0)| * |c| ^ n < x

Tactic:
split
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c x : ℝ
h : 0 < x
n : ℕ
hn : 1 ≤ n
h_1 : n = 0
⊢ |norm.{u_1} (E := R) 1| * |c| ^ n < x

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c x : ℝ
h : 0 < x
n : ℕ
hn : 1 ≤ n
h_1 : ¬n = 0
⊢ |norm.{u_1} (E := R) 0| * |c| ^ n < x

Tactic:
simpa
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
n : ℕ
a : R
simp : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n_1 : ℕ), N ≤ n_1 → ‖if n_1 = n then a else 0‖ * |c| ^ n_1 < ε
⊢ IsRestricted.{u_1} (R := R) c ((PowerSeries.monomial n : (a : R) → R⟦X⟧) a)

Tactic:
simp only [monomial_eq_mk, isRestricted_iff, coeff_mk, norm_mul, norm_pow,
    Real.norm_eq_abs, abs_norm]

Premises used: norm_pow, PowerSeries.IsRestricted.isRestricted_iff, PowerSeries.coeff_mk, norm_mul, PowerSeries.monomial_eq_mk, abs_norm, Real.norm_eq_abs
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 < ε

Tactic:
fun _ _ ↦ ⟨n + 1, fun _ _ ↦ ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
n : ℕ
a : R
refine : ∀ (x : ℝ), 0 < x → ∀ (x_2 : ℕ), n + 1 ≤ x_2 → ‖if x_2 = n then a else 0‖ * |c| ^ x_2 < x
⊢ ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n_1 : ℕ), N ≤ n_1 → ‖if n_1 = n then a else 0‖ * |c| ^ n_1 < ε

Tactic:
refine fun _ _ ↦ ⟨n + 1, fun _ _ ↦ ?_⟩
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
isFalse : ¬x_1 = n → norm.{u_1} (E := R) 0 * |c| ^ x_1 < x
⊢ ‖if x_1 = n then a else 0‖ * |c| ^ x_1 < x

Tactic:
split
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
n : ℕ
a : R
x : ℝ
h : 0 < x
x_1 : ℕ
h_1 : n + 1 ≤ x_1
h_2 : x_1 = n
⊢ ‖a‖ * |c| ^ x_1 < x

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
n : ℕ
a : R
x : ℝ
h : 0 < x
x_1 : ℕ
h_1 : n + 1 ≤ x_1
h_2 : ¬x_1 = n
⊢ norm.{u_1} (E := R) 0 * |c| ^ x_1 < x

Tactic:
simpa
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
a : R
⊢ IsRestricted.{u_1} (R := R) c ((PowerSeries.C : (a : R) → R⟦X⟧) a)

Tactic:
simpa [monomial_zero_eq_C_apply] using monomial c 0 a

Premises used: PowerSeries.IsRestricted.monomial, OfNat.ofNat, PowerSeries.monomial_zero_eq_C_apply
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f g : R⟦X⟧
hf : IsRestricted c f
hg : IsRestricted c g
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 <
              ε
⊢ IsRestricted c (f + g)

Tactic:
simp only [isRestricted_iff, map_add, norm_mul, norm_pow, Real.norm_eq_abs] at ⊢ hf hg

Premises used: norm_pow, map_add, PowerSeries.IsRestricted.isRestricted_iff, norm_mul, Real.norm_eq_abs
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 < ε
⊢ 0 < ε / 2

Tactic:
positivity
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 < ε
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 <
            ε
⊢ ∃ (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)

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ 0 < ε / 2

Tactic:
positivity
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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 <
            ε
⊢ ∃ (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)

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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 <
            ε
⊢ ∃ (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 ⊢

Premises used: abs_norm
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 <
          ε

Tactic:
⟨max fN gN, fun n hn ↦ ?_ ⟩

Premises used: Max.max, Exists.intro
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
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 < ε
⊢ ∃ (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:
refine ⟨max fN gN, fun n hn ↦ ?_ ⟩
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
grw₁ 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
⊢ ‖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:
grw [norm_add_le, add_mul]

Premises used: add_mul, norm_add_le
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
h₂ : norm (E := R) ((coeff n : (a : R⟦X⟧) → R) g : 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

Tactic:
gcongr
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 < ε / 2

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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) g : R) * |c| ^ n < ε / 2

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
⊢ ε / 2 + ε / 2 = ε

Tactic:
ring
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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
calc₂ : ε / 2 + ε / 2 = ε
⊢ ‖HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : 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

Premises used: PowerSeries.coeff, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf : IsRestricted c f
⊢ IsRestricted c (-f)

Tactic:
simpa [isRestricted_iff] using hf

Premises used: PowerSeries.IsRestricted.isRestricted_iff
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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)

Tactic:
simpa [h] using zero c

Premises used: PowerSeries.IsRestricted.zero
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
Goal:
R : Type u_1
inst : NormedRing R
c : ℝ
f : R⟦X⟧
hf : IsRestricted c f
r : R
h : ¬r = 0
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 < ε
⊢ IsRestricted c (r • f)

Tactic:
simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf

Premises used: norm_pow, PowerSeries.IsRestricted.isRestricted_iff, norm_mul, abs_norm, Real.norm_eq_abs
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 < ε
ε : ℝ
_ : 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → norm (E := R) ((coeff n : (a : R⟦X⟧) → R) (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:
_
-- Module: Mathlib.RingTheory.PowerSeries.Restricted
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 < ε
⊢ 0 < ε / ‖r‖

Tactic:
positivity