case inl
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₁ : n < natDegree f
⊢ coeff f n ∈ 𝓟

case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₂ : n > natDegree f
⊢ coeff f n ∈ 𝓟
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
⊢ coeff f n ∈ 𝓟
cases' ne_iff_lt_or_gt.1 hn with h₁ h₂
no goals
case inl
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₁ : n < natDegree f
⊢ coeff f n ∈ 𝓟
exact hf.mem h₁
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₂ : n > natDegree f
⊢ 0 ∈ 𝓟
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₂ : n > natDegree f
⊢ coeff f n ∈ 𝓟
rw [coeff_eq_zero_of_natDegree_lt h₂]
no goals
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₂ : n > natDegree f
⊢ 0 ∈ 𝓟
exact Ideal.zero_mem _