awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
⊢ (Function.support n).Finite

Tactic:
have hn : Set.Finite (n.support) := by
    change n =ᶠ[cofinite] 0
    filter_upwards [ha.tendsto_zero.eventually_mem hI] with s has
    simpa [n, Pi.zero_apply, Nat.sInf_eq_zero, or_iff_left (hn_ne s).ne_empty] using has
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
⊢ D.Finite

Tactic:
have hD : Set.Finite D := finite_Iic _
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ Tendsto (α := MvPolynomial σ R) (β := S)
    (Function.comp (β := R) (⇑φ : (a : R) → S) ((⇑(coeff d) : (a : MvPowerSeries σ R) → R) ∘ toMvPowerSeries)) (𝓝 0)
    (𝓝 0)

Tactic:
have : Tendsto (φ ∘ coeff d ∘ toMvPowerSeries) (𝓝 0) (𝓝 0) :=
      hφ.comp (continuous_coeff R d) |>.comp continuous_induced_dom |>.tendsto' 0 0 (map_zero _)
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
this :
  Tendsto (α := MvPolynomial σ R) (β := S)
    (Function.comp (β := R) (⇑φ : (a : R) → S) ((⇑(coeff d) : (a : MvPowerSeries σ R) → R) ∘ toMvPowerSeries)) (𝓝 0)
    (𝓝 0)
h :
  ∀ (f : MvPolynomial σ R)
    (hf :
      Function.comp (β := R) (⇑φ : (a : R) → S) ((⇑(coeff d) : (a : MvPowerSeries σ R) → R) ∘ toMvPowerSeries) f ∈
        (↑I : Set S)),
    Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d f) : S)
⊢ ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)

Tactic:
filter_upwards [this.eventually_mem hI] with f hf

Premises used: Filter.Tendsto.eventually_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
this :
  Tendsto (α := MvPolynomial σ R) (β := S)
    (Function.comp (β := R) (⇑φ : (a : R) → S) ((⇑(coeff d) : (a : MvPowerSeries σ R) → R) ∘ toMvPowerSeries)) (𝓝 0)
    (𝓝 0)
f : MvPolynomial σ R
hf :
  Function.comp (β := R) (⇑φ : (a : R) → S) ((⇑(coeff d) : (a : MvPowerSeries σ R) → R) ∘ toMvPowerSeries) f ∈
    (↑I : Set S)
⊢ Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d f) : S)

Tactic:
simpa using hf
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
⊢ ∀ d ∈ D, ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)

Tactic:
have : ∀ d ∈ D, ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, φ (p.coeff d) ∈ I := fun d hd ↦ by
    have : Tendsto (φ ∘ coeff d ∘ toMvPowerSeries) (𝓝 0) (𝓝 0) :=
      hφ.comp (continuous_coeff R d) |>.comp continuous_induced_dom |>.tendsto' 0 0 (map_zero _)
    filter_upwards [this.eventually_mem hI] with f hf
    simpa using hf
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ d ∈ D, ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)

Tactic:
rw [← hD.eventually_all] at this

Premises used: Set.Finite.eventually_all
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
h :
  ∀ (p : MvPolynomial σ R) (hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)),
    Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S)
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
    Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)

Tactic:
filter_upwards [this] with p hp
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
h :
  ∑ d ∈ p.support,
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
    I
⊢ Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S)

Tactic:
rw [coe_eval₂Hom, SetLike.mem_coe, eval₂_eq]

Premises used: MvPolynomial.coe_eval₂Hom, SetLike.mem_coe, MvPolynomial.eval₂_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
h :
  ∀ c ∈ p.support,
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff c p) : S)
        (∏ i ∈ c.support, HPow.hPow (β := ℕ) (a i) ((c : (a : σ) → ℕ) i : ℕ) : S) ∈
      I
⊢ ∑ d ∈ p.support,
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
    I

Tactic:
apply Ideal.sum_mem

Premises used: Ideal.sum_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h :
  d ∈ p.support →
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
      I
⊢ d ∈ p.support →
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
      I

Tactic:
_
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
pos :
  ∀ (hd : d ∈ D),
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
      I
neg :
  ∀ (hd : d ∉ D),
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
        (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
      I
⊢ HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
    I

Tactic:
by_cases hd : d ∈ D
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
hd : d ∈ D
⊢ HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
    I

Tactic:
Ideal.mul_mem_right _ _ (hp d hd)

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
hd : d ∈ D
⊢ HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
    I

Tactic:
exact Ideal.mul_mem_right _ _ (hp d hd)

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
hd : d ∉ D
neg : ∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I
⊢ HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
    I

Tactic:
apply Ideal.mul_mem_left

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
hd : d ∉ D
⊢ ¬∀ i ∈ d.support, LE.le (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) ((n₀ : (a : σ) → ℕ) i : ℕ)

Tactic:
simp only [mem_Iic, D, Finsupp.le_iff] at hd

Premises used: Finsupp.le_iff, Set.mem_Iic
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
hd : ¬∀ i ∈ d.support, LE.le (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) ((n₀ : (a : σ) → ℕ) i : ℕ)
⊢ ∃ i ∈ d.support, LT.lt (α := ℕ) ((n₀ : (a : σ) → ℕ) i : ℕ) ((d : (a : σ) → ℕ) i : ℕ)

Tactic:
push Not at hd

Premises used: Not
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
hd : ∃ i ∈ d.support, LT.lt (α := ℕ) ((n₀ : (a : σ) → ℕ) i : ℕ) ((d : (a : σ) → ℕ) i : ℕ)
neg :
  ∀ (s : σ) (hs' : s ∈ d.support) (hs : LT.lt (α := ℕ) ((n₀ : (a : σ) → ℕ) s : ℕ) ((d : (a : σ) → ℕ) s : ℕ)),
    ∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I
⊢ ∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I

Tactic:
rcases hd with ⟨s, hs', hs⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
s : σ
hs' : s ∈ d.support
hs : LT.lt (α := ℕ) ((n₀ : (a : σ) → ℕ) s : ℕ) ((d : (a : σ) → ℕ) s : ℕ)
⊢ ∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I

Tactic:
I.prod_mem hs' (I.pow_mem_of_pow_mem (Nat.sInf_mem (hn_ne s)) hs)

Premises used: Ideal.prod_mem, Set.Mem, Nat.sInf_mem, Ideal.pow_mem_of_pow_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.Evaluation
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : UniformSpace R
S : Type u_3
inst_2 : CommRing S
inst_3 : UniformSpace S
φ : R →+* S
a : σ → S
inst_4 : IsUniformAddGroup R
inst_5 : IsUniformAddGroup S
inst_6 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
I : Ideal S
hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)
n : σ → ℕ := fun (s : σ) ↦ sInf {n : ℕ | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this :
  ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i x) : S)
p : MvPolynomial σ R
hp : ∀ i ∈ D, Membership.mem (α := S) I ((φ : (a : R) → S) (MvPolynomial.coeff i p) : S)
d : σ →₀ ℕ
h : d ∈ p.support
s : σ
hs' : s ∈ d.support
hs : LT.lt (α := ℕ) ((n₀ : (a : σ) → ℕ) s : ℕ) ((d : (a : σ) → ℕ) s : ℕ)
⊢ ∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I

Tactic:
exact I.prod_mem hs' (I.pow_mem_of_pow_mem (Nat.sInf_mem (hn_ne s)) hs)

Premises used: Ideal.prod_mem