awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I : Ideal A
f g : A⟦X⟧
n : ℕ
inst_1 : I.IsTwoSided
hf : ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
⊢ ∀ i ≤ n, Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (f * g) : A)

Tactic:
simpa only [Ideal.IsTwoSided.mul_one] using
    coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal (J := 1) (g := g) n hf (by simp)

Premises used: Ideal.IsTwoSided.mul_one, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I : Ideal A
f g : A⟦X⟧
inst_1 : I.IsTwoSided
hf : ∀ (i : ℕ), Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
⊢ ∀ (i : ℕ), Membership.mem (α := A) (γ := Ideal A) 1 ((coeff i : (a : A⟦X⟧) → A) g : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem
Goal:
A : Type u_1
inst : Semiring A
I : Ideal A
f g : A⟦X⟧
inst_1 : I.IsTwoSided
hf : ∀ (i : ℕ), Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) f : A)
⊢ ∀ (i : ℕ), Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (f * g) : A)

Tactic:
simpa only [Ideal.IsTwoSided.mul_one] using
    coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (J := 1) (g := g) hf (by simp)

Premises used: Ideal.IsTwoSided.mul_one, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
a : S
⊢ HasEval a ↔ IsTopologicallyNilpotent a

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
a : S
ha : HasEval a
⊢ Filter.Tendsto.{0, u_2} (β := S) (fun (x : Unit) ↦ a) Filter.cofinite (nhds 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
a : S
ha : HasEval a
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a

Tactic:
hasEval_iff.mp ha

Premises used: Iff.mp, PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_3
inst : CommRing S
a : S
t u : TopologicalSpace S
h : t ≤ u
ha : HasEval a
simp :
  ∀ (ha : MvPowerSeries.HasEval.{0, u_3} (S := S) fun (x : Unit) ↦ a),
    MvPowerSeries.HasEval.{0, u_3} (S := S) fun (x : Unit) ↦ a
⊢ HasEval a

Tactic:
simp only [hasEval_iff] at ha ⊢

Premises used: PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_3
inst : CommRing S
a : S
t u : TopologicalSpace S
h : t ≤ u
ha : MvPowerSeries.HasEval.{0, u_3} (S := S) fun (x : Unit) ↦ a
⊢ MvPowerSeries.HasEval.{0, u_3} (S := S) fun (x : Unit) ↦ a

Tactic:
ha.mono h

Premises used: MvPowerSeries.HasEval.mono
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_3
inst : CommRing S
a : S
t u : TopologicalSpace S
h : t ≤ u
ha : MvPowerSeries.HasEval.{0, u_3} (S := S) fun (x : Unit) ↦ a
⊢ MvPowerSeries.HasEval.{0, u_3} (S := S) fun (x : Unit) ↦ a

Tactic:
exact ha.mono h

Premises used: MvPowerSeries.HasEval.mono
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
rw : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ 0
⊢ HasEval.{u_2} (S := S) 0

Tactic:
rw [hasEval_iff]

Premises used: PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ 0

Tactic:
MvPowerSeries.HasEval.zero

Premises used: MvPowerSeries.HasEval.zero
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ 0

Tactic:
exact MvPowerSeries.HasEval.zero

Premises used: MvPowerSeries.HasEval.zero
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : ContinuousAdd S
inst_3 : IsLinearTopology S S
a b : S
ha : HasEval a
hb : HasEval b
simp :
  ∀ (ha : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a)
    (hb : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ b),
    MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a + b
⊢ HasEval (a + b)

Tactic:
simp only [hasEval_iff] at ha hb ⊢

Premises used: PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : ContinuousAdd S
inst_3 : IsLinearTopology S S
a b : S
ha : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a
hb : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ b
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a + b

Tactic:
ha.add hb

Premises used: MvPowerSeries.HasEval.add
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : ContinuousAdd S
inst_3 : IsLinearTopology S S
a b : S
ha : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a
hb : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ b
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ a + b

Tactic:
exact ha.add hb

Premises used: MvPowerSeries.HasEval.add
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : S
hx : HasEval x
simp :
  ∀ (hx : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x),
    MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ c * x
⊢ HasEval (c * x)

Tactic:
simp only [hasEval_iff] at hx ⊢

Premises used: PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : S
hx : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ c * x

Tactic:
hx.mul_left _

Premises used: MvPowerSeries.HasEval.mul_left
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : S
hx : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ c * x

Tactic:
exact hx.mul_left _

Premises used: MvPowerSeries.HasEval.mul_left
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : S
hx : HasEval x
simp :
  ∀ (hx : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x),
    MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x * c
⊢ HasEval (x * c)

Tactic:
simp only [hasEval_iff] at hx ⊢

Premises used: PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : S
hx : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x * c

Tactic:
hx.mul_right _

Premises used: MvPowerSeries.HasEval.mul_right
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsLinearTopology S S
c x : S
hx : MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x_1 : Unit) ↦ x * c

Tactic:
exact hx.mul_right _

Premises used: MvPowerSeries.HasEval.mul_right
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
a : R
ha : HasEval a
simp :
  ∀ (ha : MvPowerSeries.HasEval.{0, u_1} (S := R) fun (x : Unit) ↦ a),
    MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ (φ : (a : R) → S) a
⊢ HasEval.{u_2} (S := S) ((φ : (a : R) → S) a : S)

Tactic:
simp only [hasEval_iff] at ha ⊢

Premises used: PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
a : R
ha : MvPowerSeries.HasEval.{0, u_1} (S := R) fun (x : Unit) ↦ a
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ (φ : (a : R) → S) a

Tactic:
ha.map hφ

Premises used: MvPowerSeries.HasEval.map
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
a : R
ha : MvPowerSeries.HasEval.{0, u_1} (S := R) fun (x : Unit) ↦ a
⊢ MvPowerSeries.HasEval.{0, u_2} (S := S) fun (x : Unit) ↦ (φ : (a : R) → S) a

Tactic:
exact ha.map hφ

Premises used: MvPowerSeries.HasEval.map
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
rw : MvPowerSeries.HasEval.{0, u_1} (S := R⟦X⟧) fun (x : Unit) ↦ X
⊢ HasEval.{u_1} (S := R⟦X⟧) X

Tactic:
rw [hasEval_iff]

Premises used: PowerSeries.hasEval_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
⊢ MvPowerSeries.HasEval.{0, u_1} (S := R⟦X⟧) fun (x : Unit) ↦ X

Tactic:
MvPowerSeries.HasEval.X

Premises used: PowerSeries.X, MvPowerSeries.HasEval.X
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
⊢ MvPowerSeries.HasEval.{0, u_1} (S := R⟦X⟧) fun (x : Unit) ↦ X

Tactic:
exact MvPowerSeries.HasEval.X

Premises used: MvPowerSeries.HasEval.X
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
S : Type u_2
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : IsTopologicalRing S
inst_3 : IsLinearTopology S S
a : S
⊢ Membership.mem (γ := Ideal S) hasEvalIdeal a ↔ HasEval a

Tactic:
simp [hasEvalIdeal]

Premises used: PowerSeries.hasEvalIdeal
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
f : Polynomial R
rw :
  eval₂ φ a
      (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
            ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
        R⟦X⟧) =
    Polynomial.eval₂ φ a
      ((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
        ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f))
⊢ eval₂ φ a (↑f : R⟦X⟧) = Polynomial.eval₂ φ a f

Tactic:
rw [← (MvPolynomial.uniqueAlgEquiv R Unit).apply_symm_apply f]

Premises used: MvPolynomial.uniqueAlgEquiv, AlgEquiv.apply_symm_apply, Unit
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
f : Polynomial R
simp :
  MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a)
      (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
            ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
        R⟦X⟧) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
⊢ eval₂ φ a
      (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
            ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
        R⟦X⟧) =
    Polynomial.eval₂ φ a
      ((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
        ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f))

Tactic:
simp only [PowerSeries.eval₂, MvPolynomial.eval₂_const_uniqueAlgEquiv]

Premises used: PowerSeries.eval₂, MvPolynomial.eval₂_const_uniqueAlgEquiv
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
f : Polynomial R
rw :
  MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a)
      (↑((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f) :
        MvPowerSeries PUnit.{1} R) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
rw₁ rw₂ :
  MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)
⊢ MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a)
      (↑((MvPolynomial.uniqueAlgEquiv R Unit : (a : MvPolynomial Unit R) → Polynomial R)
            ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)) :
        R⟦X⟧) =
    MvPolynomial.eval₂ φ (fun (x : Unit) ↦ a)
      ((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit) : (a : Polynomial R) → MvPolynomial Unit R) f)

Tactic:
rw [← MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPowerSeries.eval₂_coe]

Premises used: MvPowerSeries.eval₂_coe, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
r : R
rw : eval₂ φ a (↑((Polynomial.C : (a : R) → Polynomial R) r) : R⟦X⟧) = (φ : (a : R) → S) r
rw₁ : Polynomial.eval₂ φ a ((Polynomial.C : (a : R) → Polynomial R) r) = (φ : (a : R) → S) r
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) ((φ : (a : R) → S) r : S) ((φ : (a : R) → S) r : S)
⊢ eval₂ φ a ((C : (a : R) → R⟦X⟧) r) = (φ : (a : R) → S) r

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

Premises used: PowerSeries.eval₂_coe, Polynomial.coe_C, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
rw : eval₂ φ a (↑Polynomial.X : R⟦X⟧) = a
rw₁ : Polynomial.eval₂ φ a Polynomial.X = a
rw₂ rw₃ : a = a
⊢ eval₂ φ a X = a

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

Premises used: PowerSeries.eval₂_coe, Polynomial.coe_X, Polynomial.eval₂_X
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
⊢ (⇑(eval₂Hom hφ ha) : (a : R⟦X⟧) → S) = eval₂ φ a

Tactic:
MvPowerSeries.coe_eval₂Hom hφ (hasEval ha)

Premises used: PowerSeries.eval₂, MvPowerSeries.coe_eval₂Hom, PowerSeries.hasEval
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
⊢ UniformContinuous (eval₂ φ a)

Tactic:
MvPowerSeries.uniformContinuous_eval₂ hφ (hasEval ha)

Premises used: PowerSeries.eval₂, MvPowerSeries.uniformContinuous_eval₂, PowerSeries.hasEval
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
⊢ Continuous (eval₂ φ a)

Tactic:
(uniformContinuous_eval₂ hφ ha).continuous

Premises used: UniformContinuous.continuous, PowerSeries.uniformContinuous_eval₂
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
⊢ HasSum
    (fun (d : Unit →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S)
        ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)

Tactic:
have := MvPowerSeries.hasSum_eval₂ hφ (hasEval ha) f
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    (fun (d : Unit →₀ ℕ) ↦
      HMul.hMul (α := S) (β := S)
        ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
rw :
  ∀
    (this :
      HasSum
        ((fun (d : Unit →₀ ℕ) ↦
            HMul.hMul (α := S) (β := S)
              ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
              (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
          Finsupp.single ())
        (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)),
    HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
      (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
rw₁ :
  ∀ x ∉ Set.range (Finsupp.single ()),
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f : R) : S)
        (x.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S) =
      0
⊢ HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)

Tactic:
rw [← (Finsupp.single_injective ()).hasSum_iff] at this

Premises used: Finsupp.single_injective, Unit.unit, Function.Injective.hasSum_iff
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    ((fun (d : Unit →₀ ℕ) ↦
        HMul.hMul (α := S) (β := S)
          ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
          (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
      Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
⊢ HasSum
    ((fun (d : Unit →₀ ℕ) ↦
        HMul.hMul (α := S) (β := S)
          ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
          (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
      Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)

Tactic:
this
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    ((fun (d : Unit →₀ ℕ) ↦
        HMul.hMul (α := S) (β := S)
          ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
          (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
      Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
h :
  ∀ (x : ℕ),
    HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (a ^ x) =
      ((fun (d : Unit →₀ ℕ) ↦
            HMul.hMul (α := S) (β := S)
              ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
              (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
          Finsupp.single ())
        x
⊢ HasSum (fun (d : ℕ) ↦ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff d : (a : R⟦X⟧) → R) f : R) : S) (a ^ d))
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)

Tactic:
convert! this
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    ((fun (d : Unit →₀ ℕ) ↦
        HMul.hMul (α := S) (β := S)
          ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
          (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
      Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
x : ℕ
h :
  HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (a ^ x) =
    HMul.hMul (α := S)
      ((φ : (a : R) → S) ((MvPowerSeries.coeff (Finsupp.single () x) : (a : MvPowerSeries Unit R) → R) f : R) : S)
      (a ^ x)
⊢ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (a ^ x) =
    ((fun (d : Unit →₀ ℕ) ↦
          HMul.hMul (α := S) (β := S)
            ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
            (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
        Finsupp.single ())
      x

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Evaluation
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
φ : R →+* S
a : S
inst_2 : UniformSpace R
inst_3 : UniformSpace S
inst_4 : IsUniformAddGroup R
inst_5 : IsTopologicalSemiring R
inst_6 : IsUniformAddGroup S
inst_7 : T2Space S
inst_8 : CompleteSpace S
inst_9 : IsTopologicalRing S
inst_10 : IsLinearTopology S S
hφ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑φ : (a : R) → S)
ha : HasEval a
f : R⟦X⟧
this :
  HasSum
    ((fun (d : Unit →₀ ℕ) ↦
        HMul.hMul (α := S) (β := S)
          ((φ : (a : R) → S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) : S)
          (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e : S)) ∘
      Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun (x : Unit) ↦ a) f)
x : ℕ
⊢ HMul.hMul (α := S) ((φ : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (a ^ x) =
    HMul.hMul (α := S)
      ((φ : (a : R) → S) ((MvPowerSeries.coeff (Finsupp.single () x) : (a : MvPowerSeries Unit R) → R) f : R) : S)
      (a ^ x)

Tactic:
congr