case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : p = 0
⊢ rootMultiplicity x p ≤ 1

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : ¬p = 0
⊢ rootMultiplicity x p ≤ 1
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
⊢ rootMultiplicity x p ≤ 1
by_cases hp : p = 0
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : ¬p = 0
⊢ multiplicity (X - ↑C x) p ≤ 1
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : ¬p = 0
⊢ rootMultiplicity x p ≤ 1
rw [rootMultiplicity_eq_multiplicity, dif_neg hp, ← PartENat.coe_le_coe, PartENat.natCast_get,
  Nat.cast_one]
no goals
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : ¬p = 0
⊢ multiplicity (X - ↑C x) p ≤ 1
exact multiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep
no goals
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : p = 0
⊢ rootMultiplicity x p ≤ 1
simp [hp]