awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Nonempty ι
inr : ∀ (d : ℕ), Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)
⊢ Summable f

Tactic:
rw [summable_iff_summable_coeff]

Premises used: PowerSeries.WithPiTopology.summable_iff_summable_coeff
-- 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 : Nonempty ι
n : ℕ
⊢ ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order

Tactic:
simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop] at h

Premises used: ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop
-- 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 ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
inr :
  ∀ (i : ι) (hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order),
    Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)
⊢ Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)

Tactic:
obtain ⟨i, hi⟩ := 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⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
⊢ Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)

Tactic:
summable_of_hasFiniteSupport <| (Set.finite_Iic i).subset ?_

Premises used: Set.finite_Iic, Set.Finite.subset, summable_of_hasFiniteSupport
-- 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 ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
inr : (support.{u_2, u_1} (M := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)) ⊆ Set.Iic i
⊢ Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)

Tactic:
refine summable_of_hasFiniteSupport <| (Set.finite_Iic i).subset ?_

Premises used: Set.finite_Iic, Set.Finite.subset, summable_of_hasFiniteSupport
-- 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 ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
inr : ∀ (x : ι), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) (f x) : R) (0 : R) → x ≤ i
⊢ (support.{u_2, u_1} (M := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)) ⊆ Set.Iic i

Tactic:
simp_rw [Function.support_subset_iff, Set.mem_Iic]

Premises used: Function.support_subset_iff, Set.mem_Iic
-- 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 ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
k : ι
hk : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) (f k) : R) (0 : R)
inr : ∀ (hk : i < k), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f k) : R) (0 : R)
⊢ k ≤ i

Tactic:
contrapose! hk
-- 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 ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
k : ι
hk : i < k
⊢ (↑n : ℕ∞) < (f k).order

Tactic:
simpa using (hi k hk.le)

Premises used: LT.lt.le
-- 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 ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
k : ι
hk : i < k
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f k) : R) (0 : R)

Tactic:
exact coeff_of_lt_order _ <| by simpa using (hi k hk.le)

Premises used: PowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ Summable.{u_1, 0} (α := R⟦X⟧) fun (x : ℕ) ↦ f ^ x

Tactic:
MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero h

Premises used: MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_3
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
inst_3 : T2Space R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ (∑' (i : ℕ), f ^ i) * (1 - f) = 1

Tactic:
(summable_pow_of_constantCoeff_eq_zero h).tsum_pow_mul_one_sub

Premises used: Summable.tsum_pow_mul_one_sub, PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_3
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
inst_3 : T2Space R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ (1 - f) * ∑' (i : ℕ), f ^ i = 1

Tactic:
(summable_pow_of_constantCoeff_eq_zero h).one_sub_mul_tsum_pow

Premises used: Summable.one_sub_mul_tsum_pow, PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
inl : ∀ (hempty : IsEmpty ι), Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
inr : ∀ (hempty : Nonempty ι), Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
⊢ Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i

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 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i

Tactic:
apply Summable.of_finite

Premises used: Summable.of_finite
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i

Tactic:
(summable_iff_summable_coeff _).mpr fun n ↦ summable_of_hasFiniteSupport ?_

Premises used: Iff.mpr, summable_of_hasFiniteSupport, PowerSeries.WithPiTopology.summable_iff_summable_coeff
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
inr : ∀ (n : ℕ), HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)
⊢ Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i

Tactic:
refine (summable_iff_summable_coeff _).mpr fun n ↦ summable_of_hasFiniteSupport ?_

Premises used: Iff.mpr, summable_of_hasFiniteSupport, PowerSeries.WithPiTopology.summable_iff_summable_coeff
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
n : ℕ
⊢ ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order

Tactic:
simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, eventually_atTop] at h

Premises used: ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
inr :
  ∀ (i : ι) (hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order),
    HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)
⊢ HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)

Tactic:
obtain ⟨i, hi⟩ := h n
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
inr :
  (support.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)) ⊆
    (↑(Finset.Iio i).powerset : Set (Finset ι))
⊢ HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)

Tactic:
apply (Finset.Iio i).powerset.finite_toSet.subset

Premises used: Finset.Iio, Set.Finite.subset, Finset.powerset, Finset.finite_toSet
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
this :
  ∀ (s : Finset ι),
    Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R) → (↑s : Set ι) ⊆ Set.Iio i
⊢ (support.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)) ⊆
    (↑(Finset.Iio i).powerset : Set (Finset ι))

Tactic:
simpa
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
inr :
  ∀ (s : Finset ι),
    Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R) → (↑s : Set ι) ⊆ Set.Iio i
⊢ (support.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)) ⊆
    (↑(Finset.Iio i).powerset : Set (Finset ι))

Tactic:
suffices ∀ s : Finset ι, coeff n (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
inr : ∀ (hs : ¬(↑s : Set ι) ⊆ Set.Iio i), Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
⊢ (↑s : Set ι) ⊆ Set.Iio i

Tactic:
contrapose hs
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
inr :
  ∀ (x : ι) (hxs : x ∈ (↑s : Set ι)) (hxi : x ∉ Set.Iio i),
    Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)

Tactic:
obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : x ∉ Set.Iio i
⊢ i ≤ x

Tactic:
rw [Set.mem_Iio, not_lt] at hxi

Premises used: Set.mem_Iio, not_lt
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : i ≤ x
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)

Tactic:
coeff_of_lt_order _ <| (hi x hxi).trans_le <| le_trans ?_ (le_order_prod _ _)

Premises used: PowerSeries.coeff_of_lt_order, LT.lt.trans_le, PowerSeries.le_order_prod, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : i ≤ x
inr : (f x).order ≤ ∑ i ∈ s, (f i).order
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)

Tactic:
refine coeff_of_lt_order _ <| (hi x hxi).trans_le <| le_trans ?_ (le_order_prod _ _)

Premises used: PowerSeries.coeff_of_lt_order, LT.lt.trans_le, PowerSeries.le_order_prod, le_trans
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : i ≤ x
⊢ ∀ i ∈ s, 0 ≤ (f i).order

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : i ≤ x
⊢ (f x).order ≤ ∑ i ∈ s, (f i).order

Tactic:
apply Finset.single_le_sum (by simp) hxs

Premises used: Finset.single_le_sum
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Multipliable.{u_1, u_2} (α := R⟦X⟧) fun (x : ι) ↦ 1 + f x

Tactic:
multipliable_one_add_of_summable_prod <| summable_prod_of_tendsto_order_atTop_nhds_top _ h

Premises used: PowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top, multipliable_one_add_of_summable_prod
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
simp_rw : Multipliable.{u_2, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ 1 + -HPow.hPow (α := R⟦X⟧) X (n + 1)
⊢ Multipliable.{u_2, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (n + 1)

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h_1 : Nontrivial R
h : Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (-HPow.hPow (α := R⟦X⟧) X (i + 1)).order) atTop (𝓝 ⊤)
⊢ Multipliable.{u_2, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ 1 + -HPow.hPow (α := R⟦X⟧) X (n + 1)

Tactic:
apply multipliable_one_add_of_tendsto_order_atTop_nhds_top

Premises used: PowerSeries.WithPiTopology.multipliable_one_add_of_tendsto_order_atTop_nhds_top
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
⊢ Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (-HPow.hPow (α := R⟦X⟧) X (i + 1)).order) atTop (𝓝 ⊤)

Tactic:
ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)

Premises used: Iff.mpr, Exists.intro, ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h_1 : Nontrivial R
h : ∀ (n b : ℕ), b ≥ n → (↑n : ℕ∞) < (-HPow.hPow (α := R⟦X⟧) X (b + 1)).order
⊢ Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (-HPow.hPow (α := R⟦X⟧) X (i + 1)).order) atTop (𝓝 ⊤)

Tactic:
refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)

Premises used: Iff.mpr, Exists.intro, ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h_1 : Nontrivial R
n m : ℕ
hm : m ≥ n
h : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(m + 1) : ℕ∞)
⊢ (↑n : ℕ∞) < (-HPow.hPow (α := R⟦X⟧) X (m + 1)).order

Tactic:
rw [order_neg, order_X_pow]

Premises used: PowerSeries.order_neg, PowerSeries.order_X_pow
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h_1 : Nontrivial R
n m : ℕ
hm : m ≥ n
h : n < m + 1
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(m + 1) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
n m : ℕ
hm : m ≥ n
⊢ n < m + 1

Tactic:
Nat.lt_add_one_iff.mpr hm

Premises used: Iff.mpr, Nat.lt_add_one_iff
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
n m : ℕ
hm : m ≥ n
⊢ n < m + 1

Tactic:
exact Nat.lt_add_one_iff.mpr hm

Premises used: Iff.mpr, Nat.lt_add_one_iff
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
inst_3 : Nontrivial R
by_contra! : ∀ (h : Eq.{u_2 + 1} (α := R⟦X⟧) (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1))) 0), False
⊢ Ne.{u_2 + 1} (α := R⟦X⟧) (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1))) 0

Tactic:
by_contra! h
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
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
⊢ 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

Premises used: Iff.mp, PowerSeries.ext_iff, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
inst_3 : Nontrivial R
h_1 : Eq.{u_2 + 1} (α := R⟦X⟧) (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1))) 0
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)
⊢ False

Tactic:
simp [coeff_zero_eq_constantCoeff, (multipliable_one_sub_X_pow R).map_tprod _
    (continuous_constantCoeff R)] at h

Premises used: PowerSeries.WithPiTopology.continuous_constantCoeff, PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.WithPiTopology.multipliable_one_sub_X_pow, Multipliable.map_tprod
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : UniformSpace R
inst_1 : Semiring R
d : ℕ
⊢ UniformContinuous (β := R) fun (f : R⟦X⟧) ↦ (coeff d : (a : R⟦X⟧) → R) f

Tactic:
uniformContinuous_pi.mp uniformContinuous_id (Finsupp.single () d)

Premises used: Unit.unit, MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1, uniformContinuous_id, uniformContinuous_pi, Iff.mp, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : UniformSpace R
inst_1 : CompleteSpace R
⊢ CompleteSpace.{u_1} R⟦X⟧

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : UniformSpace R
inst_1 : AddGroup R
inst_2 : IsUniformAddGroup R
⊢ IsUniformAddGroup.{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
⊢ Continuous.{u_1, u_1} (X := R) (Y := R⟦X⟧) (⇑C : (a : R) → R⟦X⟧)

Tactic:
MvPowerSeries.WithPiTopology.continuous_C

Premises used: MvPowerSeries.WithPiTopology.continuous_C
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : R⟦X⟧
hf : IsNilpotent (R := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R)
⊢ Tendsto.{0, u_1} (β := R⟦X⟧) (fun (n : ℕ) ↦ f ^ n) atTop (nhds 0)

Tactic:
MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent hf

Premises used: IsTopologicallyNilpotent, MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ Tendsto.{0, u_1} (β := R⟦X⟧) (fun (n : ℕ) ↦ f ^ n) atTop (nhds 0)

Tactic:
MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero hf

Premises used: MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : R⟦X⟧
⊢ Tendsto.{0, u_1} (β := R⟦X⟧) (fun (n : ℕ) ↦ f ^ n) atTop (nhds 0) ↔
    IsNilpotent (R := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R)

Tactic:
MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent f

Premises used: MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, IsTopologicallyNilpotent
-- Module: Mathlib.RingTheory.PowerSeries.PiTopology
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
f : R⟦X⟧
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
⊢ HasSum (fun (d : ℕ) ↦ (monomial d : (a : R) → R⟦X⟧) ((coeff d : (a : R⟦X⟧) → R) f : R)) f

Tactic:
rw [← (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.hasSum_iff]

Premises used: Unit.unit, Equiv.hasSum_iff, Finsupp.uniqueLinearEquiv, Nat, LinearEquiv.toEquiv