Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right.a.a
σ : 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
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (↑p i) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Tactic:
by_cases hd : d ∈ D
Proof state after:
case pos
σ : 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
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (↑p i) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
hd : d ∈ D
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I

case neg
σ : 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
hpow : ∀ (s : σ), IsTopologicallyNilpotent (a s) := ha.hpow
tendsto_zero : (a ⁻¹' ↑I)ᶜ.Finite
hpow' : ∀ (s : σ), ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → a s ^ b ∈ I
n : σ → ℕ := fun s => sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := { support := hn.toFinset, toFun := n, mem_support_toFun := ⋯ }
D : Set (σ →₀ ℕ) := Set.Iic n₀
hD : D.Finite
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (↑p i) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
hd : d ∉ D
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I