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 : 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:
exact (toMvPowerSeries_isDenseInducing.extend_unique h hε).symm

Premises used: IsDenseInducing.extend_unique, MvPolynomial.toMvPowerSeries_isDenseInducing, Eq.symm
-- 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
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
hε₁ : Continuous[instTopologicalSpace R, inst_11.toTopologicalSpace] ((⇑ε : (a : S) → T) ∘ eval₂ φ a)
h :
  ∀ (p : MvPolynomial σ R),
    ((⇑ε : (a : S) → T) ∘ eval₂ φ a) (↑p : MvPowerSeries σ R) =
      MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
apply : Continuous[inst_1.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑(ε.comp φ) : (a : R) → T)
⊢ (⇑ε : (a : S) → T) ∘ eval₂ φ a = eval₂ (ε.comp φ) ((⇑ε : (a : S) → T) ∘ a)

Tactic:
apply eval₂_unique _ (ha.map hε)

Premises used: MvPowerSeries.HasEval.map, MvPowerSeries.eval₂_unique
-- 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
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ Continuous[instTopologicalSpace R, inst_11.toTopologicalSpace] ((⇑ε : (a : S) → T) ∘ eval₂ φ a)

Tactic:
Continuous.comp hε (continuous_eval₂ hφ ha)

Premises used: MvPowerSeries.continuous_eval₂, Continuous.comp
-- 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
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ Continuous[instTopologicalSpace R, inst_11.toTopologicalSpace] ((⇑ε : (a : S) → T) ∘ eval₂ φ a)

Tactic:
exact Continuous.comp hε (continuous_eval₂ hφ ha)

Premises used: MvPowerSeries.continuous_eval₂, Continuous.comp
-- 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
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
p : MvPolynomial σ R
h :
  (ε : (a : S) → T) (MvPolynomial.eval₂ φ a p) = MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
⊢ ((⇑ε : (a : S) → T) ∘ eval₂ φ a) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p

Tactic:
simp only [Function.comp_apply, eval₂_coe]

Premises used: MvPowerSeries.eval₂_coe, Function.comp_apply
-- 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
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
p : MvPolynomial σ R
h :
  (ε : (a : S) → T) ((MvPolynomial.eval₂Hom φ a : (a : MvPolynomial σ R) → S) p : S) =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
h₁ :
  (ε.comp (MvPolynomial.eval₂Hom φ a) : (a : MvPolynomial σ R) → T) p =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
h₂ :
  (MvPolynomial.eval₂Hom (ε.comp φ) fun (i : σ) ↦ (ε : (a : S) → T) (a i) : (a : MvPolynomial σ R) → T) p =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
h₃ h₄ :
  MvPolynomial.eval₂ (ε.comp φ) (fun (i : σ) ↦ (ε : (a : S) → T) (a i)) p =
    MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p
⊢ (ε : (a : S) → T) (MvPolynomial.eval₂ φ a p) = MvPolynomial.eval₂ (ε.comp φ) (fun (s : σ) ↦ (ε : (a : S) → T) (a s)) p

Tactic:
rw [← MvPolynomial.coe_eval₂Hom, ← comp_apply, MvPolynomial.comp_eval₂Hom,
      MvPolynomial.coe_eval₂Hom]

Premises used: MvPolynomial.comp_eval₂Hom, MvPolynomial.coe_eval₂Hom, RingHom.comp_apply
-- 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
T : Type u_4
inst_11 : UniformSpace T
inst_12 : CompleteSpace T
inst_13 : T2Space T
inst_14 : CommRing T
inst_15 : IsTopologicalRing T
inst_16 : IsLinearTopology T T
inst_17 : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst_3.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑ε : (a : S) → T)
⊢ Continuous[inst_1.toTopologicalSpace, inst_11.toTopologicalSpace] (⇑(ε.comp φ) : (a : R) → T)

Tactic:
simp only [coe_comp, Continuous.comp hε hφ]

Premises used: Continuous.comp, RingHom.coe_comp
-- 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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
r : R
simp :
  Eq.{u_3 + 1} (α := S)
    ((eval₂Hom (φ := algebraMap R S) ⋯ ha : (a : MvPowerSeries σ R) → S)
        ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) :
      S)
    ((algebraMap R S : (a : R) → S) r : S)
⊢ OneHom.toFun (↑(↑(eval₂Hom (φ := algebraMap R S) ⋯ ha) : MvPowerSeries σ R →* S) : OneHom (MvPowerSeries σ R) S)
      ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r) =
    (algebraMap R S : (a : R) → S) r

Tactic:
simp only [toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe]

Premises used: RingHom.toMonoidHom_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe, OneHom.toFun_eq_coe
-- 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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
r : R
rw :
  Eq.{u_3 + 1} (α := S)
    ((eval₂Hom (φ := algebraMap R S) ⋯ ha : (a : MvPowerSeries σ R) → S)
        ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) :
      S)
    ((algebraMap R S : (a : R) → S) r : S)
rw₁ : eval₂ (algebraMap R S) a ((C : (a : R) → MvPowerSeries σ R) r) = (algebraMap R S : (a : R) → S) r
rw₂ rw₃ : Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
⊢ Eq.{u_3 + 1} (α := S)
    ((eval₂Hom (φ := algebraMap R S) ⋯ ha : (a : MvPowerSeries σ R) → S)
        ((algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) :
      S)
    ((algebraMap R S : (a : R) → S) r : S)

Tactic:
rw [← c_eq_algebraMap, coe_eval₂Hom, eval₂_C]

Premises used: MvPowerSeries.coe_eval₂Hom, MvPowerSeries.c_eq_algebraMap, MvPowerSeries.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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
⊢ (⇑(aeval ha) : (a : MvPowerSeries σ R) → S) = eval₂ (algebraMap R S) a

Tactic:
simp only [aeval, AlgHom.coe_mk, coe_eval₂Hom]

Premises used: AlgHom.coe_mk, MvPowerSeries.aeval, 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
rw : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ (algebraMap R S) a)
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑(aeval ha) : (a : MvPowerSeries σ R) → S)

Tactic:
rw [coe_aeval]

Premises used: MvPowerSeries.coe_aeval
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ (algebraMap R S) a)

Tactic:
continuous_eval₂ (continuous_algebraMap R S) ha

Premises used: MvPowerSeries.continuous_eval₂, continuous_algebraMap
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
⊢ Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (eval₂ (algebraMap R S) a)

Tactic:
exact continuous_eval₂ (continuous_algebraMap R S) ha

Premises used: MvPowerSeries.continuous_eval₂, continuous_algebraMap
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ha : HasEval a
p : MvPolynomial σ R
rw : eval₂ (algebraMap R S) a (↑p : MvPowerSeries σ R) = (MvPolynomial.aeval a : (a : MvPolynomial σ R) → S) p
rw₁ : eval₂ (algebraMap R S) a (↑p : MvPowerSeries σ R) = MvPolynomial.eval₂ (algebraMap R S) a p
rw₂ rw₃ : MvPolynomial.eval₂ (algebraMap R S) a p = MvPolynomial.eval₂ (algebraMap R S) a p
⊢ Eq.{u_3 + 1} (α := S) ((aeval ha : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) : S)
    ((MvPolynomial.aeval a : (a : MvPolynomial σ R) → S) p : S)

Tactic:
rw [coe_aeval, aeval_def, eval₂_coe]

Premises used: MvPowerSeries.eval₂_coe, MvPolynomial.aeval_def, MvPowerSeries.coe_aeval
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
h :
  Eq (α := (a : MvPowerSeries σ R) → S)
    (⇑(aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) ⋯) : (a : MvPowerSeries σ R) → S)
    (⇑ε : (a : MvPowerSeries σ R) → S)
⊢ aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) ⋯ = ε

Tactic:
apply DFunLike.ext'

Premises used: DFunLike.ext'
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
h :
  Eq (α := (a : MvPowerSeries σ R) → S)
    (eval₂ (algebraMap R S) fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s))
    (⇑ε : (a : MvPowerSeries σ R) → S)
⊢ Eq (α := (a : MvPowerSeries σ R) → S)
    (⇑(aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) ⋯) : (a : MvPowerSeries σ R) → S)
    (⇑ε : (a : MvPowerSeries σ R) → S)

Tactic:
rw [coe_aeval]

Premises used: MvPowerSeries.coe_aeval
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
⊢ Eq (α := (a : MvPowerSeries σ R) → S)
    (eval₂ (algebraMap R S) fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s))
    (⇑ε : (a : MvPowerSeries σ R) → S)

Tactic:
(eval₂_unique (continuous_algebraMap R S) (HasEval.X.map hε) hε ?_).symm

Premises used: continuous_algebraMap, MvPowerSeries.HasEval.map, MvPowerSeries.HasEval.X, MvPowerSeries.eval₂_unique, Eq.symm
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
h :
  ∀ (p : MvPolynomial σ R),
    (ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) =
      MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
⊢ Eq (α := (a : MvPowerSeries σ R) → S)
    (eval₂ (algebraMap R S) fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s))
    (⇑ε : (a : MvPowerSeries σ R) → S)

Tactic:
refine (eval₂_unique (continuous_algebraMap R S) (HasEval.X.map hε) hε ?_).symm

Premises used: continuous_algebraMap, MvPowerSeries.HasEval.map, MvPowerSeries.HasEval.X, MvPowerSeries.eval₂_unique, Eq.symm
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
trans :
  Eq.{u_3 + 1} (α := S) ((ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) : S)
    ((ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p : S)
trans₁ :
  (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
⊢ (ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p

Tactic:
trans ε.comp (coeToMvPowerSeries.algHom R) p

Premises used: MvPolynomial.coeToMvPowerSeries.algHom, AlgHom.comp, DFunLike.coe
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
⊢ Eq.{u_3 + 1} (α := S) ((ε : (a : MvPowerSeries σ R) → S) (↑p : MvPowerSeries σ R) : S)
    ((ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p : S)

Tactic:
simp
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
rw :
  MvPolynomial.eval₂ (algebraMap R S)
    (fun (i : σ) ↦ (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) (MvPolynomial.X i)) p
| (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p

Tactic:
rw [← p.aeval_X_left_apply, MvPolynomial.comp_aeval_apply, MvPolynomial.aeval_def]

Premises used: MvPolynomial.aeval_X_left_apply, MvPolynomial.aeval_def, MvPolynomial.comp_aeval_apply
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
conv_lhs :
  MvPolynomial.eval₂ (algebraMap R S)
      (fun (i : σ) ↦ (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) (MvPolynomial.X i)) p =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p
⊢ (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) p =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p

Tactic:
conv_lhs => rw [← p.aeval_X_left_apply, MvPolynomial.comp_aeval_apply, MvPolynomial.aeval_def]

Premises used: MvPolynomial.aeval_X_left_apply, MvPolynomial.aeval_def, MvPolynomial.comp_aeval_apply
-- 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
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
inst_11 : Algebra R S
inst_12 : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst_3.toTopologicalSpace] (⇑ε : (a : MvPowerSeries σ R) → S)
p : MvPolynomial σ R
⊢ MvPolynomial.eval₂ (algebraMap R S)
      (fun (i : σ) ↦ (ε.comp (coeToMvPowerSeries.algHom R) : (a : MvPolynomial σ R) → S) (MvPolynomial.X i)) p =
    MvPolynomial.eval₂ (algebraMap R S) (fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries σ R) → S) (X s)) p

Tactic:
simp