R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∀ (n_1 : ℕ), coeff (erase n p) n_1 ∈ RingHom.rangeS f
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : p ∈ lifts f
⊢ erase n p ∈ lifts f
rw [lifts_iff_ringHom_rangeS, mem_map_rangeS] at h⊢
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∀ (n_1 : ℕ), coeff (erase n p) n_1 ∈ RingHom.rangeS f
intro k
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : k = n
⊢ coeff (erase n p) k ∈ RingHom.rangeS f

case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
by_cases hk : k = n
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
i : R
hi : ↑f i = coeff p k
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
obtain ⟨i, hi⟩ := h k
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
i : R
hi : ↑f i = coeff p k
⊢ ↑f i = coeff (erase n p) k
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
i : R
hi : ↑f i = coeff p k
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
use i
no goals
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
i : R
hi : ↑f i = coeff p k
⊢ ↑f i = coeff (erase n p) k
simp only [hi, hk, erase_ne, Ne.def, not_false_iff]
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : k = n
⊢ ↑f 0 = coeff (erase n p) k
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : k = n
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
use 0
no goals
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : k = n
⊢ ↑f 0 = coeff (erase n p) k
simp only [hk, RingHom.map_zero, erase_same]