awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ 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)
have 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)
Tactic: simp_rw [HasSum, ← map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ Summable f ↔ ∀ (d : σ →₀ ℕ), Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)
have 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
Tactic: simp_rw [Summable, hasSum_iff_hasSum_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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
⊢ (∃ (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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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
⊢ ∃ (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)
have 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)
Tactic: choose a h using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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 (𝓝 ⊤)
⊢ Summable f
have inl : ∀ (hempty : IsEmpty ι), Summable f
Tactic: rcases isEmpty_or_nonempty ι with hempty | hempty
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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
⊢ Summable f
have inr : ∀ (hempty : Nonempty ι), Summable f
Tactic: rcases isEmpty_or_nonempty ι with hempty | hempty
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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 ι
⊢ Summable f
have inr : ∀ (d : σ →₀ ℕ), Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)
Tactic: rw [summable_iff_summable_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (hypothesis)
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 ι
⊢ ∀ (d : σ →₀ ℕ), Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)
have h₁ : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
Tactic: simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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 : σ →₀ ℕ
⊢ Summable.{u_2, u_3} (α := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)
have 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)
Tactic: obtain ⟨i, hi⟩ := h (Finsupp.weight w d)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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)
have inr : (support.{u_3, u_2} (M := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)) ⊆ Set.Iic i
Tactic: refine summable_of_hasFiniteSupport <| (Set.finite_Iic i).subset ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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)
⊢ (support.{u_3, u_2} (M := R) fun (i : ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f i)) ⊆ Set.Iic i
have inr : ∀ (x : ι), Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f x) : R) (0 : R) → x ≤ i
Tactic: simp_rw [Function.support_subset_iff, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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)
⊢ k ≤ i
have inr : ∀ (hk : i < k), Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f k) : R) (0 : R)
Tactic: contrapose! hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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)
⊢ Summable (α := MvPowerSeries σ R) fun (x : ℕ) ↦ f ^ x
have h₁ : Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (f ^ i).order) atTop (𝓝 ⊤)
Tactic: apply summable_of_tendsto_order_atTop_nhds_top
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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)
⊢ Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (f ^ i).order) atTop (𝓝 ⊤)
have h₁ : ∀ (n : ℕ), ∃ (a : ℕ), ∀ b ≥ a, (↑n : ℕ∞) < (f ^ b).order
Tactic: simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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
have h₁ : ∀ (n m : ℕ) (hm : m ≥ n + 1), (↑n : ℕ∞) < m • f.order
Tactic: refine fun n ↦ ⟨n + 1, fun m hm ↦ lt_of_lt_of_le ?_ (le_order_pow _)⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
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
have h₁ : (↑m : ℕ∞) ≤ m • f.order
Tactic: refine (ENat.coe_lt_coe.mpr (Nat.add_one_le_iff.mp hm.le)).trans_le ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
⊢ Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
have inl : ∀ (hempty : IsEmpty ι), Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
Tactic: rcases isEmpty_or_nonempty ι with hempty | hempty
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
inl : ∀ (hempty : IsEmpty ι), Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
⊢ Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
have inr : ∀ (hempty : Nonempty ι), Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
Tactic: rcases isEmpty_or_nonempty ι with hempty | hempty
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
have inr : ∀ (d : σ →₀ ℕ),
  HasFiniteSupport.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ i, f i)
Tactic: refine summable_iff_summable_coeff.mpr fun d ↦ summable_of_hasFiniteSupport ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (hypothesis)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ weightedOrder w (f i)) atTop (𝓝 ⊤)
hempty : Nonempty ι
d : σ →₀ ℕ
⊢ HasFiniteSupport.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ i, f i)
have h₁ : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
Tactic: simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, eventually_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
⊢ HasFiniteSupport.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ i, f i)
have inr : ∀ (i : ι) (hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)),
  HasFiniteSupport.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ i, f i)
Tactic: obtain ⟨i, hi⟩ := h (Finsupp.weight w d)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
⊢ HasFiniteSupport.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ i, f i)
have inr : (support.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ i, f i)) ⊆
  (↑(Finset.Iio i).powerset : Set (Finset ι))
Tactic: apply (Finset.Iio i).powerset.finite_toSet.subset
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
⊢ (support.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ i, f i)) ⊆
    (↑(Finset.Iio i).powerset : Set (Finset ι))
have inr : ∀ (s : Finset ι),
  Ne.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ s, f i) : R) (0 : R) → (↑s : Set ι) ⊆ Set.Iio i
Tactic: suffices ∀ s : Finset ι, coeff d (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
s : Finset ι
hs : Ne.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ s, f i) : R) (0 : R)
⊢ (↑s : Set ι) ⊆ Set.Iio i
have inr : ∀ (hs : ¬(↑s : Set ι) ⊆ Set.Iio i),
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ s, f i) : R) (0 : R)
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ s, f i) : R) (0 : R)
have inr : ∀ (x : ι) (hxs : x ∈ (↑s : Set ι)) (hxi : x ∉ Set.Iio i),
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ s, f i) : R) (0 : R)
Tactic: obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (hypothesis)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : x ∉ Set.Iio i
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ s, f i) : R) (0 : R)
have hxi₁ : i ≤ x
Tactic: rw [Set.mem_Iio, not_lt] at hxi
Cleared hypotheses: hxi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)
i : ι
hi : ∀ b ≥ i, (↑((Finsupp.weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f b)
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : i ≤ x
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ s, f i) : R) (0 : R)
have inr : weightedOrder w (f x) ≤ weightedOrder.{u_3, u_4} (R := R) w (∏ i ∈ s, f i)
Tactic: refine coeff_eq_zero_of_lt_weightedOrder w <| (hi x hxi).trans_le <| ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
x : σ →₀ ℕ
r : R
⊢ Eq (α := MvPowerSeries τ R) (renameFun f ((monomial x : (a : R) → MvPowerSeries σ R) r))
    ((monomial (mapDomain f x) : (a : R) → MvPowerSeries τ R) r)
have h : ∀ (n : τ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries τ R) → R) (renameFun f ((monomial x : (a : R) → MvPowerSeries σ R) r)) : R)
    ((coeff n : (a : MvPowerSeries τ R) → R)
        ((monomial (mapDomain f x) : (a : R) → MvPowerSeries τ R) r : MvPowerSeries τ R) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
x : σ →₀ ℕ
r : R
⊢ Eq (α := MvPowerSeries τ R) (renameFun f ((monomial x : (a : R) → MvPowerSeries σ R) r))
    ((monomial (mapDomain f x) : (a : R) → MvPowerSeries τ R) r)
have h : ∀ (n : τ →₀ ℕ),
  Eq.{u_4 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries τ R) → R) (renameFun f ((monomial x : (a : R) → MvPowerSeries σ R) r)) : R)
    ((coeff n : (a : MvPowerSeries τ R) → R)
        ((monomial (mapDomain f x) : (a : R) → MvPowerSeries τ R) r : MvPowerSeries τ R) :
      R)
Tactic: classical
  ext; simp [coeff_renameFun, coeff_monomial, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
x : τ →₀ ℕ
⊢ Set.Finite.{u_1} (α := (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
    {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
      mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1}
have hs : (↑((Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) sorry).sup fun (y : σ →₀ ℕ) ↦
        Finset.product {y} (@Finset.antidiagonal _ Finsupp.instAddMonoid _ y)) :
    Set ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite
Tactic: apply Set.Finite.subset
    (s := ↑((TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) x).toFinset.sup
    (fun y ↦ Finset.product {y} (Finset.antidiagonal y))))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
x : τ →₀ ℕ
hs :
  (↑((Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯).sup fun (y : σ →₀ ℕ) ↦
          Finset.product {y} (@Finset.antidiagonal _ Finsupp.instAddMonoid _ y)) :
      Set ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite
⊢ Set.Finite.{u_1} (α := (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
    {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
      mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1}
have ht : {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) | mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1} ⊆
  (↑((Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) sorry).sup fun (y : σ →₀ ℕ) ↦
        Finset.product {y} (@Finset.antidiagonal _ Finsupp.instAddMonoid _ y)) :
    Set ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)))
Tactic: apply Set.Finite.subset
    (s := ↑((TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) x).toFinset.sup
    (fun y ↦ Finset.product {y} (Finset.antidiagonal y))))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
x : τ →₀ ℕ
a : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ Membership.mem (γ := Set ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)))
      {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
        mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1}
      a →
    a ∈
      (↑((Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯).sup fun (y : σ →₀ ℕ) ↦
            Finset.product {y} (@Finset.antidiagonal _ Finsupp.instAddMonoid _ y)) :
        Set ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)))
have ht : mapDomain f a.1 = x →
  a.2.1 + a.2.2 = a.1 → ∃ (a_3 : σ →₀ ℕ) (b : σ →₀ ℕ), mapDomain f (a_3 + b) = x ∧ (a_3 + b, a_3, b) = a
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq τ
x : τ →₀ ℕ
⊢ Set.Finite (α := Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)))
    {p : Prod.{u_2, u_1} ((τ →₀ ℕ) × (τ →₀ ℕ)) ((σ →₀ ℕ) × (σ →₀ ℕ)) |
      p.1 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ x ∧
        p.2 ∈
          Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.1}) ⋯ ×ˢ Set.Finite.toFinset (s := mapDomain f ⁻¹' {p.1.2}) ⋯}
have hs : (↑((@Finset.antidiagonal _ Finsupp.instAddMonoid _ x).sup fun (q : (τ →₀ ℕ) × (τ →₀ ℕ)) ↦
        Finset.product {q}
          (Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.1}) sorry ×ˢ Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.2}) sorry)) :
    Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite
Tactic: apply Set.Finite.subset (s := ↑((Finset.antidiagonal x).sup (fun q ↦ Finset.product {q}
    ((TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.1).toFinset ×ˢ
      (TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.2).toFinset))))