R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
⊢ eval₂ f x (sum p g) = sum p fun n a => eval₂ f x (g n a)
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T
p : T[X]
g : ℕ → T → R[X]
x : S
⊢ eval₂ f x (sum p g) = sum p fun n a => eval₂ f x (g n a)
let T : R[X] →+ S :=
  { toFun := eval₂ f x
    map_zero' := eval₂_zero _ _
    map_add' := fun p q => eval₂_add _ _ }
R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
A : ∀ (y : R[X]), eval₂ f x y = ↑T y
⊢ eval₂ f x (sum p g) = sum p fun n a => eval₂ f x (g n a)
R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
⊢ eval₂ f x (sum p g) = sum p fun n a => eval₂ f x (g n a)
have A : ∀ y, eval₂ f x y = T y := fun y => rfl
R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
A : ∀ (y : R[X]), eval₂ f x y = ↑T y
⊢ ↑{ toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
          map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
      (sum p g) =
    sum p fun n a =>
      ↑{ toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
            map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
        (g n a)
R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
A : ∀ (y : R[X]), eval₂ f x y = ↑T y
⊢ eval₂ f x (sum p g) = sum p fun n a => eval₂ f x (g n a)
simp only [A]
no goals
R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
A : ∀ (y : R[X]), eval₂ f x y = ↑T y
⊢ ↑{ toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
          map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
      (sum p g) =
    sum p fun n a =>
      ↑{ toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
            map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
        (g n a)
rw [sum, T.map_sum, sum]