internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.EvalDomain.map
Proof state before:
case hf
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite (nhds 0)
Tactic:
exact ha.tendsto_zero
Proof state after:
no goals
Theorem: MvPowerSeries.Continuous.on_scalars
Proof state before:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
ε : MvPowerSeries σ R →+* S
hε : Continuous ⇑ε
⊢ Continuous ⇑(ε.comp (C σ R))
Tactic:
simp only [RingHom.coe_comp]
Proof state after:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
ε : MvPowerSeries σ R →+* S
hε : Continuous ⇑ε
⊢ Continuous (⇑ε ∘ ⇑(C σ R))
Theorem: MvPowerSeries.Continuous.on_scalars
Proof state before:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
ε : MvPowerSeries σ R →+* S
hε : Continuous ⇑ε
⊢ Continuous (⇑ε ∘ ⇑(C σ R))
Tactic:
exact Continuous.comp hε MvPowerSeries.continuous_C
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
⊢ f ∈ closure (Set.range ⇑coeToMvPowerSeries.ringHom)
Tactic:
rw [mem_closure_iff_nhds, nhds_pi]
Proof state after:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
⊢ ∀ t ∈ Filter.pi fun i => nhds (f i), (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
⊢ ∀ t ∈ Filter.pi fun i => nhds (f i), (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Tactic:
intro t
Proof state after:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
⊢ (t ∈ Filter.pi fun i => nhds (f i)) → (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
⊢ (t ∈ Filter.pi fun i => nhds (f i)) → (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Tactic:
rw [Filter.mem_pi]
Proof state after:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
⊢ (∃ I, I.Finite ∧ ∃ t_1, (∀ (i : σ →₀ ℕ), t_1 i ∈ nhds (f i)) ∧ I.pi t_1 ⊆ t) →
    (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
⊢ (∃ I, I.Finite ∧ ∃ t_1, (∀ (i : σ →₀ ℕ), t_1 i ∈ nhds (f i)) ∧ I.pi t_1 ⊆ t) →
    (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Tactic:
rintro ⟨I, hI, p, hp, hp_le⟩
Proof state after:
case intro.intro.intro.intro
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
⊢ (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case intro.intro.intro.intro
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
⊢ (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Tactic:
obtain ⟨n, hn⟩ := hI.bddAbove
Proof state after:
case intro.intro.intro.intro.intro
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case intro.intro.intro.intro.intro
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ (t ∩ Set.range ⇑coeToMvPowerSeries.ringHom).Nonempty
Tactic:
use f.truncFun' n
Proof state after:
case h
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ↑(truncFun' n f) ∈ t ∩ Set.range ⇑coeToMvPowerSeries.ringHom
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ↑(truncFun' n f) ∈ t ∩ Set.range ⇑coeToMvPowerSeries.ringHom
Tactic:
constructor
Proof state after:
case h.left
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ↑(truncFun' n f) ∈ t

case h.right
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ↑(truncFun' n f) ∈ Set.range ⇑coeToMvPowerSeries.ringHom
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.left
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ↑(truncFun' n f) ∈ t
Tactic:
apply hp_le
Proof state after:
case h.left.a
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ↑(truncFun' n f) ∈ I.pi p
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.left.a
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ↑(truncFun' n f) ∈ I.pi p
Tactic:
simp only [Set.mem_pi]
Proof state after:
case h.left.a
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ∀ i ∈ I, ↑(truncFun' n f) i ∈ p i
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.left.a
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ∀ i ∈ I, ↑(truncFun' n f) i ∈ p i
Tactic:
intro d hd
Proof state after:
case h.left.a
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ ↑(truncFun' n f) d ∈ p d
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.left.a
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ ↑(truncFun' n f) d ∈ p d
Tactic:
apply mem_of_mem_nhds
Proof state after:
case h.left.a.a
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ p d ∈ nhds (↑(truncFun' n f) d)
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.left.a.a
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ p d ∈ nhds (↑(truncFun' n f) d)
Tactic:
convert hp d using 2
Proof state after:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ ↑(truncFun' n f) d = f d
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ ↑(truncFun' n f) d = f d
Tactic:
change MvPolynomial.coeff d (truncFun' n f)  = MvPowerSeries.coeff R d f
Proof state after:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ MvPolynomial.coeff d (truncFun' n f) = (coeff R d) f
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ MvPolynomial.coeff d (truncFun' n f) = (coeff R d) f
Tactic:
rw [coeff_truncFun']
Proof state after:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ (if d ≤ n then (coeff R d) f else 0) = (coeff R d) f
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
d : σ →₀ ℕ
hd : d ∈ I
⊢ (if d ≤ n then (coeff R d) f else 0) = (coeff R d) f
Tactic:
rw [if_pos (hn hd)]
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_denseRange
Proof state before:
case h.right
σ : Type u_1
inst✝⁶ : DecidableEq σ
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
f : MvPowerSeries σ R
t : Set (MvPowerSeries σ R)
I : Set (σ →₀ ℕ)
hI : I.Finite
p : (σ →₀ ℕ) → Set R
hp : ∀ (i : σ →₀ ℕ), p i ∈ nhds (f i)
hp_le : I.pi p ⊆ t
n : σ →₀ ℕ
hn : n ∈ upperBounds I
⊢ ↑(truncFun' n f) ∈ Set.range ⇑coeToMvPowerSeries.ringHom
Tactic:
simp only [Set.mem_range, coeToMvPowerSeries.ringHom_apply, coe_inj, exists_eq]
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
⊢ UniformContinuous ⇑(eval₂Hom φ a)
Tactic:
apply uniformContinuous_of_continuousAt_zero
Proof state after:
case hf
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
⊢ ContinuousAt (⇑(eval₂Hom φ a)) 0
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case hf
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
⊢ ContinuousAt (⇑(eval₂Hom φ a)) 0
Tactic:
intro u hu
Proof state after:
case hf
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
hu : u ∈ nhds ((eval₂Hom φ a) 0)
⊢ u ∈ Filter.map (⇑(eval₂Hom φ a)) (nhds 0)
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case hf
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
hu : u ∈ nhds ((eval₂Hom φ a) 0)
⊢ u ∈ Filter.map (⇑(eval₂Hom φ a)) (nhds 0)
Tactic:
simp only [coe_eval₂Hom, (induced_iff_nhds_eq _).mp rfl, coe_zero,
  Filter.mem_map, Filter.mem_comap]
Proof state after:
case hf
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
hu : u ∈ nhds ((eval₂Hom φ a) 0)
⊢ ∃ t ∈ nhds 0, toMvPowerSeries ⁻¹' t ⊆ eval₂ φ a ⁻¹' u
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case hf
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
hu : u ∈ nhds ((eval₂Hom φ a) 0)
⊢ ∃ t ∈ nhds 0, toMvPowerSeries ⁻¹' t ⊆ eval₂ φ a ⁻¹' u
Tactic:
rw [map_zero, hS.mem_nhds_zero_iff] at hu
Proof state after:
case hf
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
hu : ∃ i ∈ LinearTopology.toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ u
⊢ ∃ t ∈ nhds 0, toMvPowerSeries ⁻¹' t ⊆ eval₂ φ a ⁻¹' u
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case hf
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
hu : ∃ i ∈ LinearTopology.toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ u
⊢ ∃ t ∈ nhds 0, toMvPowerSeries ⁻¹' t ⊆ eval₂ φ a ⁻¹' u
Tactic:
rcases hu with ⟨I, _, hI, hI'⟩
Proof state after:
case hf.intro.intro.intro
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformAddGroup R
inst✝⁶ : TopologicalRing R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : UniformSpace S
inst✝³ : UniformAddGroup S
inst✝² : TopologicalRing S
inst✝¹ : T2Space S
inst✝ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
u : Set S
I : Ideal S
left✝ : I ∈ LinearTopology.toIdealBasis.sets
hI : ↑I ∈ nhds 0
hI' : ↑I ≤ u
⊢ ∃ t ∈ nhds 0, toMvPowerSeries ⁻¹' t ⊆ eval₂ φ a ⁻¹' u