internlm/Lean-Github huggingface dataset:
Theorem: Finset.prod_one_add
Proof state before:
case e_f.h
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s t : Finset ι
⊢ (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1 = t.prod f
Tactic:
convert mul_one (Finset.prod t fun a => f a)
Proof state after:
case h.e'_2.h.e'_6
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s t : Finset ι
⊢ ∏ i ∈ s \ t, 1 = 1
Theorem: Finset.prod_one_add
Proof state before:
case h.e'_2.h.e'_6
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s t : Finset ι
⊢ ∏ i ∈ s \ t, 1 = 1
Tactic:
exact Finset.prod_eq_one (fun i _ => rfl)
Proof state after:
no goals
Theorem: MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
σ : Type u_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Semiring α
ι : Type u_2
f : ι → MvPowerSeries σ α
u : Filter ι
g : MvPowerSeries σ α
⊢ Filter.Tendsto f u (nhds g) ↔ ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Tactic:
rw [nhds_pi, Filter.tendsto_pi]
Proof state after:
σ : Type u_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Semiring α
ι : Type u_2
f : ι → MvPowerSeries σ α
u : Filter ι
g : MvPowerSeries σ α
⊢ (∀ (i : σ →₀ ℕ), Filter.Tendsto (fun x => f x i) u (nhds (g i))) ↔
    ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Theorem: MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
σ : Type u_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Semiring α
ι : Type u_2
f : ι → MvPowerSeries σ α
u : Filter ι
g : MvPowerSeries σ α
⊢ (∀ (i : σ →₀ ℕ), Filter.Tendsto (fun x => f x i) u (nhds (g i))) ↔
    ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Tactic:
exact forall_congr' (fun d => Iff.rfl)
Proof state after:
no goals
Theorem: MvPowerSeries.continuous_C
Proof state before:
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ Continuous ⇑(C σ α)
Tactic:
apply continuous_of_continuousAt_zero
Proof state after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ContinuousAt (⇑(C σ α)) 0
Theorem: MvPowerSeries.continuous_C
Proof state before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ContinuousAt (⇑(C σ α)) 0
Tactic:
rw [continuousAt_pi]
Proof state after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ∀ (i : σ →₀ ℕ), ContinuousAt (fun y => (C σ α) y i) 0
Theorem: MvPowerSeries.continuous_C
Proof state before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ∀ (i : σ →₀ ℕ), ContinuousAt (fun y => (C σ α) y i) 0
Tactic:
intro d
Proof state after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
⊢ ContinuousAt (fun y => (C σ α) y d) 0
Theorem: MvPowerSeries.continuous_C
Proof state before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
⊢ ContinuousAt (fun y => (C σ α) y d) 0
Tactic:
change ContinuousAt (fun y => coeff α d ((C σ α) y)) 0
Proof state after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0
Theorem: MvPowerSeries.continuous_C
Proof state before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0
Tactic:
by_cases hd : d = 0
Proof state after:
case pos
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : d = 0
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0

case neg
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0
Theorem: MvPowerSeries.continuous_C
Proof state before:
case pos
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : d = 0
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0
Tactic:
convert continuousAt_id
Proof state after:
case h.e'_5.h
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : d = 0
x✝ : α
⊢ (coeff α d) ((C σ α) x✝) = id x✝
Theorem: MvPowerSeries.continuous_C
Proof state before:
case h.e'_5.h
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : d = 0
x✝ : α
⊢ (coeff α d) ((C σ α) x✝) = id x✝
Tactic:
rw [hd, coeff_zero_C, id_eq]
Proof state after:
no goals
Theorem: MvPowerSeries.continuous_C
Proof state before:
case neg
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ContinuousAt (fun y => (coeff α d) ((C σ α) y)) 0
Tactic:
convert continuousAt_const
Proof state after:
case h.e'_5.h
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
x✝ : α
⊢ (coeff α d) ((C σ α) x✝) = ?neg.convert_6✝

case neg.convert_6
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
⊢ α
Theorem: MvPowerSeries.continuous_C
Proof state before:
case h.e'_5.h
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
x✝ : α
⊢ (coeff α d) ((C σ α) x✝) = ?neg.convert_6✝

case neg.convert_6
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
hd : ¬d = 0
⊢ α
Tactic:
rw [coeff_C, if_neg hd]
Proof state after:
no goals
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ Filter.Tendsto (fun s => X s) Filter.cofinite (nhds 0)
Tactic:
rw [tendsto_pi_nhds]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ∀ (x : σ →₀ ℕ), Filter.Tendsto (fun i => X i x) Filter.cofinite (nhds (0 x))
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ∀ (x : σ →₀ ℕ), Filter.Tendsto (fun i => X i x) Filter.cofinite (nhds (0 x))
Tactic:
intro d s hs
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
⊢ s ∈ Filter.map (fun i => X i d) Filter.cofinite
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
⊢ s ∈ Filter.map (fun i => X i d) Filter.cofinite
Tactic:
rw [Filter.mem_map, Filter.mem_cofinite, ← Set.preimage_compl]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Tactic:
by_cases h : ∃ i, d = Finsupp.single i 1
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite

case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Tactic:
. convert Set.finite_empty
  rw [Set.eq_empty_iff_forall_not_mem]
  intro x
  rw [Set.mem_preimage, Set.not_mem_compl_iff]
  convert mem_of_mem_nhds hs using 1
  rw [← coeff_eq_apply (X x) d, coeff_X, if_neg]
  rfl
  . intro h'
    apply h
    exact ⟨x, h'⟩
Proof state after:
no goals
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Tactic:
obtain ⟨i, rfl⟩ := h
Proof state after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
⊢ ((fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ).Finite
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
⊢ ((fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ).Finite
Tactic:
apply Set.Finite.subset (Set.finite_singleton i)
Proof state after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
⊢ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ ⊆ {i}
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
⊢ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ ⊆ {i}
Tactic:
intro x
Proof state after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
x : σ
⊢ x ∈ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ → x ∈ {i}
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
x : σ
⊢ x ∈ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ → x ∈ {i}
Tactic:
simp only [OfNat.ofNat, Zero.zero] at hs
Proof state after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
⊢ x ∈ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ → x ∈ {i}
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
⊢ x ∈ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ → x ∈ {i}
Tactic:
rw [Set.mem_preimage, Set.mem_compl_iff, Set.mem_singleton_iff, not_imp_comm]
Proof state after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
⊢ ¬x = i → X x (Finsupp.single i 1) ∈ s
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
⊢ ¬x = i → X x (Finsupp.single i 1) ∈ s
Tactic:
intro hx
Proof state after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ X x (Finsupp.single i 1) ∈ s
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ X x (Finsupp.single i 1) ∈ s
Tactic:
convert mem_of_mem_nhds hs
Proof state after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ X x (Finsupp.single i 1) = Zero.zero
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ X x (Finsupp.single i 1) = Zero.zero
Tactic:
rw [← coeff_eq_apply (X x) (Finsupp.single i 1), coeff_X, if_neg]
Proof state after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ 0 = Zero.zero

case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ ¬Finsupp.single i 1 = Finsupp.single x 1
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ 0 = Zero.zero

case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ ¬Finsupp.single i 1 = Finsupp.single x 1
Tactic:
rfl
Proof state after:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ ¬Finsupp.single i 1 = Finsupp.single x 1
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ ¬Finsupp.single i 1 = Finsupp.single x 1
Tactic:
simp only [Finsupp.single_eq_single_iff, Ne.symm hx, and_true, one_ne_zero, and_self,
or_self, not_false_eq_true]
Proof state after:
no goals
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Tactic:
convert Set.finite_empty
Proof state after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ (fun i => X i d) ⁻¹' sᶜ = ∅
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ (fun i => X i d) ⁻¹' sᶜ = ∅
Tactic:
rw [Set.eq_empty_iff_forall_not_mem]
Proof state after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ∀ (x : σ), x ∉ (fun i => X i d) ⁻¹' sᶜ
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ∀ (x : σ), x ∉ (fun i => X i d) ⁻¹' sᶜ
Tactic:
intro x
Proof state after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ x ∉ (fun i => X i d) ⁻¹' sᶜ
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ x ∉ (fun i => X i d) ⁻¹' sᶜ
Tactic:
rw [Set.mem_preimage, Set.not_mem_compl_iff]
Proof state after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ X x d ∈ s
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ X x d ∈ s
Tactic:
convert mem_of_mem_nhds hs using 1
Proof state after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ X x d = 0 d
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ X x d = 0 d
Tactic:
rw [← coeff_eq_apply (X x) d, coeff_X, if_neg]
Proof state after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ 0 = 0 d

case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ 0 = 0 d

case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1
Tactic:
rfl
Proof state after:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1
Tactic:
. intro h'
  apply h
  exact ⟨x, h'⟩
Proof state after:
no goals
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1
Tactic:
intro h'
Proof state after:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
h' : d = Finsupp.single x 1
⊢ False
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
h' : d = Finsupp.single x 1
⊢ False
Tactic:
apply h
Proof state after:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
h' : d = Finsupp.single x 1
⊢ ∃ i, d = Finsupp.single i 1
Theorem: MvPowerSeries.variables_tendsto_zero
Proof state before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
h' : d = Finsupp.single x 1
⊢ ∃ i, d = Finsupp.single i 1
Tactic:
exact ⟨x, h'⟩
Proof state after:
no goals
Theorem: MvPowerSeries.tendsto_pow_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : IsNilpotent ((constantCoeff σ α) f)
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
Tactic:
classical
obtain ⟨m, hm⟩ := hf
simp_rw [tendsto_iff_coeff_tendsto, coeff_zero]
exact fun d =>  tendsto_atTop_of_eventually_const fun n hn =>
  coeff_eq_zero_of_constantCoeff_nilpotent f m hm d n hn
Proof state after:
no goals
Theorem: MvPowerSeries.tendsto_pow_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : IsNilpotent ((constantCoeff σ α) f)
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
Tactic:
obtain ⟨m, hm⟩ := hf
Proof state after:
case intro
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
m : ℕ
hm : (constantCoeff σ α) f ^ m = 0
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
Theorem: MvPowerSeries.tendsto_pow_zero_of_constantCoeff_nilpotent
Proof state before:
case intro
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
m : ℕ
hm : (constantCoeff σ α) f ^ m = 0
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
Tactic:
simp_rw [tendsto_iff_coeff_tendsto, coeff_zero]
Proof state after:
case intro
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
m : ℕ
hm : (constantCoeff σ α) f ^ m = 0
⊢ ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f ^ i)) Filter.atTop (nhds 0)