Theorem: MvPolynomial.coeToMvPowerSeries_denseRange (DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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']
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

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)]
State after:
no goals

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]
State after:
no goals