R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
i : R
hi : i ∈ ↑(frange (ofSubring T p))
⊢ i ∈ ↑T
R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
⊢ ↑(frange (ofSubring T p)) ⊆ ↑T
intro i hi
R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
i : R
hi : ∃ x, ¬coeff (ofSubring T p) x = 0 ∧ coeff (ofSubring T p) x = i
⊢ i ∈ ↑T
R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
i : R
hi : i ∈ ↑(frange (ofSubring T p))
⊢ i ∈ ↑T
simp only [frange, Set.mem_image, mem_support_iff, Ne.def, Finset.mem_coe, Finset.coe_image] at hi
case intro.intro
R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
i : R
n : ℕ
left✝ : ¬coeff (ofSubring T p) n = 0
h'n : coeff (ofSubring T p) n = i
⊢ i ∈ ↑T
R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
i : R
hi : ∃ x, ¬coeff (ofSubring T p) x = 0 ∧ coeff (ofSubring T p) x = i
⊢ i ∈ ↑T
rcases hi with ⟨n, _, h'n⟩
case intro.intro
R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
i : R
n : ℕ
left✝ : ¬coeff (ofSubring T p) n = 0
h'n : coeff (ofSubring T p) n = i
⊢ ↑(coeff p n) ∈ ↑T
case intro.intro
R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
i : R
n : ℕ
left✝ : ¬coeff (ofSubring T p) n = 0
h'n : coeff (ofSubring T p) n = i
⊢ i ∈ ↑T
rw [← h'n, coeff_ofSubring]
no goals
case intro.intro
R : Type u
S : Type ?u.109024
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
T : Subring R
p : { x // x ∈ T }[X]
i : R
n : ℕ
left✝ : ¬coeff (ofSubring T p) n = 0
h'n : coeff (ofSubring T p) n = i
⊢ ↑(coeff p n) ∈ ↑T
exact Subtype.mem (coeff p n : T)