awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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 ∈ 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
have 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
Tactic: apply Ideal.sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
have 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
Tactic: by_cases hd : d ∈ D
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
⊢ HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) (MvPolynomial.coeff d p) : S)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) : S) ∈
    I
have 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
Tactic: by_cases hd : d ∈ D
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
have neg : ∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I
Tactic: apply Ideal.mul_mem_left
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I
have hd₁ : ¬∀ i ∈ d.support, LE.le (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) ((n₀ : (a : σ) → ℕ) i : ℕ)
Tactic: simp only [mem_Iic, D, Finsupp.le_iff] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I
have hd₁ : ∃ i ∈ d.support, LT.lt (α := ℕ) ((n₀ : (a : σ) → ℕ) i : ℕ) ((d : (a : σ) → ℕ) i : ℕ)
Tactic: push Not at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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 : ℕ)
⊢ ∏ i ∈ d.support, HPow.hPow (β := ℕ) (a i) ((d : (a : σ) → ℕ) i : ℕ) ∈ I
have 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
Tactic: rcases hd with ⟨s, hs', hs⟩
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
⊢ UniformContinuous (α := MvPolynomial σ R) (β := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S)
have hf : ContinuousAt (X := MvPolynomial σ R) (Y := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S) 0
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)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
⊢ UniformContinuous (α := MvPolynomial σ R) (β := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S)
have hf₁ : ∀ (i : Ideal S),
  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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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)
⊢ UniformContinuous (α := MvPolynomial σ R) (β := S) (⇑(eval₂Hom φ a) : (a : MvPolynomial σ R) → S)
have 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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (hypothesis)
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
f : MvPolynomial σ R
⊢ eval₂ φ a (↑f : MvPowerSeries σ R) = MvPolynomial.eval₂ φ a f
have this : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)
Tactic: have : ∃ p : MvPolynomial σ R, (p : MvPowerSeries σ R) = f := ⟨f, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
f : MvPolynomial σ R
this : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)
⊢ eval₂ φ a (↑f : MvPowerSeries σ R) = MvPolynomial.eval₂ φ a f
have rw : MvPolynomial.eval₂ φ a
    (this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R))) =
  MvPolynomial.eval₂ φ a f
Tactic: rw [eval₂, dif_pos this]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
f : MvPolynomial σ R
this : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)
⊢ MvPolynomial.eval₂ φ a
      (this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R))) =
    MvPolynomial.eval₂ φ a f
have e_p : this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)) = f
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
f : MvPolynomial σ R
this : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)
⊢ this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)) = f
have e_p : (↑(this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R))) :
    MvPowerSeries σ R) =
  (↑f : MvPowerSeries σ R)
Tactic: rw [← MvPolynomial.coe_inj, this.choose_spec]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
f : MvPolynomial σ R
this : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)
e_p :
  (↑(this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R))) :
      MvPowerSeries σ R) =
    (↑f : MvPowerSeries σ R)
⊢ this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)) = f
have e_p₁ : (↑f : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)
Tactic: rw [← MvPolynomial.coe_inj, this.choose_spec]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
r : R
⊢ eval₂ φ a ((C : (a : R) → MvPowerSeries σ R) r) = (φ : (a : R) → S) r
have rw : eval₂ φ a (↑((MvPolynomial.C : (a : R) → MvPolynomial σ R) r) : MvPowerSeries σ R) = (φ : (a : R) → S) r
Tactic: rw [← coe_C, eval₂_coe, MvPolynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
r : R
rw : eval₂ φ a (↑((MvPolynomial.C : (a : R) → MvPolynomial σ R) r) : MvPowerSeries σ R) = (φ : (a : R) → S) r
⊢ eval₂ φ a ((C : (a : R) → MvPowerSeries σ R) r) = (φ : (a : R) → S) r
have rw₁ : MvPolynomial.eval₂ φ a ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r) = (φ : (a : R) → S) r
Tactic: rw [← coe_C, eval₂_coe, MvPolynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
r : R
rw : eval₂ φ a (↑((MvPolynomial.C : (a : R) → MvPolynomial σ R) r) : MvPowerSeries σ R) = (φ : (a : R) → S) r
rw₁ : MvPolynomial.eval₂ φ a ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r) = (φ : (a : R) → S) r
⊢ eval₂ φ a ((C : (a : R) → MvPowerSeries σ R) r) = (φ : (a : R) → S) r
have rw₂ : Eq.{u_3 + 1} (α := S) ((φ : (a : R) → S) r : S) ((φ : (a : R) → S) r : S)
Tactic: rw [← coe_C, eval₂_coe, MvPolynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
s : σ
⊢ eval₂ φ a (X s) = a s
have rw : eval₂ φ a (↑(MvPolynomial.X s) : MvPowerSeries σ R) = a s
Tactic: rw [← coe_X, eval₂_coe, MvPolynomial.eval₂_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
s : σ
rw : eval₂ φ a (↑(MvPolynomial.X s) : MvPowerSeries σ R) = a s
⊢ eval₂ φ a (X s) = a s
have rw₁ : MvPolynomial.eval₂ φ a (MvPolynomial.X s) = a s
Tactic: rw [← coe_X, eval₂_coe, MvPolynomial.eval₂_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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
s : σ
rw : eval₂ φ a (↑(MvPolynomial.X s) : MvPowerSeries σ R) = a s
rw₁ : MvPolynomial.eval₂ φ a (MvPolynomial.X s) = a s
⊢ eval₂ φ a (X s) = a s
have rw₂ : a s = a s
Tactic: rw [← coe_X, eval₂_coe, MvPolynomial.eval₂_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Evaluation (goal)
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 : IsTopologicalSemiring R
inst_5 : IsUniformAddGroup R
inst_6 : IsUniformAddGroup S
inst_7 : CompleteSpace S
inst_8 : T2Space S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous[inst_1.toTopologicalSpace, inst_3.toTopologicalSpace] (⇑φ : (a : R) → S)
ha : HasEval a
⊢ (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S) = eval₂ φ a
have h : ∀ (f : MvPowerSeries σ R), (eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f = eval₂ φ a f
Tactic: ext f