case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : p = 0
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)

case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
by_cases hp : p = 0
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ coeff (map f (↑(expand R p) q)) n✝ = coeff (↑(expand S p) (map f q)) n✝
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
ext
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ ↑f (if p ∣ n✝ then coeff q (n✝ / p) else 0) = if p ∣ n✝ then coeff (map f q) (n✝ / p) else 0
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ coeff (map f (↑(expand R p) q)) n✝ = coeff (↑(expand S p) (map f q)) n✝
rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]
no goals
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ ↑f (if p ∣ n✝ then coeff q (n✝ / p) else 0) = if p ∣ n✝ then coeff (map f q) (n✝ / p) else 0
split_ifs <;> simp_all
no goals
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : p = 0
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
simp [hp]