Theorem: MvPowerSeries.aeval_unique (DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean)

State before:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
⊢ ε = aeval ⋯
Tactic:
apply DFunLike.ext'
State after:
case h
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
⊢ ⇑ε = ⇑(aeval ⋯)

State before:
case h
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
⊢ ⇑ε = ⇑(aeval ⋯)
Tactic:
rw [coe_aeval]
State after:
case h
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
⊢ ⇑ε = eval₂ (algebraMap R S) fun s => ε.toRingHom (X s)

State before:
case h
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
⊢ ⇑ε = eval₂ (algebraMap R S) fun s => ε.toRingHom (X s)
Tactic:
apply eval₂_unique hε
State after:
case h
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), ε.toRingHom ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) p

State before:
case h
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), ε.toRingHom ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) p
Tactic:
intro p
State after:
case h
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε.toRingHom ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) p

State before:
case h
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε.toRingHom ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) p
Tactic:
induction p using MvPolynomial.induction_on with
| h_C r =>
  simp only [AlgHom.toRingHom_eq_coe, coe_C, RingHom.coe_coe, MvPolynomial.eval₂_C]
  rw [c_eq_algebraMap, AlgHom.commutes]
| h_add p q hp hq =>
  simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe] at hp hq
  simp only [AlgHom.toRingHom_eq_coe, coe_add, map_add,
    RingHom.coe_coe, eval₂_add, hp, hq]
| h_X p s h =>
  simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe] at h
  simp only [AlgHom.toRingHom_eq_coe, coe_mul, coe_X, map_mul,
    RingHom.coe_coe, eval₂_mul, MvPolynomial.eval₂_X, h]
State after:
no goals

State before:
case h.h_C
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
r : R
⊢ ε.toRingHom ↑(MvPolynomial.C r) = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) (MvPolynomial.C r)
Tactic:
simp only [AlgHom.toRingHom_eq_coe, coe_C, RingHom.coe_coe, MvPolynomial.eval₂_C]
State after:
case h.h_C
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
r : R
⊢ ε ((C σ R) r) = (algebraMap R S) r

State before:
case h.h_C
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
r : R
⊢ ε ((C σ R) r) = (algebraMap R S) r
Tactic:
rw [c_eq_algebraMap, AlgHom.commutes]
State after:
no goals

State before:
case h.h_add
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
p q : MvPolynomial σ R
hp : ε.toRingHom ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) p
hq : ε.toRingHom ↑q = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) q
⊢ ε.toRingHom ↑(p + q) = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) (p + q)
Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe] at hp hq
State after:
case h.h_add
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
p q : MvPolynomial σ R
hp : ε ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε (X s)) p
hq : ε ↑q = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε (X s)) q
⊢ ε.toRingHom ↑(p + q) = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) (p + q)

State before:
case h.h_add
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
p q : MvPolynomial σ R
hp : ε ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε (X s)) p
hq : ε ↑q = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε (X s)) q
⊢ ε.toRingHom ↑(p + q) = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) (p + q)
Tactic:
simp only [AlgHom.toRingHom_eq_coe, coe_add, map_add,
  RingHom.coe_coe, eval₂_add, hp, hq]
State after:
no goals

State before:
case h.h_X
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
p : MvPolynomial σ R
s : σ
h : ε.toRingHom ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) p
⊢ ε.toRingHom ↑(p * MvPolynomial.X s) =
    MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) (p * MvPolynomial.X s)
Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe] at h
State after:
case h.h_X
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
p : MvPolynomial σ R
s : σ
h : ε ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε (X s)) p
⊢ ε.toRingHom ↑(p * MvPolynomial.X s) =
    MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) (p * MvPolynomial.X s)

State before:
case h.h_X
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous ⇑ε
p : MvPolynomial σ R
s : σ
h : ε ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s => ε (X s)) p
⊢ ε.toRingHom ↑(p * MvPolynomial.X s) =
    MvPolynomial.eval₂ (algebraMap R S) (fun s => ε.toRingHom (X s)) (p * MvPolynomial.X s)
Tactic:
simp only [AlgHom.toRingHom_eq_coe, coe_mul, coe_X, map_mul,
  RingHom.coe_coe, eval₂_mul, MvPolynomial.eval₂_X, h]
State after:
no goals