R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), f ∈ ⨅ (_ : i ≥ n), LinearMap.ker (lcoeff R i)) ↔ degree f < ↑n
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ f ∈ degreeLT R n ↔ degree f < ↑n
rw [degreeLT, Submodule.mem_iInf]
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ degree f < ↑n
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), f ∈ ⨅ (_ : i ≥ n), LinearMap.ker (lcoeff R i)) ↔ degree f < ↑n
conv_lhs => intro i; rw [Submodule.mem_iInf]
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ sup (support f) WithBot.some < ↑n
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ degree f < ↑n
rw [degree, Finset.max_eq_sup_coe]
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), b ∈ support f → ↑b < ↑n

R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ⊥ < ↑n
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ sup (support f) WithBot.some < ↑n
rw [Finset.sup_lt_iff ?_]
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ⊥ < ↑n

R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), b ∈ support f → ↑b < ↑n
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), b ∈ support f → ↑b < ↑n

R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ⊥ < ↑n
rotate_left
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), b ∈ support f → ↑b < ↑n
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ ⊥ < ↑n

R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), b ∈ support f → ↑b < ↑n
apply WithBot.bot_lt_coe
no goals
R : Type u
S : Type ?u.11734
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ (∀ (i : ℕ), i ≥ n → f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), b ∈ support f → ↑b < ↑n
conv_rhs =>
  simp only [mem_support_iff]
  intro b
  rw [Nat.cast_withBot, WithBot.coe_lt_coe, lt_iff_not_le, Ne, not_imp_not]