-- 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
hf : ContinuousAt (X := MvPolynomial σ R) (Y := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S) 0
hf₁ hf₂ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
      Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
hf₃ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
      Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
hf₄ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S))
    (hn_ne : ∀ (s : σ), Set.Nonempty (α := ℕ) {n : ℕ | a s ^ n.succ ∈ I}),
    ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
      Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
hf₅ hf₆ hf₇ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
        Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
hf₈ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      let n₀ := Finsupp.ofSupportFinite n hn;
      let D := Iic n₀;
      ∀ (hD : D.Finite),
        ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
          Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
hf₉ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      let n₀ := Finsupp.ofSupportFinite n hn;
      let D := 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,
          Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
hf₁₀ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      let n₀ := Finsupp.ofSupportFinite n hn;
      let D := 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)),
        ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0,
          Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) x : S)
h :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      let n₀ := Finsupp.ofSupportFinite n hn;
      let D := 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)),
        Membership.mem (α := S) (↑I : Set S) ((eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S)
h₁ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      let n₀ := Finsupp.ofSupportFinite n hn;
      let D := 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 ∈ 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
h₂ h₃ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      let n₀ := Finsupp.ofSupportFinite n hn;
      let D := 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 ∈ 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
pos :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      let n₀ := Finsupp.ofSupportFinite n hn;
      let D := 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 ∈ 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
neg neg₁ :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Filter S) (𝓝 0) (↑I : Set S)),
    let 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),
      let n₀ := Finsupp.ofSupportFinite n hn;
      let D := 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 ∈ 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
⊢ UniformContinuous (α := MvPolynomial σ R) (β := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S)

Tactic:
classical
  apply uniformContinuous_of_continuousAt_zero
  rw [ContinuousAt, map_zero, IsLinearTopology.hasBasis_ideal.tendsto_right_iff]
  intro I hI
  let n : σ → ℕ := fun s ↦ sInf {n : ℕ | (a s) ^ n.succ ∈ I}
  have hn_ne : ∀ s, Set.Nonempty {n : ℕ | (a s) ^ n.succ ∈ I} := fun s ↦ by
    rcases ha.hpow s |>.eventually_mem hI |>.exists_forall_of_atTop with ⟨n, hn⟩
    use n
    simpa using hn n.succ n.le_succ
  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
  let n₀ : σ →₀ ℕ := .ofSupportFinite n hn
  let D := Iic n₀
  have hD : Set.Finite D := finite_Iic _
  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
  rw [← hD.eventually_all] at this
  filter_upwards [this] with p hp
  rw [coe_eval₂Hom, SetLike.mem_coe, eval₂_eq]
  apply Ideal.sum_mem
  intro d _
  by_cases hd : d ∈ D
  · exact Ideal.mul_mem_right _ _ (hp d hd)
  · apply Ideal.mul_mem_left
    simp only [mem_Iic, D, Finsupp.le_iff] at hd
    push Not at hd
    rcases hd with ⟨s, hs', hs⟩
    exact I.prod_mem hs' (I.pow_mem_of_pow_mem (Nat.sInf_mem (hn_ne s)) hs)

Premises used: ContinuousAt, Finsupp.le_iff, map_zero, Ideal.sum_mem, MvPolynomial.coe_eval₂Hom, uniformContinuous_of_continuousAt_zero, SetLike.mem_coe, Set.mem_Iic, MvPolynomial.eval₂_eq, Filter.HasBasis.tendsto_right_iff, IsLinearTopology.hasBasis_ideal, Ideal.mul_mem_left, Not