case refine'_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (p q : R[X]),
    ↑(↑(aeval f) p) x = eval (↑f x) p →
      ↑(↑(aeval f) q) x = eval (↑f x) q → ↑(↑(aeval f) (p + q)) x = eval (↑f x) (p + q)

case refine'_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (n : ℕ) (a : R), ↑(↑(aeval f) (↑(monomial n) a)) x = eval (↑f x) (↑(monomial n) a)
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ↑(↑(aeval f) g) x = eval (↑f x) g
refine' Polynomial.induction_on' g _ _
case refine'_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
p q : R[X]
hp : ↑(↑(aeval f) p) x = eval (↑f x) p
hq : ↑(↑(aeval f) q) x = eval (↑f x) q
⊢ ↑(↑(aeval f) (p + q)) x = eval (↑f x) (p + q)
case refine'_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (p q : R[X]),
    ↑(↑(aeval f) p) x = eval (↑f x) p →
      ↑(↑(aeval f) q) x = eval (↑f x) q → ↑(↑(aeval f) (p + q)) x = eval (↑f x) (p + q)
intro p q hp hq
no goals
case refine'_1
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
p q : R[X]
hp : ↑(↑(aeval f) p) x = eval (↑f x) p
hq : ↑(↑(aeval f) q) x = eval (↑f x) q
⊢ ↑(↑(aeval f) (p + q)) x = eval (↑f x) (p + q)
simp [hp, hq]
case refine'_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
n : ℕ
a : R
⊢ ↑(↑(aeval f) (↑(monomial n) a)) x = eval (↑f x) (↑(monomial n) a)
case refine'_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ ∀ (n : ℕ) (a : R), ↑(↑(aeval f) (↑(monomial n) a)) x = eval (↑f x) (↑(monomial n) a)
intro n a
no goals
case refine'_2
R : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
n : ℕ
a : R
⊢ ↑(↑(aeval f) (↑(monomial n) a)) x = eval (↑f x) (↑(monomial n) a)
simp [Pi.pow_apply]