internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right
σ : 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
⊢ p ∈ eval₂ φ a ⁻¹' u
Tactic:
simp only [Set.mem_preimage]
Proof state after:
case h.right
σ : 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
⊢ eval₂ φ a p ∈ u
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right
σ : 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
⊢ eval₂ φ a p ∈ u
Tactic:
apply hI'
Proof state after:
case h.right.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
⊢ eval₂ φ a p ∈ ↑I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right.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
⊢ eval₂ φ a p ∈ ↑I
Tactic:
simp only [coe_eval₂Hom, SetLike.mem_coe]
Proof state after:
case h.right.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
⊢ eval₂ φ a p ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right.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
⊢ eval₂ φ a p ∈ I
Tactic:
rw [eval₂_eq]
Proof state after:
case h.right.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 ∈ p.support, φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case h.right.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 ∈ p.support, φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Tactic:
apply Ideal.sum_mem
Proof state after:
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
⊢ ∀ c ∈ p.support, φ (MvPolynomial.coeff c p) * ∏ i ∈ c.support, a i ^ c i ∈ I
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
⊢ ∀ c ∈ p.support, φ (MvPolynomial.coeff c p) * ∏ i ∈ c.support, a i ^ c i ∈ I
Tactic:
intro d _
Proof state after:
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
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
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
Tactic:
exact Ideal.mul_mem_right _ _ (hp d hd)
Proof state after:
no goals
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
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
Tactic:
apply Ideal.mul_mem_left
Proof state after:
case neg.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
hd : d ∉ D
⊢ ∏ i ∈ d.support, a i ^ d i ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case neg.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
hd : d ∉ D
⊢ ∏ i ∈ d.support, a i ^ d i ∈ I
Tactic:
simp only [Set.mem_Iic, D, Finsupp.le_iff] at hd
Proof state after:
case neg.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
hd : ¬∀ i ∈ d.support, d i ≤ n₀ i
⊢ ∏ i ∈ d.support, a i ^ d i ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case neg.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
hd : ¬∀ i ∈ d.support, d i ≤ n₀ i
⊢ ∏ i ∈ d.support, a i ^ d i ∈ I
Tactic:
push_neg at hd
Proof state after:
case neg.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
hd : ∃ i ∈ d.support, n₀ i < d i
⊢ ∏ i ∈ d.support, a i ^ d i ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case neg.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
hd : ∃ i ∈ d.support, n₀ i < d i
⊢ ∏ i ∈ d.support, a i ^ d i ∈ I
Tactic:
rcases hd with ⟨s, hs', hs⟩
Proof state after:
case neg.a.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
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
s : σ
hs' : s ∈ d.support
hs : n₀ s < d s
⊢ ∏ i ∈ d.support, a i ^ d i ∈ I