internlm/Lean-Github huggingface dataset:
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Tactic:
suffices h_open : IsOpen ((fun xy : α × α => xy.fst - xy.snd) ⁻¹' U₀) by
  rw [isOpen_prod_iff] at h_open
  obtain ⟨u, v, hu, hv, mem_u, mem_v, H⟩ :=
    h_open 0 0 (by simp only [Set.mem_preimage, sub_self, memU₀])
  use u ∩ v, IsOpen.inter hu hv, ⟨mem_u, mem_v⟩
  apply subset_trans _ (Set.image_subset_iff.mpr H)
  rw [image_prod]
  rintro z ⟨x, hx, y, hy, rfl⟩
  exact ⟨x, mem_of_mem_inter_left hx, y, mem_of_mem_inter_right hy, rfl⟩
Proof state after:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ IsOpen ((fun xy => xy.1 - xy.2) ⁻¹' U₀)
Theorem: Function.tendsto_zero_of_summable
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open : IsOpen ((fun xy => xy.1 - xy.2) ⁻¹' U₀)
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Tactic:
rw [isOpen_prod_iff] at h_open
Proof state after:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Theorem: Function.tendsto_zero_of_summable
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Tactic:
obtain ⟨u, v, hu, hv, mem_u, mem_v, H⟩ :=
  h_open 0 0 (by simp only [Set.mem_preimage, sub_self, memU₀])
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ ∃ U₁, IsOpen U₁ ∧ 0 ∈ U₁ ∧ U₁ - U₁ ≤ U₀
Tactic:
use u ∩ v, IsOpen.inter hu hv, ⟨mem_u, mem_v⟩
Proof state after:
case right
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ≤ U₀
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case right
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ≤ U₀
Tactic:
apply subset_trans _ (Set.image_subset_iff.mpr H)
Proof state after:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ⊆ (fun xy => xy.1 - xy.2) '' u ×ˢ v
Theorem: Function.tendsto_zero_of_summable
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ⊆ (fun xy => xy.1 - xy.2) '' u ×ˢ v
Tactic:
rw [image_prod]
Proof state after:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ⊆ image2 HSub.hSub u v
Theorem: Function.tendsto_zero_of_summable
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ u ∩ v - u ∩ v ⊆ image2 HSub.hSub u v
Tactic:
rintro z ⟨x, hx, y, hy, rfl⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
x : α
hx : x ∈ u ∩ v
y : α
hy : y ∈ u ∩ v
⊢ (fun x x_1 => x - x_1) x y ∈ image2 HSub.hSub u v
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
u v : Set α
hu : IsOpen u
hv : IsOpen v
mem_u : 0 ∈ u
mem_v : 0 ∈ v
H : u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
x : α
hx : x ∈ u ∩ v
y : α
hy : y ∈ u ∩ v
⊢ (fun x x_1 => x - x_1) x y ∈ image2 HSub.hSub u v
Tactic:
exact ⟨x, mem_of_mem_inter_left hx, y, mem_of_mem_inter_right hy, rfl⟩
Proof state after:
no goals
Theorem: Function.tendsto_zero_of_summable
Proof state before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
h_open :
  ∀ (a b : α),
    (a, b) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀ →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ (fun xy => xy.1 - xy.2) ⁻¹' U₀
⊢ (0, 0) ∈ (fun xy => xy.1 - xy.2) ⁻¹' U₀
Tactic:
simp only [Set.mem_preimage, sub_self, memU₀]
Proof state after:
no goals
Theorem: Function.tendsto_zero_of_summable
Proof state before:
case intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f : ι → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset ι), N ≤ n → ∑ b ∈ n, f b ∈ U
U₀ : Set α
hU₀ : IsOpen U₀
memU₀ : 0 ∈ U₀
⊢ IsOpen ((fun xy => xy.1 - xy.2) ⁻¹' U₀)
Tactic:
exact IsOpen.preimage continuous_sub hU₀
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.congr
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
h : f = g
⊢ StronglySummable f ↔ StronglySummable g
Tactic:
rw [h]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.of_weightedOrder_tendsto_top
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
⊢ StronglySummable f
Tactic:
intro d
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)).Finite
Theorem: MvPowerSeries.StronglySummable.of_weightedOrder_tendsto_top
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)).Finite
Tactic:
rw [HasBasis.tendsto_right_iff nhds_top_basis] at hf
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : ∀ i < ⊤, ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi i
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)).Finite
Theorem: MvPowerSeries.StronglySummable.of_weightedOrder_tendsto_top
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
hf : ∀ i < ⊤, ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi i
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) (f i)).Finite
Tactic:
specialize hf (weight w d : ℕ∞) (WithTop.coe_lt_top _)
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
⊢ (support fun i => (coeff α d) (f i)).Finite
Theorem: MvPowerSeries.StronglySummable.of_weightedOrder_tendsto_top
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
⊢ (support fun i => (coeff α d) (f i)).Finite
Tactic:
refine' hf.subset _
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
⊢ (support fun i => (coeff α d) (f i)) ⊆ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}ᶜ
Theorem: MvPowerSeries.StronglySummable.of_weightedOrder_tendsto_top
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
⊢ (support fun i => (coeff α d) (f i)) ⊆ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}ᶜ
Tactic:
intro i  h' h
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
i : ι
h' : i ∈ support fun i => (coeff α d) (f i)
h : i ∈ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}
⊢ False
Theorem: MvPowerSeries.StronglySummable.of_weightedOrder_tendsto_top
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
i : ι
h' : i ∈ support fun i => (coeff α d) (f i)
h : i ∈ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}
⊢ False
Tactic:
apply h'
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
i : ι
h' : i ∈ support fun i => (coeff α d) (f i)
h : i ∈ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}
⊢ (fun i => (coeff α d) (f i)) i = 0
Theorem: MvPowerSeries.StronglySummable.of_weightedOrder_tendsto_top
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
w : σ → ℕ
f : ι → MvPowerSeries σ α
d : σ →₀ ℕ
hf : ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)
i : ι
h' : i ∈ support fun i => (coeff α d) (f i)
h : i ∈ {x | (fun x => weightedOrder w (f x) ∈ Set.Ioi ↑((weight w) d)) x}
⊢ (fun i => (coeff α d) (f i)) i = 0
Tactic:
exact coeff_of_lt_weightedOrder w _ h
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
⊢ StronglySummable f ↔ Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
Tactic:
refine' ⟨fun hf => _, of_weightedOrder_tendsto_top w f⟩
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ Tendsto (fun i => weightedOrder w (f i)) cofinite (nhds ⊤)
Tactic:
rw [HasBasis.tendsto_right_iff nhds_top_basis]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ ∀ i < ⊤, ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi i
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ ∀ i < ⊤, ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi i
Tactic:
intro n hn
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ∞
hn : n < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi n
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ∞
hn : n < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi n
Tactic:
induction n
Proof state after:
case top
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
hn : ⊤ < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ⊤

case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
a✝ : ℕ
hn : ↑a✝ < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑a✝
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case top
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
hn : ⊤ < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ⊤
Tactic:
exfalso
Proof state after:
case top
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
hn : ⊤ < ⊤
⊢ False
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case top
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
hn : ⊤ < ⊤
⊢ False
Tactic:
exact lt_irrefl ⊤ hn
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
a✝ : ℕ
hn : ↑a✝ < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑a✝
Tactic:
rename_i n
Proof state after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑n
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
⊢ ∀ᶠ (x : ι) in cofinite, weightedOrder w (f x) ∈ Set.Ioi ↑n
Tactic:
simp only [Set.mem_Ioi, eventually_cofinite, not_lt]
Proof state after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite
Tactic:
let s := {d : σ →₀ ℕ | (weight w d) ≤ n}
Proof state after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite
Tactic:
suffices h_ss : {i | (f i).weightedOrder w ≤ some n} ⊆
    ⋃ (d : σ →₀ ℕ) (_ : d ∈ s), {i | coeff α d (f i) ≠ 0} by
  exact ((finite_of_weight_le w hw n).biUnion fun d _ => hf d).subset h_ss
Proof state after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
⊢ {i | weightedOrder w (f i) ≤ some n} ⊆ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
h_ss : {i | weightedOrder w (f i) ≤ some n} ⊆ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
⊢ {x | weightedOrder w (f x) ≤ ↑n}.Finite
Tactic:
exact ((finite_of_weight_le w hw n).biUnion fun d _ => hf d).subset h_ss
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.weightedOrder_tendsto_top_iff
Proof state before:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
⊢ {i | weightedOrder w (f i) ≤ some n} ⊆ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}
Tactic:
intro i hi
Proof state after:
case coe
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι✝ : Type ?u.15453
inst✝¹ : Semiring α
inst✝ : Finite σ
ι : Type u_3
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
f : ι → MvPowerSeries σ α
hf : StronglySummable f
n : ℕ
hn : ↑n < ⊤
s : Set (σ →₀ ℕ) := {d | (weight w) d ≤ n}
i : ι
hi : i ∈ {i | weightedOrder w (f i) ≤ some n}
⊢ i ∈ ⋃ d ∈ s, {i | (coeff α d) (f i) ≠ 0}