R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
⊢ ↑(if coeff p n = 0 then 0 else { val := coeff p n, property := (_ : coeff p n ∈ T) }) = coeff p n
R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
⊢ ↑(coeff (toSubring p T hp) n) = coeff p n
simp only [toSubring, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
  Ne.def, ite_not]
case inl
R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
h : coeff p n = 0
⊢ ↑0 = coeff p n

case inr
R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
h : ¬coeff p n = 0
⊢ ↑{ val := coeff p n, property := (_ : coeff p n ∈ T) } = coeff p n
R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
⊢ ↑(if coeff p n = 0 then 0 else { val := coeff p n, property := (_ : coeff p n ∈ T) }) = coeff p n
split_ifs with h
case inl
R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
h : coeff p n = 0
⊢ ↑0 = 0
case inl
R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
h : coeff p n = 0
⊢ ↑0 = coeff p n
rw [h]
no goals
case inl
R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
h : coeff p n = 0
⊢ ↑0 = 0
rfl
no goals
case inr
R : Type u
S : Type ?u.84546
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑(frange p) ⊆ ↑T
n : ℕ
h : ¬coeff p n = 0
⊢ ↑{ val := coeff p n, property := (_ : coeff p n ∈ T) } = coeff p n
rfl