no goals
R : Type u
S : Type ?u.98028
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
i : ℕ
⊢ ↑(coeff (toSubring 1 T (_ : ↑(frange 1) ⊆ ↑T)) i) = ↑(coeff 1 i)
rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
  OneMemClass.coe_one]