case a
R : Type u
S : Type ?u.69179
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ i ∈ support (restriction p) ↔ i ∈ support p
R : Type u
S : Type ?u.69179
inst✝ : Ring R
p : R[X]
⊢ support (restriction p) = support p
ext i
case a
R : Type u
S : Type ?u.69179
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ coeff (restriction p) i = 0 ↔ coeff p i = 0
case a
R : Type u
S : Type ?u.69179
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ i ∈ support (restriction p) ↔ i ∈ support p
simp only [mem_support_iff, not_iff_not, Ne.def]
case a
R : Type u
S : Type ?u.69179
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ coeff (restriction p) i = 0 ↔ ↑(coeff (restriction p) i) = 0
case a
R : Type u
S : Type ?u.69179
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ coeff (restriction p) i = 0 ↔ coeff p i = 0
conv_rhs => rw [← coeff_restriction]
no goals
case a
R : Type u
S : Type ?u.69179
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ coeff (restriction p) i = 0 ↔ ↑(coeff (restriction p) i) = 0
exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩
no goals
R : Type u
S : Type ?u.69179
inst✝ : Ring R
p : R[X]
i : ℕ
H : coeff (restriction p) i = 0
⊢ ↑(coeff (restriction p) i) = 0
rw [H, ZeroMemClass.coe_zero]