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
f : MvPolynomial σ R
⊢ ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)

Tactic:
have : ∃ p : MvPolynomial σ R, (p : MvPowerSeries σ R) = f := ⟨f, rfl⟩
-- 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
f : MvPolynomial σ R
this : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)
rw :
  MvPolynomial.eval₂ φ a
      (this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R))) =
    MvPolynomial.eval₂ φ a f
⊢ eval₂ φ a (↑f : MvPowerSeries σ R) = MvPolynomial.eval₂ φ a f

Tactic:
rw [eval₂, dif_pos this]

Premises used: dif_pos, MvPowerSeries.eval₂
-- 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
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)) = f
⊢ MvPolynomial.eval₂ φ a
      (this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R))) =
    MvPolynomial.eval₂ φ a f

Tactic:
congr
-- 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
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)
e_p₁ e_p₂ : (↑f : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)
⊢ this.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = (↑f : MvPowerSeries σ R)) = f

Tactic:
rw [← MvPolynomial.coe_inj, this.choose_spec]

Premises used: Exists.choose_spec, MvPolynomial.coe_inj
-- 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
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
rw₂ rw₃ : Eq.{u_3 + 1} (α := S) ((φ : (a : R) → S) r : S) ((φ : (a : R) → S) r : S)
⊢ eval₂ φ a ((C : (a : R) → MvPowerSeries σ R) r) = (φ : (a : R) → S) r

Tactic:
rw [← coe_C, eval₂_coe, MvPolynomial.eval₂_C]

Premises used: MvPolynomial.coe_C, MvPowerSeries.eval₂_coe, MvPolynomial.eval₂_C
-- 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
s : σ
rw : eval₂ φ a (↑(MvPolynomial.X s) : MvPowerSeries σ R) = a s
rw₁ : MvPolynomial.eval₂ φ a (MvPolynomial.X s) = a s
rw₂ rw₃ : a s = a s
⊢ eval₂ φ a (X s) = a s

Tactic:
rw [← coe_X, eval₂_coe, MvPolynomial.eval₂_X]

Premises used: MvPowerSeries.eval₂_coe, MvPolynomial.coe_X, MvPolynomial.eval₂_X
-- 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 : 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
f : MvPowerSeries σ R
⊢ (eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f = IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Classical.epsilon, Set.Mem, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, Filter.lim, Filter.limUnder, IsDenseInducing.extend, Finset.sum, rfl
-- 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 : 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
h : ∀ (f : MvPowerSeries σ R), (eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f = eval₂ φ a f
⊢ (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S) = eval₂ φ a

Tactic:
ext f
-- 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 : 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
f : MvPowerSeries σ R
h :
  IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f =
    if H : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f then
      MvPolynomial.eval₂ φ a (H.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
    else IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f
⊢ (eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f = eval₂ φ a f

Tactic:
simp only [eval₂Hom_eq_extend, eval₂]

Premises used: MvPowerSeries.eval₂Hom_eq_extend, MvPowerSeries.eval₂
-- 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 : 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
f : MvPowerSeries σ R
pos :
  ∀ (h : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f),
    IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f =
      MvPolynomial.eval₂ φ a (h.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
neg :
  ∀ (h : ¬∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f),
    IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f = IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f
⊢ IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f =
    if H : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f then
      MvPolynomial.eval₂ φ a (H.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))
    else IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f

Tactic:
split_ifs with h
-- 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 : 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
f : MvPowerSeries σ R
h : ∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f
pos :
  ∀ (p : MvPolynomial σ R),
    IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) (↑p : MvPowerSeries σ R) =
      MvPolynomial.eval₂ φ a
        (Exists.choose (p := fun (p_1 : MvPolynomial σ R) ↦ (↑p_1 : MvPowerSeries σ R) = (↑p : MvPowerSeries σ R)) ⋯)
⊢ IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f =
    MvPolynomial.eval₂ φ a (h.choose (p := fun (p : MvPolynomial σ R) ↦ (↑p : MvPowerSeries σ R) = f))

Tactic:
obtain ⟨p, rfl⟩ := h

Premises used: rfl
-- 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 : 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
p : MvPolynomial σ R
⊢ IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ φ a
      (Exists.choose (p := fun (p_1 : MvPolynomial σ R) ↦ (↑p_1 : MvPowerSeries σ R) = (↑p : MvPowerSeries σ R)) ⋯)

Tactic:
simpa [MvPolynomial.coe_eval₂Hom] using
      toMvPowerSeries_isDenseInducing.extend_eq
        (toMvPowerSeries_uniformContinuous hφ ha).continuous p

Premises used: MvPolynomial.toMvPowerSeries_uniformContinuous, MvPolynomial.toMvPowerSeries_isDenseInducing, MvPolynomial.coe_eval₂Hom, UniformContinuous.continuous, IsDenseInducing.extend_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 : 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
f : MvPowerSeries σ R
h : ¬∃ (p : MvPolynomial σ R), (↑p : MvPowerSeries σ R) = f
neg neg₁ :
  Eq.{u_3 + 1} (α := S) ((eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f : S)
    ((eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f : S)
⊢ IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f = IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f

Tactic:
rw [← eval₂Hom_eq_extend hφ ha]

Premises used: MvPowerSeries.eval₂Hom_eq_extend
-- 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 : 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
rw : UniformContinuous (α := MvPowerSeries σ R) (β := S) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
⊢ UniformContinuous (eval₂ φ a)

Tactic:
rw [← coe_eval₂Hom hφ ha]

Premises used: MvPowerSeries.coe_eval₂Hom
-- 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 : 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
⊢ UniformContinuous (α := MvPowerSeries σ R) (β := S) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)

Tactic:
uniformContinuous_uniformly_extend
    toMvPowerSeries_isUniformInducing
    denseRange_toMvPowerSeries
    (toMvPowerSeries_uniformContinuous hφ ha)

Premises used: MvPolynomial.toMvPowerSeries_uniformContinuous, Classical.epsilon, MvPolynomial.toMvPowerSeries_isUniformInducing, Set.Mem, uniformContinuous_uniformly_extend, MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeries, Filter.lim, Filter.limUnder, IsDenseInducing.extend
-- 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 : 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
⊢ UniformContinuous (α := MvPowerSeries σ R) (β := S) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)

Tactic:
exact uniformContinuous_uniformly_extend
    toMvPowerSeries_isUniformInducing
    denseRange_toMvPowerSeries
    (toMvPowerSeries_uniformContinuous hφ ha)

Premises used: MvPolynomial.toMvPowerSeries_uniformContinuous, MvPolynomial.toMvPowerSeries_isUniformInducing, uniformContinuous_uniformly_extend, MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeries
-- 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 : 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
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ φ a)

Tactic:
(uniformContinuous_eval₂ hφ ha).continuous

Premises used: UniformContinuous.continuous, MvPowerSeries.uniformContinuous_eval₂
-- 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 : 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
f : MvPowerSeries σ R
rw :
  HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f)
⊢ HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (eval₂ φ a f)

Tactic:
rw [← coe_eval₂Hom hφ ha, eval₂Hom_eq_extend hφ ha]

Premises used: MvPowerSeries.eval₂Hom_eq_extend, MvPowerSeries.coe_eval₂Hom
-- 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 : 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
f : MvPowerSeries σ R
⊢ HasSum.{u_3, u_1} (α := S) (β := σ →₀ ℕ)
    (Function.comp (β := MvPowerSeries σ R) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S) fun (d : σ →₀ ℕ) ↦
        (monomial d : (a : R) → MvPowerSeries σ R) ((coeff d : (a : MvPowerSeries σ R) → R) f) :
      (σ →₀ ℕ) → S)
    ((eval₂Hom hφ ha : (a : MvPowerSeries σ R) → S) f : S)

Tactic:
(hasSum_of_monomials_self f).map (eval₂Hom hφ ha) (?_)

Premises used: HasSum.map, MvPowerSeries.eval₂Hom, MvPowerSeries.WithPiTopology.hasSum_of_monomials_self
-- 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 : 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
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S) =
      Function.comp (β := MvPowerSeries σ R) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
        (fun (d : σ →₀ ℕ) ↦ (monomial d : (a : R) → MvPowerSeries σ R) ((coeff d : (a : MvPowerSeries σ R) → R) f)) d
convert! :
  Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
⊢ HasSum
    (fun (d : σ →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S))
    (IsDenseInducing.extend ⋯ (MvPolynomial.eval₂ φ a) f)

Tactic:
convert! (hasSum_of_monomials_self f).map (eval₂Hom hφ ha) (?_) with d

Premises used: HasSum.map, MvPowerSeries.eval₂Hom, MvPowerSeries.WithPiTopology.hasSum_of_monomials_self
-- 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 : 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
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
      (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S) =
    Function.comp (β := MvPowerSeries σ R) (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
      (fun (d : σ →₀ ℕ) ↦ (monomial d : (a : R) → MvPowerSeries σ R) ((coeff d : (a : MvPowerSeries σ R) → R) f)) d

Tactic:
simp only [Function.comp_apply, coe_eval₂Hom, ← MvPolynomial.coe_monomial,
      eval₂_coe, eval₂_monomial]

Premises used: MvPowerSeries.eval₂_coe, MvPolynomial.coe_monomial, MvPowerSeries.coe_eval₂Hom, Function.comp_apply, MvPolynomial.eval₂_monomial
-- 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 : 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
f : MvPowerSeries σ R
rw : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ φ a)
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)

Tactic:
rw [coe_eval₂Hom]

Premises used: MvPowerSeries.coe_eval₂Hom
-- 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 : 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
f : MvPowerSeries σ R
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ φ a)

Tactic:
continuous_eval₂ hφ ha

Premises used: MvPowerSeries.continuous_eval₂
-- 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 : 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
f : MvPowerSeries σ R
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ φ a)

Tactic:
exact continuous_eval₂ hφ ha

Premises used: MvPowerSeries.continuous_eval₂
-- 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 : 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
f : MvPowerSeries σ R
⊢ eval₂ φ a f =
    ∑' (d : σ →₀ ℕ),
      HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) : S)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e : S)

Tactic:
(hasSum_eval₂ hφ ha f).tsum_eq.symm

Premises used: HasSum.tsum_eq, Eq.symm, MvPowerSeries.hasSum_eval₂
-- 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 : 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
ε : MvPowerSeries σ R → S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] ε
h : ∀ (p : MvPolynomial σ R), ε (↑p : MvPowerSeries σ R) = MvPolynomial.eval₂ φ a p
rw : ε = (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)
⊢ ε = eval₂ φ a

Tactic:
rw [← coe_eval₂Hom hφ ha]

Premises used: MvPowerSeries.coe_eval₂Hom
-- 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 : 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
ε : MvPowerSeries σ R → S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] ε
h : ∀ (p : MvPolynomial σ R), ε (↑p : MvPowerSeries σ R) = MvPolynomial.eval₂ φ a p
⊢ ε = (⇑(eval₂Hom hφ ha) : (a : MvPowerSeries σ R) → S)

Tactic:
(toMvPowerSeries_isDenseInducing.extend_unique h hε).symm

Premises used: Multiset.sum, Multiset.foldr, Classical.epsilon, Set.Mem, IsDenseInducing.extend_unique, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.toMvPowerSeries_isDenseInducing, MvPolynomial.toMvPowerSeries, MvPolynomial.coeff, Filter.lim, Eq.symm, Filter.limUnder, IsDenseInducing.extend, Finset.sum