awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
⊢ ∀ (d : σ →₀ ℕ), Tendsto.{0, u_2} (β := R) (fun (i : ℕ) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f ^ i)) atTop (𝓝 0)

Tactic:
exact fun d ↦ tendsto_atTop_of_eventually_const fun n hn ↦
    coeff_eq_zero_of_constantCoeff_nilpotent hm hn

Premises used: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent, tendsto_atTop_of_eventually_const
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
obtain :
  ∀ (m : ℕ) (hm : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0),
    IsTopologicallyNilpotent f
obtain₁ :
  ∀ (m : ℕ) (hm : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0) (d : σ →₀ ℕ),
    Tendsto.{0, u_2} (β := R) (fun (i : ℕ) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f ^ i)) atTop (𝓝 0)
⊢ IsTopologicallyNilpotent f

Tactic:
classical
  obtain ⟨m, hm⟩ := hf
  simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero]
  exact fun d ↦ tendsto_atTop_of_eventually_const fun n hn ↦
    coeff_eq_zero_of_constantCoeff_nilpotent hm hn

Premises used: MvPowerSeries.coeff_zero, IsTopologicallyNilpotent, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hf₁ : IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ Tendsto (β := MvPowerSeries σ R) (fun (n : ℕ) ↦ f ^ n) atTop (𝓝 0)

Tactic:
apply isTopologicallyNilpotent_of_constantCoeff_isNilpotent

Premises used: MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hf₁ : IsNilpotent.{u_2} (R := R) 0
⊢ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
rw [hf]
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ IsNilpotent.{u_2} (R := R) 0

Tactic:
IsNilpotent.zero

Premises used: IsNilpotent.zero
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ IsNilpotent.{u_2} (R := R) 0

Tactic:
exact IsNilpotent.zero

Premises used: IsNilpotent.zero
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
⊢ IsTopologicallyNilpotent f ↔ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
⟨fun H ↦ ?_, isTopologicallyNilpotent_of_constantCoeff_isNilpotent⟩

Premises used: Iff.intro, MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
refine :
  ∀ (H : IsTopologicallyNilpotent f), IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ IsTopologicallyNilpotent f ↔ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
refine ⟨fun H ↦ ?_, isTopologicallyNilpotent_of_constantCoeff_isNilpotent⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent f
⊢ IsTopologicallyNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
replace H := H.map (continuous_constantCoeff R)
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) x = 0

Tactic:
simp_rw [IsTopologicallyNilpotent, nhds_discrete, tendsto_pure] at H

Premises used: IsTopologicallyNilpotent, Filter.tendsto_pure, nhds_discrete
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
H : ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) x = 0
⊢ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
H.exists

Premises used: Filter.Eventually.exists, IsNilpotent
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
H : ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) x = 0
⊢ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
exact H.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
rw :
  ∀ (x : σ →₀ ℕ),
    HasSum (fun (i : σ →₀ ℕ) ↦ (monomial i : (a : R) → MvPowerSeries σ R) ((coeff i : (a : MvPowerSeries σ R) → R) f) x)
      (f x)
⊢ HasSum (fun (d : σ →₀ ℕ) ↦ (monomial d : (a : R) → MvPowerSeries σ R) ((coeff d : (a : MvPowerSeries σ R) → R) f)) f

Tactic:
rw [Pi.hasSum]

Premises used: Pi.hasSum
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ HasSum (fun (i : σ →₀ ℕ) ↦ (monomial i : (a : R) → MvPowerSeries σ R) ((coeff i : (a : MvPowerSeries σ R) → R) f) d)
    (f d)

Tactic:
simpa using hasSum_single d (fun d' h ↦ coeff_monomial_ne h.symm _)

Premises used: hasSum_single, Ne.symm, MvPowerSeries.coeff_monomial_ne, SummationFilter.unconditional
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : T2Space R
f : MvPowerSeries σ R
⊢ f = ∑' (d : σ →₀ ℕ), (monomial d : (a : R) → MvPowerSeries σ R) ((coeff d : (a : MvPowerSeries σ R) → R) f)

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

Premises used: HasSum.tsum_eq, MvPowerSeries.WithPiTopology.hasSum_of_monomials_self, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ R
simp_rw :
  Tendsto (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : σ →₀ ℕ),
      Tendsto.{u_3, u_2} (β := R) (fun (s : Finset ι) ↦ ((coeff d : (a : MvPowerSeries σ R) → R) (∑ b ∈ s, f b) : R))
        (SummationFilter.unconditional ι).filter (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) g) : Filter R)
⊢ HasSum f g ↔
    ∀ (d : σ →₀ ℕ),
      HasSum.{u_2, u_3} (α := R) (fun (i : ι) ↦ ((coeff d : (a : MvPowerSeries σ R) → R) (f i) : R))
        ((coeff d : (a : MvPowerSeries σ R) → R) g : R)

Tactic:
simp_rw [HasSum, ← map_sum]

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

Tactic:
apply tendsto_iff_coeff_tendsto

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

Tactic:
simp_rw [Summable, hasSum_iff_hasSum_coeff]

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

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
a : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    HasSum.{u_2, u_3} (α := R) (fun (i : ι) ↦ ((coeff d : (a : MvPowerSeries σ R) → R) (f i) : R))
      ((coeff d : (a : MvPowerSeries σ R) → R) a : R)
n : σ →₀ ℕ
⊢ ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff n : (a : MvPowerSeries σ R) → R) (f i)) a

Tactic:
⟨coeff n a, h n⟩

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

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

Tactic:
choose a h using h
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
a : (d : σ →₀ ℕ) → R
h : ∀ (d : σ →₀ ℕ), HasSum (fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)) (a d)
⊢ ∀ (d : σ →₀ ℕ),
    HasSum.{u_2, u_3} (α := R) (fun (i : ι) ↦ ((coeff d : (a : MvPowerSeries σ R) → R) (f i) : R))
      ((coeff d : (a : MvPowerSeries σ R) → R) a : R)

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
a : (d : σ →₀ ℕ) → R
h : ∀ (d : σ →₀ ℕ), HasSum (fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)) (a d)
⊢ ∃ (a : MvPowerSeries σ R),
    ∀ (d : σ →₀ ℕ),
      HasSum.{u_2, u_3} (α := R) (fun (i : ι) ↦ ((coeff d : (a : MvPowerSeries σ R) → R) (f i) : R))
        ((coeff d : (a : MvPowerSeries σ R) → R) a : R)

Tactic:
exact ⟨a, by simpa using h⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ weightedOrder w (f i)) 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.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : IsEmpty ι
⊢ Summable f

Tactic:
apply summable_empty

Premises used: summable_empty
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
inr : ∀ (d : σ →₀ ℕ), Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)
⊢ Summable f

Tactic:
rw [summable_iff_summable_coeff]

Premises used: MvPowerSeries.WithPiTopology.summable_iff_summable_coeff
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)

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.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
d : σ →₀ ℕ
inr :
  ∀ (i : ι) (hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)),
    Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)
⊢ Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)

Tactic:
obtain ⟨i, hi⟩ := h (Finsupp.weight w d)

Premises used: Finsupp.weight, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
⊢ Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → 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.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
inr : (support.{u_3, u_2} (M := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)) ⊆ Set.Iic i
⊢ Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → 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.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
inr : ∀ (x : ι), Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f x) : R) (0 : R) → x ≤ i
⊢ (support.{u_3, u_2} (M := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → 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.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
k : ι
hk : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f k) : R) (0 : R)
inr : ∀ (hk : i < k), Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f k) : R) (0 : R)
⊢ k ≤ i

Tactic:
contrapose! hk
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
k : ι
hk : i < k
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f k) : R) (0 : R)

Tactic:
coeff_eq_zero_of_lt_weightedOrder w <| hi k hk.le

Premises used: LT.lt.le, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
k : ι
hk : i < k
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f k) : R) (0 : R)

Tactic:
exact coeff_eq_zero_of_lt_weightedOrder w <| hi k hk.le

Premises used: LT.lt.le, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Summable f

Tactic:
summable_of_tendsto_weightedOrder_atTop_nhds_top h

Premises used: MvPowerSeries.WithPiTopology.summable_of_tendsto_weightedOrder_atTop_nhds_top
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
h₁ : Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (f ^ i).order) atTop (𝓝 ⊤)
⊢ Summable (α := MvPowerSeries σ R) fun (x : ℕ) ↦ f ^ x

Tactic:
apply summable_of_tendsto_order_atTop_nhds_top

Premises used: MvPowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
h₁ : ∀ (n : ℕ), ∃ (a : ℕ), ∀ b ≥ a, (↑n : ℕ∞) < (f ^ b).order
⊢ Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (f ^ i).order) atTop (𝓝 ⊤)

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

Premises used: ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ ∀ (n : ℕ), ∃ (a : ℕ), ∀ b ≥ a, (↑n : ℕ∞) < (f ^ b).order

Tactic:
fun n ↦ ⟨n + 1, fun m hm ↦ lt_of_lt_of_le ?_ (le_order_pow _)⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat, MvPowerSeries.le_order_pow, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
h₁ : ∀ (n m : ℕ) (hm : m ≥ n + 1), (↑n : ℕ∞) < m • f.order
⊢ ∀ (n : ℕ), ∃ (a : ℕ), ∀ b ≥ a, (↑n : ℕ∞) < (f ^ b).order

Tactic:
refine fun n ↦ ⟨n + 1, fun m hm ↦ lt_of_lt_of_le ?_ (le_order_pow _)⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
n m : ℕ
hm : m ≥ n + 1
⊢ (↑n : ℕ∞) < m • f.order

Tactic:
(ENat.coe_lt_coe.mpr (Nat.add_one_le_iff.mp hm.le)).trans_le ?_

Premises used: Iff.mpr, Nat.add_one_le_iff, LT.lt.trans_le, ENat.coe_lt_coe, Iff.mp, GE.ge.le
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
n m : ℕ
hm : m ≥ n + 1
h₁ : (↑m : ℕ∞) ≤ m • f.order
⊢ (↑n : ℕ∞) < m • f.order

Tactic:
refine (ENat.coe_lt_coe.mpr (Nat.add_one_le_iff.mp hm.le)).trans_le ?_

Premises used: Iff.mpr, Nat.add_one_le_iff, LT.lt.trans_le, ENat.coe_lt_coe, Iff.mp, GE.ge.le