case H0
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
ps : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
hf : ∀ (p : R[X]), p ∈ [] → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
⊢ eval₂ f x (List.prod []) = List.prod (List.map (eval₂ f x) [])

case H1
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
ps✝ : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps✝ → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
ps : List R[X]
p : R[X]
ihp :
  (∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x) →
    eval₂ f x (List.prod ps) = List.prod (List.map (eval₂ f x) ps)
hf : ∀ (p_1 : R[X]), p_1 ∈ ps ++ [p] → ∀ (k : ℕ), Commute (↑f (coeff p_1 k)) x
⊢ eval₂ f x (List.prod (ps ++ [p])) = List.prod (List.map (eval₂ f x) (ps ++ [p]))
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
ps : List R[X]
hf : ∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
⊢ eval₂ f x (List.prod ps) = List.prod (List.map (eval₂ f x) ps)
induction' ps using List.reverseRecOn with ps p ihp
no goals
case H0
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
ps : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
hf : ∀ (p : R[X]), p ∈ [] → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
⊢ eval₂ f x (List.prod []) = List.prod (List.map (eval₂ f x) [])
simp
case H1
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
ps✝ : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps✝ → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
ps : List R[X]
p : R[X]
ihp :
  (∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x) →
    eval₂ f x (List.prod ps) = List.prod (List.map (eval₂ f x) ps)
hf : (∀ (x_1 : R[X]), x_1 ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff x_1 k)) x) ∧ ∀ (k : ℕ), Commute (↑f (coeff p k)) x
⊢ eval₂ f x (List.prod (ps ++ [p])) = List.prod (List.map (eval₂ f x) (ps ++ [p]))
case H1
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
ps✝ : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps✝ → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
ps : List R[X]
p : R[X]
ihp :
  (∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x) →
    eval₂ f x (List.prod ps) = List.prod (List.map (eval₂ f x) ps)
hf : ∀ (p_1 : R[X]), p_1 ∈ ps ++ [p] → ∀ (k : ℕ), Commute (↑f (coeff p_1 k)) x
⊢ eval₂ f x (List.prod (ps ++ [p])) = List.prod (List.map (eval₂ f x) (ps ++ [p]))
simp only [List.forall_mem_append, List.forall_mem_singleton] at hf
no goals
case H1
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
ps✝ : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps✝ → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
ps : List R[X]
p : R[X]
ihp :
  (∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x) →
    eval₂ f x (List.prod ps) = List.prod (List.map (eval₂ f x) ps)
hf : (∀ (x_1 : R[X]), x_1 ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff x_1 k)) x) ∧ ∀ (k : ℕ), Commute (↑f (coeff p k)) x
⊢ eval₂ f x (List.prod (ps ++ [p])) = List.prod (List.map (eval₂ f x) (ps ++ [p]))
simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]