awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
_ :
  HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder
_₁ : HPow.hPow (α := R⟦X⟧) X (f * g).order.toNat * (f * g).divXPowOrder = f * g
_₂ :
  f * g =
    HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * g.divXPowOrder)
_₃ :
  HPow.hPow (α := R⟦X⟧) X f.order.toNat * f.divXPowOrder * (HPow.hPow (α := R⟦X⟧) X g.order.toNat * g.divXPowOrder) =
    f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat)
_₄ :
  f.divXPowOrder * g.divXPowOrder * HPow.hPow (α := R⟦X⟧) X (g.order.toNat + f.order.toNat) =
    HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)
⊢ HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    HPow.hPow (α := R⟦X⟧) X (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)

Tactic:
calc
    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
    _ = f * g := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) := by
        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
    _ = X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder) := by
        rw [X_pow_mul, add_comm]

Premises used: HMul.hMul, PowerSeries.divXPowOrder, PowerSeries.X, HPow.hPow, HAdd.hAdd, PowerSeries.order, ENat.toNat
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := (a : R⟦X⟧) → Multiplicative ℕ∞) (⇑orderHom : (a : R⟦X⟧) → Multiplicative ℕ∞) order

Tactic:
rfl

Premises used: dite, PowerSeries.order, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
φ : R⟦X⟧
n : ℕ
⊢ (φ ^ n).order = n • φ.order

Tactic:
map_pow orderHom φ n

Premises used: map_pow, dite, ENat, PowerSeries.order, PowerSeries.orderHom, WithTop
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
ι : Type u_3
φ : ι → R⟦X⟧
s : Finset ι
⊢ order.{u_2} (R := R) (∏ i ∈ s, φ i) = ∑ i ∈ s, (φ i).order

Tactic:
map_prod orderHom φ s

Premises used: Multiset.sum, WithTop.map₂, map_prod, WithTop.some, dite, ENat, PowerSeries.order, PowerSeries.orderHom, Finset.sum, Option.map₂, WithTop
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := (a : R⟦X⟧) → R⟦X⟧) (⇑divXPowOrderHom : (a : R⟦X⟧) → R⟦X⟧) divXPowOrder

Tactic:
rfl

Premises used: PowerSeries.divXPowOrder, PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
φ : R⟦X⟧
n : ℕ
⊢ (φ ^ n).divXPowOrder = φ.divXPowOrder ^ n

Tactic:
map_pow divXPowOrderHom φ n

Premises used: PowerSeries.divXPowOrder, map_pow, PowerSeries.mk, PowerSeries.divXPowOrderHom
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
ι : Type u_3
φ : ι → R⟦X⟧
s : Finset ι
⊢ Eq.{u_2 + 1} (α := R⟦X⟧) (divXPowOrder (∏ i ∈ s, φ i)) (∏ i ∈ s, (φ i).divXPowOrder)

Tactic:
map_prod divXPowOrderHom φ s

Premises used: Multiset.foldr, PowerSeries.divXPowOrder, Multiset.prod, map_prod, Finset.prod, PowerSeries.mk, PowerSeries.divXPowOrderHom
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
⊢ (p.toSubring T hp).order = p.order

Tactic:
eq_of_le_of_ge ?_ ?_

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
refine_1 : (p.toSubring T hp).order ≤ p.order
refine_2 : p.order ≤ (p.toSubring T hp).order
⊢ (p.toSubring T hp).order = p.order

Tactic:
refine eq_of_le_of_ge ?_ ?_

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
d : ℕ
hd : (↑d : ℕ∞) < (p.toSubring T hp).order
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) p : R) (0 : R)

Tactic:
simp [coeff_of_lt_order d hd, ← coeff_toSubring p T hp]

Premises used: PowerSeries.coeff_toSubring, PowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
⊢ (p.toSubring T hp).order ≤ p.order

Tactic:
refine le_order _ _ fun d hd => by simp [coeff_of_lt_order d hd, ← coeff_toSubring p T hp]

Premises used: PowerSeries.le_order
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
d : ℕ
hd : (↑d : ℕ∞) < p.order
⊢ Eq (α := ↥T) ((coeff d : (a : (↥T)⟦X⟧) → ↥T) (p.toSubring T hp) : ↥T) (0 : ↥T)

Tactic:
exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_of_lt_order d hd)
-- Module: Mathlib.RingTheory.PowerSeries.Order
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
⊢ p.order ≤ (p.toSubring T hp).order

Tactic:
exact le_order _ _ fun d hd => by
      exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_of_lt_order d hd)

Premises used: PowerSeries.le_order
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T0Space R
⊢ T0Space.{u_1} R⟦X⟧

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
⊢ T2Space.{u_1} R⟦X⟧

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
d : ℕ
⊢ Continuous[instTopologicalSpace R, inst] (⇑(coeff d) : (a : R⟦X⟧) → R)

Tactic:
continuous_pi_iff.mp continuous_id (Finsupp.single () d)

Premises used: Unit.unit, MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1, continuous_pi_iff, continuous_id, Iff.mp, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
⊢ Continuous[instTopologicalSpace R, inst] (⇑constantCoeff : (a : R⟦X⟧) → R)

Tactic:
coeff_zero_eq_constantCoeff (R := R) ▸ continuous_coeff R 0

Premises used: PowerSeries.WithPiTopology.continuous_coeff, Eq.rec, PowerSeries.coeff_zero_eq_constantCoeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
rw :
  (∀ (d : Unit →₀ ℕ),
      Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
        (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R)) ↔
    ∀ (d : ℕ),
      Tendsto (β := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) u
        (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)
⊢ Tendsto f u (𝓝 g) ↔
    ∀ (d : ℕ),
      Tendsto (β := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) u
        (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)

Tactic:
rw [MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto]

Premises used: MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
apply :
  ∀ (a : Unit →₀ ℕ),
    Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff a : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
        (𝓝 ((MvPowerSeries.coeff a : (a : MvPowerSeries Unit R) → R) g) : Filter R) ↔
      Tendsto (β := R)
        (fun (i : ι) ↦
          ((coeff
                  ((LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()) :
                      (a : Unit →₀ ℕ) → ℕ)
                    a) :
                (a : R⟦X⟧) → R)
              (f i) :
            R))
        u
        (𝓝
            ((coeff
                  ((LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()) :
                      (a : Unit →₀ ℕ) → ℕ)
                    a) :
                (a : R⟦X⟧) → R)
              g) :
          Filter R)
⊢ (∀ (d : Unit →₀ ℕ),
      Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
        (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R)) ↔
    ∀ (d : ℕ),
      Tendsto (β := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) u
        (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)

Tactic:
apply (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.forall_congr

Premises used: Unit.unit, Finsupp.uniqueLinearEquiv, Nat, LinearEquiv.toEquiv, Equiv.forall_congr
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
simp :
  Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) ↔
    Tendsto (β := R)
      (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)
⊢ Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) ↔
    Tendsto (β := R)
      (fun (i : ι) ↦
        ((coeff
                ((LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()) :
                    (a : Unit →₀ ℕ) → ℕ)
                  d) :
              (a : R⟦X⟧) → R)
            (f i) :
          R))
      u
      (𝓝
          ((coeff
                ((LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()) :
                    (a : Unit →₀ ℕ) → ℕ)
                  d) :
              (a : R⟦X⟧) → R)
            g) :
        Filter R)

Tactic:
simp only [LinearEquiv.coe_toEquiv, Finsupp.uniqueLinearEquiv_apply, coeff]

Premises used: LinearEquiv.coe_toEquiv, PowerSeries.coeff, Finsupp.uniqueLinearEquiv_apply
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
a :
  Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) =
    Tendsto (β := R)
      (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)
⊢ Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) ↔
    Tendsto (β := R)
      (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)

Tactic:
apply iff_of_eq

Premises used: iff_of_eq
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
a :
  Eq (α := ι → R) (fun (i : ι) ↦ (MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i)) fun (i : ι) ↦
    (MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i)
a₁ : d = Finsupp.single () ((d : (a : Unit) → ℕ) ())
⊢ Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) =
    Tendsto (β := R)
      (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)

Tactic:
congr
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
a :
  ∀ (x : ι),
    Eq (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f x) : R)
      ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f x) : R)
⊢ Eq (α := ι → R) (fun (i : ι) ↦ (MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i)) fun (i : ι) ↦
    (MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i)

Tactic:
ext _
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x : ι
a : d = Finsupp.single () ((d : (a : Unit) → ℕ) ())
⊢ Eq (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f x) : R)
    ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f x) : R)

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

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

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
a :
  Eq (α := ℕ) ((d : (a : Unit) → ℕ) default : ℕ)
    (((Finsupp.single () ((d : (a : Unit) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
⊢ d = Finsupp.single () ((d : (a : Unit) → ℕ) ())

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

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : R⟦X⟧
rw :
  ∀ (d : ℕ),
    Tendsto (β := R)
      (fun (i : ℕ) ↦ ((coeff d : (a : R⟦X⟧) → R) (↑((trunc i : (a : R⟦X⟧) → Polynomial R) f) : R⟦X⟧) : R)) atTop
      (𝓝 ((coeff d : (a : R⟦X⟧) → R) f) : Filter R)
⊢ Tendsto (fun (d : ℕ) ↦ (↑((trunc d : (a : R⟦X⟧) → Polynomial R) f) : R⟦X⟧)) atTop (𝓝 f)

Tactic:
rw [tendsto_iff_coeff_tendsto]

Premises used: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : R⟦X⟧
d n : ℕ
hdn : d < n
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (↑((trunc n : (a : R⟦X⟧) → Polynomial R) f) : R⟦X⟧) : R)
    ((coeff d : (a : R⟦X⟧) → R) f : R)

Tactic:
simp [coeff_trunc, hdn]

Premises used: PowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : R⟦X⟧
d : ℕ
⊢ Tendsto (β := R) (fun (i : ℕ) ↦ ((coeff d : (a : R⟦X⟧) → R) (↑((trunc i : (a : R⟦X⟧) → Polynomial R) f) : R⟦X⟧) : R))
    atTop (𝓝 ((coeff d : (a : R⟦X⟧) → R) f) : Filter R)

Tactic:
exact tendsto_atTop_of_eventually_const fun n (hdn : d < n) ↦ (by simp [coeff_trunc, hdn])

Premises used: tendsto_atTop_of_eventually_const
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
⊢ DenseRange.{u_1, u_1} (X := R⟦X⟧) (α := Polynomial R) Polynomial.toPowerSeries

Tactic:
fun f =>
  mem_closure_of_tendsto (tendsto_trunc_atTop R f) <| .of_forall fun _ ↦ Set.mem_range_self _

Premises used: Set.mem_range_self, Dense, Filter.Eventually.of_forall, DenseRange, PowerSeries.WithPiTopology.tendsto_trunc_atTop, DFunLike.coe, PowerSeries.trunc, mem_closure_of_tendsto
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : IsTopologicalSemiring R
⊢ IsTopologicalSemiring.{u_1} R⟦X⟧

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
⊢ IsTopologicalRing.{u_1} R⟦X⟧

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
g : R⟦X⟧
simp_rw :
  Tendsto (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : ℕ),
      Tendsto (β := R) (fun (s : Finset ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (∑ b ∈ s, f b) : R))
        (SummationFilter.unconditional ι).filter (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)
⊢ HasSum f g ↔
    ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) g : R)

Tactic:
simp_rw [HasSum, ← map_sum]

Premises used: map_sum, HasSum, SummationFilter.unconditional
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
g : R⟦X⟧
⊢ Tendsto (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : ℕ),
      Tendsto (β := R) (fun (s : Finset ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (∑ b ∈ s, f b) : R))
        (SummationFilter.unconditional ι).filter (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)

Tactic:
apply tendsto_iff_coeff_tendsto

Premises used: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
simp_rw :
  (∃ (a : R⟦X⟧),
      ∀ (d : ℕ),
        HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)) ↔
    ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
⊢ Summable f ↔ ∀ (d : ℕ), Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)

Tactic:
simp_rw [Summable, hasSum_iff_hasSum_coeff]

Premises used: PowerSeries.WithPiTopology.hasSum_iff_hasSum_coeff, Summable, SummationFilter.unconditional
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
mp :
  (∃ (a : R⟦X⟧),
      ∀ (d : ℕ),
        HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)) →
    ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
mpr :
  (∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a) →
    ∃ (a : R⟦X⟧),
      ∀ (d : ℕ),
        HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)
⊢ (∃ (a : R⟦X⟧),
      ∀ (d : ℕ),
        HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)) ↔
    ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
a : R⟦X⟧
h : ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)
n : ℕ
⊢ ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)) a

Tactic:
⟨coeff n a, h n⟩

Premises used: PowerSeries.coeff, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
a : R⟦X⟧
h : ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)
n : ℕ
⊢ ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)) a

Tactic:
exact ⟨coeff n a, h n⟩
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
h : ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
mpr :
  ∀ (a : (d : ℕ) → R) (h : ∀ (d : ℕ), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) (a d)),
    ∃ (a : R⟦X⟧),
      ∀ (d : ℕ),
        HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)
⊢ ∃ (a : R⟦X⟧),
    ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)

Tactic:
choose a h using h
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
a : (d : ℕ) → R
h : ∀ (d : ℕ), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) (a d)
⊢ ∀ (d : ℕ),
    HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) (mk a) : R)

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
a : (d : ℕ) → R
h : ∀ (d : ℕ), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) (a d)
⊢ ∃ (a : R⟦X⟧),
    ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)

Tactic:
exact ⟨mk a, by simpa using h⟩
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
inl : ∀ (hempty : IsEmpty ι), Summable f
inr : ∀ (hempty : Nonempty ι), Summable f
⊢ Summable f

Tactic:
rcases isEmpty_or_nonempty ι with hempty | hempty

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f

Tactic:
apply summable_empty

Premises used: summable_empty