R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(if coeff p n = 0 then 0 else { val := coeff p n, property := (_ : coeff p n ∈ Subring.closure ↑(frange p)) }) =
    coeff p n
R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(coeff (restriction p) n) = coeff p n
simp only [restriction, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
  Ne.def, ite_not]
case inl
R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
h : coeff p n = 0
⊢ ↑0 = coeff p n

case inr
R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
h : ¬coeff p n = 0
⊢ ↑{ val := coeff p n, property := (_ : coeff p n ∈ Subring.closure ↑(frange p)) } = coeff p n
R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(if coeff p n = 0 then 0 else { val := coeff p n, property := (_ : coeff p n ∈ Subring.closure ↑(frange p)) }) =
    coeff p n
split_ifs with h
case inl
R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
h : coeff p n = 0
⊢ ↑0 = 0
case inl
R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
h : coeff p n = 0
⊢ ↑0 = coeff p n
rw [h]
no goals
case inl
R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
h : coeff p n = 0
⊢ ↑0 = 0
rfl
no goals
case inr
R : Type u
S : Type ?u.66016
inst✝ : Ring R
p : R[X]
n : ℕ
h : ¬coeff p n = 0
⊢ ↑{ val := coeff p n, property := (_ : coeff p n ∈ Subring.closure ↑(frange p)) } = coeff p n
rfl