internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.comp_eval₂
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ Continuous (⇑ε ∘ ⇑(eval₂Hom hφ ha))

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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
exact Continuous.comp hε (continuous_eval₂ hφ ha)
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Theorem: MvPowerSeries.comp_eval₂
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
intro p
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Theorem: MvPowerSeries.comp_eval₂
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, eval₂_coe]
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε ((eval₂Hom hφ ha) ↑p) = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Theorem: MvPowerSeries.comp_eval₂
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε ((eval₂Hom hφ ha) ↑p) = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
rw [coe_eval₂Hom hφ ha, eval₂_coe hφ ha, ← MvPolynomial.coe_eval₂Hom]
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε ((MvPolynomial.eval₂Hom φ a) p) = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Theorem: MvPowerSeries.comp_eval₂
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε ((MvPolynomial.eval₂Hom φ a) p) = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
rw [← RingHom.comp_apply, MvPolynomial.comp_eval₂Hom]
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ (MvPolynomial.eval₂Hom (ε.comp φ) fun i => ε (a i)) p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Theorem: MvPowerSeries.comp_eval₂
Proof 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ (MvPolynomial.eval₂Hom (ε.comp φ) fun i => ε (a i)) p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.aeval_coe
Proof 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
p : MvPolynomial σ R
⊢ (aeval ha) ↑p = (MvPolynomial.aeval a) p
Tactic:
simp only [coe_aeval, eval₂_coe (continuous_algebraMap R S) ha, aeval_def]
Proof state after:
no goals
Theorem: MvPowerSeries.aeval_unique
Proof 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'
Proof 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 ⋯)
Theorem: MvPowerSeries.aeval_unique
Proof 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]
Proof 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)
Theorem: MvPowerSeries.aeval_unique
Proof 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ε
Proof 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
Theorem: MvPowerSeries.aeval_unique
Proof 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
Proof 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
Theorem: MvPowerSeries.aeval_unique
Proof 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]
Proof state after:
no goals
Theorem: MvPowerSeries.aeval_unique
Proof 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]
Proof 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
Theorem: MvPowerSeries.aeval_unique
Proof 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]
Proof state after:
no goals
Theorem: MvPowerSeries.aeval_unique
Proof 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
Proof 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)
Theorem: MvPowerSeries.aeval_unique
Proof 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]
Proof state after:
no goals
Theorem: MvPowerSeries.aeval_unique
Proof 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
Proof 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)
Theorem: MvPowerSeries.aeval_unique
Proof 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]
Proof state after:
no goals