internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
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
Tactic:
rw [Finset.prod_eq_prod_diff_singleton_mul 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
⊢ (∏ x ∈ d.support \ {s}, a x ^ d x) * a s ^ d s ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
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
⊢ (∏ x ∈ d.support \ {s}, a x ^ d x) * a s ^ d s ∈ I
Tactic:
apply Ideal.mul_mem_left
Proof state after:
case neg.a.intro.intro.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
s : σ
hs' : s ∈ d.support
hs : n₀ s < d s
⊢ a s ^ d s ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case neg.a.intro.intro.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
s : σ
hs' : s ∈ d.support
hs : n₀ s < d s
⊢ a s ^ d s ∈ I
Tactic:
rw [← Nat.add_sub_of_le (Nat.succ_le_of_lt hs), pow_add]
Proof state after:
case neg.a.intro.intro.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
s : σ
hs' : s ∈ d.support
hs : n₀ s < d s
⊢ a s ^ (n₀ s).succ * a s ^ (d s - (n₀ s).succ) ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case neg.a.intro.intro.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
s : σ
hs' : s ∈ d.support
hs : n₀ s < d s
⊢ a s ^ (n₀ s).succ * a s ^ (d s - (n₀ s).succ) ∈ I
Tactic:
apply Ideal.mul_mem_right
Proof state after:
case neg.a.intro.intro.a.h
σ : 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
⊢ a s ^ (n₀ s).succ ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case neg.a.intro.intro.a.h
σ : 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
⊢ a s ^ (n₀ s).succ ∈ I
Tactic:
simp only [Finsupp.coe_mk, n₀, n]
Proof state after:
case neg.a.intro.intro.a.h
σ : 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
⊢ a s ^ (sInf {n | a s ^ n.succ ∈ I}).succ ∈ I
Theorem: MvPolynomial.coeToMvPowerSeries_uniformContinuous
Proof state before:
case neg.a.intro.intro.a.h
σ : 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
⊢ a s ^ (sInf {n | a s ^ n.succ ∈ I}).succ ∈ I
Tactic:
exact Nat.sInf_mem (hn_ne s)
Proof state after:
no goals
Theorem: MvPowerSeries.coe_eval₂Hom
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
⊢ ⇑(eval₂Hom hφ ha) = eval₂ φ a
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.eval₂_coe
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
p : MvPolynomial σ R
⊢ eval₂ φ a ↑p = MvPolynomial.eval₂ φ a p
Tactic:
simp only [eval₂]
Proof state after:
σ : 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
p : MvPolynomial σ R
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) ↑p = MvPolynomial.eval₂ φ a p
Theorem: MvPowerSeries.eval₂_coe
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
p : MvPolynomial σ R
⊢ ⋯.extend (MvPolynomial.eval₂ φ a) ↑p = MvPolynomial.eval₂ φ a p
Tactic:
apply DenseInducing.extend_eq
  coeToMvPowerSeries_denseInducing
  (coeToMvPowerSeries_uniformContinuous hφ ha).continuous
Proof state after:
no goals
Theorem: MvPowerSeries.eval₂_C
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
r : R
⊢ eval₂ φ a ((C σ R) r) = φ r
Tactic:
rw [← coe_C, eval₂_coe hφ ha, MvPolynomial.eval₂_C]
Proof state after:
no goals
Theorem: MvPowerSeries.eval₂_X
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
s : σ
⊢ eval₂ φ a (X s) = a s
Tactic:
rw [← coe_X, eval₂_coe hφ ha, MvPolynomial.eval₂_X]
Proof state after:
no goals
Theorem: MvPowerSeries.hasSum_eval₂
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
f✝ : MvPowerSeries σ R
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ HasSum (fun d => φ ((coeff R d) f) * d.prod fun s e => a s ^ e) (eval₂ φ a f)
Tactic:
convert (hasSum_of_monomials_self f).map (eval₂Hom hφ ha) (continuous_eval₂ hφ ha) with d
Proof state after:
case h.e'_5.h
σ : 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
f✝ : MvPowerSeries σ R
d✝ : σ →₀ ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (φ ((coeff R d) f) * d.prod fun s e => a s ^ e) = (⇑(eval₂Hom hφ ha) ∘ fun d => (monomial R d) ((coeff R d) f)) d
Theorem: MvPowerSeries.hasSum_eval₂
Proof state before:
case h.e'_5.h
σ : 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
f✝ : MvPowerSeries σ R
d✝ : σ →₀ ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (φ ((coeff R d) f) * d.prod fun s e => a s ^ e) = (⇑(eval₂Hom hφ ha) ∘ fun d => (monomial R d) ((coeff R d) f)) d
Tactic:
simp only [Function.comp_apply, coe_eval₂Hom, ← MvPolynomial.coe_monomial, eval₂_coe hφ ha, eval₂_monomial]
Proof state after:
no goals
Theorem: MvPowerSeries.comp_eval₂
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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (⇑ε ∘ a)
Tactic:
rw [← coe_eval₂Hom hφ ha, ← RingHom.coe_comp]
Proof state after:
σ : 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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ⇑(ε.comp (eval₂Hom hφ ha)) = eval₂ (ε.comp φ) (⇑ε ∘ a)
Theorem: MvPowerSeries.comp_eval₂
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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ⇑(ε.comp (eval₂Hom hφ ha)) = eval₂ (ε.comp φ) (⇑ε ∘ a)
Tactic:
apply eval₂_unique
Proof state after:
case hε
σ : 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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ Continuous ⇑(ε.comp (eval₂Hom hφ ha))

case h
σ : 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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Theorem: MvPowerSeries.comp_eval₂
Proof state before:
case hε
σ : 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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ Continuous ⇑(ε.comp (eval₂Hom hφ ha))

case h
σ : 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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
simp only [RingHom.coe_comp]
Proof state after:
case hε
σ : 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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ Continuous (⇑ε ∘ ⇑(eval₂Hom hφ ha))

case h
σ : 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
f : MvPowerSeries σ R
d : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p