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 : 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
⊢ (↑m : ℕ∞) ≤ m • f.order

Tactic:
simpa [nsmul_eq_mul] using ENat.self_le_mul_right m (order_ne_zero_iff_constCoeff_eq_zero.mpr h)

Premises used: Iff.mpr, Nat.cast, MvPowerSeries.order_ne_zero_iff_constCoeff_eq_zero, nsmul_eq_mul, ENat.self_le_mul_right
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_4
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
inst_3 : T2Space R
f : MvPowerSeries σ R
h : Eq.{u_4 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → 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: MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero, Summable.tsum_pow_mul_one_sub
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_4
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
inst_3 : T2Space R
f : MvPowerSeries σ R
h : Eq.{u_4 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → 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: MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero, Summable.one_sub_mul_tsum_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
inr : ∀ (hempty : Nonempty ι), Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
⊢ Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i

Tactic:
rcases isEmpty_or_nonempty ι with hempty | hempty

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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 : IsEmpty ι
⊢ Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i

Tactic:
apply Summable.of_finite

Premises used: Summable.of_finite
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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

Tactic:
summable_iff_summable_coeff.mpr fun d ↦ summable_of_hasFiniteSupport ?_

Premises used: Iff.mpr, summable_of_hasFiniteSupport, MvPowerSeries.WithPiTopology.summable_iff_summable_coeff
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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 ι
inr :
  ∀ (d : σ →₀ ℕ),
    HasFiniteSupport.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ i, f i)
⊢ Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i

Tactic:
refine summable_iff_summable_coeff.mpr fun d ↦ summable_of_hasFiniteSupport ?_

Premises used: Iff.mpr, summable_of_hasFiniteSupport, MvPowerSeries.WithPiTopology.summable_iff_summable_coeff
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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 : σ →₀ ℕ
⊢ ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < weightedOrder w (f b)

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.MvPowerSeries.PiTopology
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)
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)
⊢ 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)

Premises used: Finsupp.weight, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)
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 ι))
⊢ HasFiniteSupport.{u_5, u_4} (M := R) fun (i : Finset ι) ↦ (coeff d : (a : MvPowerSeries σ R) → 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.MvPowerSeries.PiTopology
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)
this :
  ∀ (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
⊢ (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:
simpa
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)
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
⊢ (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:
suffices ∀ s : Finset ι, coeff d (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)
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)
⊢ (↑s : Set ι) ⊆ Set.Iio i

Tactic:
contrapose hs
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
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)
⊢ 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

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
⊢ i ≤ x

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

Premises used: Set.mem_Iio, not_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)

Tactic:
coeff_eq_zero_of_lt_weightedOrder w <| (hi x hxi).trans_le <| ?_

Premises used: LT.lt.trans_le, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
inr : weightedOrder w (f x) ≤ weightedOrder.{u_3, u_4} (R := R) w (∏ i ∈ s, f i)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ i ∈ s, f i) : R) (0 : R)

Tactic:
refine coeff_eq_zero_of_lt_weightedOrder w <| (hi x hxi).trans_le <| ?_

Premises used: LT.lt.trans_le, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
⊢ ∀ i ∈ s, 0 ≤ weightedOrder w (f i)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
⊢ weightedOrder w (f x) ≤ weightedOrder.{u_3, u_4} (R := R) w (∏ i ∈ s, f i)

Tactic:
apply le_trans (Finset.single_le_sum (by simp) hxs) (le_weightedOrder_prod w _ _)

Premises used: MvPowerSeries.le_weightedOrder_prod, Finset.single_le_sum, le_trans
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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 ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Summable (α := MvPowerSeries σ R) fun (x : Finset ι) ↦ ∏ i ∈ x, f i

Tactic:
summable_prod_of_tendsto_weightedOrder_atTop_nhds_top h

Premises used: MvPowerSeries.WithPiTopology.summable_prod_of_tendsto_weightedOrder_atTop_nhds_top
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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 (𝓝 ⊤)
⊢ Multipliable (α := MvPowerSeries σ R) fun (x : ι) ↦ 1 + f x

Tactic:
multipliable_one_add_of_summable_prod <| summable_prod_of_tendsto_weightedOrder_atTop_nhds_top h

Premises used: MvPowerSeries.WithPiTopology.summable_prod_of_tendsto_weightedOrder_atTop_nhds_top, multipliable_one_add_of_summable_prod
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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 ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Multipliable (α := MvPowerSeries σ R) fun (x : ι) ↦ 1 + f x

Tactic:
multipliable_one_add_of_summable_prod <| summable_prod_of_tendsto_order_atTop_nhds_top h

Premises used: multipliable_one_add_of_summable_prod, MvPowerSeries.WithPiTopology.summable_prod_of_tendsto_order_atTop_nhds_top
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : UniformSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
⊢ UniformContinuous (β := R) fun (f : MvPowerSeries σ R) ↦ (coeff d : (a : MvPowerSeries σ R) → R) f

Tactic:
uniformContinuous_pi.mp uniformContinuous_id d

Premises used: MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1, uniformContinuous_id, uniformContinuous_pi, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : UniformSpace R
inst_1 : CompleteSpace R
⊢ CompleteSpace (MvPowerSeries σ R)

Tactic:
Pi.complete _

Premises used: MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1, Pi.complete
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : UniformSpace R
inst_1 : AddGroup R
inst_2 : IsUniformAddGroup R
⊢ IsUniformAddGroup (MvPowerSeries σ R)

Tactic:
Pi.instIsUniformAddGroup

Premises used: MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1, Pi.instIsUniformAddGroup
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
p : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R) ((coeff x : (a : MvPowerSeries τ R) → R) (renameFun f p) : R)
    (∑ x ∈ Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯, (coeff x : (a : MvPowerSeries σ R) → R) p : R)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, MvPowerSeries.renameFun, Filter.TendstoCofinite.mapDomain, Finset.sum, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
x : σ →₀ ℕ
r : R
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)
⊢ Eq (α := MvPowerSeries τ R) (renameFun f ((monomial x : (a : R) → MvPowerSeries σ R) r))
    ((monomial (mapDomain f x) : (a : R) → MvPowerSeries τ R) r)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
x : σ →₀ ℕ
r : R
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:
simp [coeff_renameFun, coeff_monomial, eq_comm]

Premises used: _private.0.MvPowerSeries.coeff_renameFun, eq_comm, MvPowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst : TendstoCofinite f
inst_1 : Semiring R
x : σ →₀ ℕ
r : R
h 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)
⊢ Eq (α := MvPowerSeries τ R) (renameFun f ((monomial x : (a : R) → MvPowerSeries σ R) r))
    ((monomial (mapDomain f x) : (a : R) → MvPowerSeries τ R) r)

Tactic:
classical
  ext; simp [coeff_renameFun, coeff_monomial, eq_comm]

Premises used: _private.0.MvPowerSeries.coeff_renameFun, eq_comm, MvPowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
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
ht :
  {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
      mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1} ⊆
    (↑((Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯).sup fun (y : σ →₀ ℕ) ↦
          Finset.product {y} (@Finset.antidiagonal _ Finsupp.instAddMonoid _ y)) :
      Set ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)))
⊢ Set.Finite.{u_1} (α := (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))
    {p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ) |
      mapDomain f p.1 = x ∧ p.2 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ p.1}

Tactic:
apply Set.Finite.subset
    (s := ↑((TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) x).toFinset.sup
    (fun y ↦ Finset.product {y} (Finset.antidiagonal y))))

Premises used: Set.Finite.subset
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
x : τ →₀ ℕ
⊢ (↑((Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯).sup fun (y : σ →₀ ℕ) ↦
          Finset.product {y} (@Finset.antidiagonal _ Finsupp.instAddMonoid _ y)) :
      Set ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite

Tactic:
Finset.finite_toSet ..

Premises used: setOf, Finset.finite_toSet
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
x : τ →₀ ℕ
⊢ (↑((Set.Finite.toFinset (s := mapDomain f ⁻¹' {x}) ⋯).sup fun (y : σ →₀ ℕ) ↦
          Finset.product {y} (@Finset.antidiagonal _ Finsupp.instAddMonoid _ y)) :
      Set ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite

Tactic:
exact Finset.finite_toSet ..

Premises used: Finset.finite_toSet
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
x : τ →₀ ℕ
a : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)
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
⊢ 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 ((σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq σ
x : τ →₀ ℕ
a : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ 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:
grind
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq τ
x : τ →₀ ℕ
hs :
  (↑((@Finset.antidiagonal _ Finsupp.instAddMonoid _ x).sup fun (q : (τ →₀ ℕ) × (τ →₀ ℕ)) ↦
          Finset.product {q}
            (Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.1}) ⋯ ×ˢ
              Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.2}) ⋯)) :
      Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite
ht :
  {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}) ⋯} ⊆
    (↑((@Finset.antidiagonal _ Finsupp.instAddMonoid _ x).sup fun (q : (τ →₀ ℕ) × (τ →₀ ℕ)) ↦
          Finset.product {q}
            (Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.1}) ⋯ ×ˢ
              Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.2}) ⋯)) :
      Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
⊢ 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}) ⋯}

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))))

Premises used: Set.Finite.subset
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq τ
x : τ →₀ ℕ
⊢ (↑((@Finset.antidiagonal _ Finsupp.instAddMonoid _ x).sup fun (q : (τ →₀ ℕ) × (τ →₀ ℕ)) ↦
          Finset.product {q}
            (Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.1}) ⋯ ×ˢ
              Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.2}) ⋯)) :
      Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite

Tactic:
Finset.finite_toSet ..

Premises used: setOf, Finset.finite_toSet
-- Module: Mathlib.RingTheory.MvPowerSeries.Rename
Goal:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst : TendstoCofinite f
inst_1 : DecidableEq τ
x : τ →₀ ℕ
⊢ (↑((@Finset.antidiagonal _ Finsupp.instAddMonoid _ x).sup fun (q : (τ →₀ ℕ) × (τ →₀ ℕ)) ↦
          Finset.product {q}
            (Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.1}) ⋯ ×ˢ
              Set.Finite.toFinset (s := mapDomain f ⁻¹' {q.2}) ⋯)) :
      Set (((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))).Finite

Tactic:
exact Finset.finite_toSet ..

Premises used: Finset.finite_toSet