diff --git a/Archive/Wiedijk100Theorems/AbelRuffini.lean b/Archive/Wiedijk100Theorems/AbelRuffini.lean
index b3e7ef47ddb03..58a9f96527dae 100644
--- a/Archive/Wiedijk100Theorems/AbelRuffini.lean
+++ b/Archive/Wiedijk100Theorems/AbelRuffini.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
-import Mathlib.Analysis.Calculus.LocalExtr
+import Mathlib.Analysis.Calculus.LocalExtr.Polynomial
 import Mathlib.FieldTheory.AbelRuffini
 import Mathlib.RingTheory.RootsOfUnity.Minpoly
 import Mathlib.RingTheory.EisensteinCriterion
diff --git a/Mathlib.lean b/Mathlib.lean
index 6f07e61fcd277..011a1f36f7af7 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -567,7 +567,9 @@ import Mathlib.Analysis.Calculus.Inverse
 import Mathlib.Analysis.Calculus.IteratedDeriv
 import Mathlib.Analysis.Calculus.LHopital
 import Mathlib.Analysis.Calculus.LagrangeMultipliers
-import Mathlib.Analysis.Calculus.LocalExtr
+import Mathlib.Analysis.Calculus.LocalExtr.Basic
+import Mathlib.Analysis.Calculus.LocalExtr.Polynomial
+import Mathlib.Analysis.Calculus.LocalExtr.Rolle
 import Mathlib.Analysis.Calculus.MeanValue
 import Mathlib.Analysis.Calculus.Monotone
 import Mathlib.Analysis.Calculus.ParametricIntegral
@@ -3134,6 +3136,7 @@ import Mathlib.Topology.Algebra.Order.LiminfLimsup
 import Mathlib.Topology.Algebra.Order.MonotoneContinuity
 import Mathlib.Topology.Algebra.Order.MonotoneConvergence
 import Mathlib.Topology.Algebra.Order.ProjIcc
+import Mathlib.Topology.Algebra.Order.Rolle
 import Mathlib.Topology.Algebra.Order.T5
 import Mathlib.Topology.Algebra.Order.UpperLower
 import Mathlib.Topology.Algebra.Polynomial
diff --git a/Mathlib/Analysis/Calculus/Darboux.lean b/Mathlib/Analysis/Calculus/Darboux.lean
index 2e07555a9a137..4577748ce7317 100644
--- a/Mathlib/Analysis/Calculus/Darboux.lean
+++ b/Mathlib/Analysis/Calculus/Darboux.lean
@@ -3,7 +3,9 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Analysis.Calculus.LocalExtr
+import Mathlib.Analysis.Calculus.Deriv.Add
+import Mathlib.Analysis.Calculus.Deriv.Mul
+import Mathlib.Analysis.Calculus.LocalExtr.Basic
 
 #align_import analysis.calculus.darboux from "leanprover-community/mathlib"@"61b5e2755ccb464b68d05a9acf891ae04992d09d"
 
diff --git a/Mathlib/Analysis/Calculus/FDerivSymmetric.lean b/Mathlib/Analysis/Calculus/FDerivSymmetric.lean
index 372d828ec60e3..76d3646498aad 100644
--- a/Mathlib/Analysis/Calculus/FDerivSymmetric.lean
+++ b/Mathlib/Analysis/Calculus/FDerivSymmetric.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
+import Mathlib.Analysis.Calculus.Deriv.Pow
 import Mathlib.Analysis.Calculus.MeanValue
 
 #align_import analysis.calculus.fderiv_symmetric from "leanprover-community/mathlib"@"2c1d8ca2812b64f88992a5294ea3dba144755cd1"
diff --git a/Mathlib/Analysis/Calculus/LocalExtr.lean b/Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
similarity index 58%
rename from Mathlib/Analysis/Calculus/LocalExtr.lean
rename to Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
index a5afc09941289..26a94d167e677 100644
--- a/Mathlib/Analysis/Calculus/LocalExtr.lean
+++ b/Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
@@ -3,14 +3,12 @@ Copyright (c) 2019 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Analysis.Calculus.Deriv.Polynomial
-import Mathlib.Topology.Algebra.Order.ExtendFrom
-import Mathlib.Topology.Algebra.Polynomial
+import Mathlib.Analysis.Calculus.Deriv.Add
 
 #align_import analysis.calculus.local_extr from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
 
 /-!
-# Local extrema of smooth functions
+# Local extrema of differentiable functions
 
 ## Main definitions
 
@@ -24,7 +22,7 @@ This set is used in the proof of Fermat's Theorem (see below), and can be used t
 
 For each theorem name listed below,
 we also prove similar theorems for `min`, `extr` (if applicable),
-and `(f)deriv` instead of `has_fderiv`.
+and `fderiv`/`deriv` instead of `HasFDerivAt`/`HasDerivAt`.
 
 * `IsLocalMaxOn.hasFDerivWithinAt_nonpos` : `f' y ≤ 0` whenever `a` is a local maximum
   of `f` on `s`, `f` has derivative `f'` at `a` within `s`, and `y` belongs to the positive tangent
@@ -37,10 +35,6 @@ and `(f)deriv` instead of `has_fderiv`.
   [Fermat's Theorem](https://en.wikipedia.org/wiki/Fermat's_theorem_(stationary_points)),
   the derivative of a differentiable function at a local extremum point equals zero.
 
-* `exists_hasDerivAt_eq_zero` :
-  [Rolle's Theorem](https://en.wikipedia.org/wiki/Rolle's_theorem): given a function `f` continuous
-  on `[a, b]` and differentiable on `(a, b)`, there exists `c ∈ (a, b)` such that `f' c = 0`.
-
 ## Implementation notes
 
 For each mathematical fact we prove several versions of its formalization:
@@ -54,12 +48,11 @@ due to the fact that `fderiv` and `deriv` are defined to be zero for non-differe
 ## References
 
 * [Fermat's Theorem](https://en.wikipedia.org/wiki/Fermat's_theorem_(stationary_points));
-* [Rolle's Theorem](https://en.wikipedia.org/wiki/Rolle's_theorem);
 * [Tangent cone](https://en.wikipedia.org/wiki/Tangent_cone);
 
 ## Tags
 
-local extremum, Fermat's Theorem, Rolle's Theorem
+local extremum, tangent cone, Fermat's Theorem
 -/
 
 
@@ -67,12 +60,16 @@ universe u v
 
 open Filter Set
 
-open scoped Topology Classical Polynomial
+open scoped Topology Classical
 
 section Module
 
 variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ}
 
+/-!
+### Positive tangent cone
+-/
+
 /-- "Positive" tangent cone to `s` at `x`; the only difference from `tangentConeAt`
 is that we require `c n → ∞` instead of `‖c n‖ → ∞`. One can think about `posTangentConeAt`
 as `tangentConeAt NNReal` but we have no theory of normed semifields yet. -/
@@ -108,6 +105,10 @@ theorem posTangentConeAt_univ : posTangentConeAt univ a = univ :=
   eq_univ_of_forall fun _ => mem_posTangentConeAt_of_segment_subset' (subset_univ _)
 #align pos_tangent_cone_at_univ posTangentConeAt_univ
 
+/-!
+### Fermat's Theorem (vector space)
+-/
+
 /-- If `f` has a local max on `s` at `a`, `f'` is the derivative of `f` at `a` within `s`, and
 `y` belongs to the positive tangent cone of `s` at `a`, then `f' y ≤ 0`. -/
 theorem IsLocalMaxOn.hasFDerivWithinAt_nonpos {s : Set E} (h : IsLocalMaxOn f s a)
@@ -219,6 +220,10 @@ theorem IsLocalExtr.fderiv_eq_zero (h : IsLocalExtr f a) : fderiv ℝ f a = 0 :=
 
 end Module
 
+/-!
+### Fermat's Theorem
+-/
+
 section Real
 
 variable {f : ℝ → ℝ} {f' : ℝ} {a b : ℝ}
@@ -256,160 +261,3 @@ theorem IsLocalExtr.deriv_eq_zero (h : IsLocalExtr f a) : deriv f a = 0 :=
 #align is_local_extr.deriv_eq_zero IsLocalExtr.deriv_eq_zero
 
 end Real
-
-section Rolle
-
-variable (f f' : ℝ → ℝ) {a b : ℝ}
-
-/-- A continuous function on a closed interval with `f a = f b` takes either its maximum
-or its minimum value at a point in the interior of the interval. -/
-theorem exists_Ioo_extr_on_Icc (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
-    ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c := by
-  have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab)
-  -- Consider absolute min and max points
-  obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x :=
-    isCompact_Icc.exists_forall_le ne hfc
-  obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C :=
-    isCompact_Icc.exists_forall_ge ne hfc
-  by_cases hc : f c = f a
-  · by_cases hC : f C = f a
-    · have : ∀ x ∈ Icc a b, f x = f a := fun x hx => le_antisymm (hC ▸ Cge x hx) (hc ▸ cle x hx)
-      -- `f` is a constant, so we can take any point in `Ioo a b`
-      rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
-      refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
-      simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]
-    · refine' ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt _ hC, lt_of_le_of_ne Cmem.2 <| mt _ hC⟩, Or.inr Cge⟩
-      exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
-  · refine' ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt _ hc, lt_of_le_of_ne cmem.2 <| mt _ hc⟩, Or.inl cle⟩
-    exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
-#align exists_Ioo_extr_on_Icc exists_Ioo_extr_on_Icc
-
-/-- A continuous function on a closed interval with `f a = f b` has a local extremum at some
-point of the corresponding open interval. -/
-theorem exists_local_extr_Ioo (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
-    ∃ c ∈ Ioo a b, IsLocalExtr f c :=
-  let ⟨c, cmem, hc⟩ := exists_Ioo_extr_on_Icc f hab hfc hfI
-  ⟨c, cmem, hc.isLocalExtr <| Icc_mem_nhds cmem.1 cmem.2⟩
-#align exists_local_extr_Ioo exists_local_extr_Ioo
-
-/-- **Rolle's Theorem** `HasDerivAt` version -/
-theorem exists_hasDerivAt_eq_zero (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b)
-    (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) : ∃ c ∈ Ioo a b, f' c = 0 :=
-  let ⟨c, cmem, hc⟩ := exists_local_extr_Ioo f hab hfc hfI
-  ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩
-#align exists_has_deriv_at_eq_zero exists_hasDerivAt_eq_zero
-
-/-- **Rolle's Theorem** `deriv` version -/
-theorem exists_deriv_eq_zero (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
-    ∃ c ∈ Ioo a b, deriv f c = 0 :=
-  let ⟨c, cmem, hc⟩ := exists_local_extr_Ioo f hab hfc hfI
-  ⟨c, cmem, hc.deriv_eq_zero⟩
-#align exists_deriv_eq_zero exists_deriv_eq_zero
-
-variable {f f'} {l : ℝ}
-
-/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has derivative `f'`
-on `(a, b)` and has the same limit `l` at `𝓝[>] a` and `𝓝[<] b`, then `f' c = 0`
-for some `c ∈ (a, b)`.  -/
-theorem exists_hasDerivAt_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l))
-    (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) :
-    ∃ c ∈ Ioo a b, f' c = 0 := by
-  have : ContinuousOn f (Ioo a b) := fun x hx => (hff' x hx).continuousAt.continuousWithinAt
-  have hcont := continuousOn_Icc_extendFrom_Ioo hab.ne this hfa hfb
-  obtain ⟨c, hc, hcextr⟩ : ∃ c ∈ Ioo a b, IsLocalExtr (extendFrom (Ioo a b) f) c := by
-    apply exists_local_extr_Ioo _ hab hcont
-    rw [eq_lim_at_right_extendFrom_Ioo hab hfb]
-    exact eq_lim_at_left_extendFrom_Ioo hab hfa
-  use c, hc
-  apply (hcextr.congr _).hasDerivAt_eq_zero (hff' c hc)
-  rw [eventuallyEq_iff_exists_mem]
-  exact ⟨Ioo a b, Ioo_mem_nhds hc.1 hc.2, extendFrom_extends this⟩
-#align exists_has_deriv_at_eq_zero' exists_hasDerivAt_eq_zero'
-
-/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has the same limit
-`l` at `𝓝[>] a` and `𝓝[<] b`, then `deriv f c = 0` for some `c ∈ (a, b)`. This version
-does not require differentiability of `f` because we define `deriv f c = 0` whenever `f` is not
-differentiable at `c`. -/
-theorem exists_deriv_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l))
-    (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) : ∃ c ∈ Ioo a b, deriv f c = 0 :=
-  by_cases
-    (fun h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x =>
-      show ∃ c ∈ Ioo a b, deriv f c = 0 from
-        exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt)
-    fun h : ¬∀ x ∈ Ioo a b, DifferentiableAt ℝ f x =>
-    have h : ∃ x, x ∈ Ioo a b ∧ ¬DifferentiableAt ℝ f x := by push_neg at h; exact h
-    let ⟨c, hc, hcdiff⟩ := h
-    ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩
-#align exists_deriv_eq_zero' exists_deriv_eq_zero'
-
-end Rolle
-
-namespace Polynomial
-
-open scoped BigOperators
-
-/-- The number of roots of a real polynomial `p` is at most the number of roots of its derivative
-that are not roots of `p` plus one. -/
-theorem card_roots_toFinset_le_card_roots_derivative_diff_roots_succ (p : ℝ[X]) :
-    p.roots.toFinset.card ≤ (p.derivative.roots.toFinset \ p.roots.toFinset).card + 1 := by
-  cases' eq_or_ne (derivative p) 0 with hp' hp'
-  · rw [eq_C_of_derivative_eq_zero hp', roots_C, Multiset.toFinset_zero, Finset.card_empty]
-    exact zero_le _
-  have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
-  refine' Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => _
-  rw [Multiset.mem_toFinset, mem_roots hp] at hx hy
-  obtain ⟨z, hz1, hz2⟩ :=
-    exists_deriv_eq_zero (fun x : ℝ => eval x p) hxy p.continuousOn (hx.trans hy.symm)
-  refine' ⟨z, _, hz1⟩
-  rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
-#align polynomial.card_roots_to_finset_le_card_roots_derivative_diff_roots_succ Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ
-
-/-- The number of roots of a real polynomial is at most the number of roots of its derivative plus
-one. -/
-theorem card_roots_toFinset_le_derivative (p : ℝ[X]) :
-    p.roots.toFinset.card ≤ p.derivative.roots.toFinset.card + 1 :=
-  p.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ.trans <|
-    add_le_add_right (Finset.card_mono <| Finset.sdiff_subset _ _) _
-#align polynomial.card_roots_to_finset_le_derivative Polynomial.card_roots_toFinset_le_derivative
-
-/-- The number of roots of a real polynomial (counted with multiplicities) is at most the number of
-roots of its derivative (counted with multiplicities) plus one. -/
-theorem card_roots_le_derivative (p : ℝ[X]) :
-    Multiset.card p.roots ≤ Multiset.card (derivative p).roots + 1 :=
-  calc
-    Multiset.card p.roots = ∑ x in p.roots.toFinset, p.roots.count x :=
-      (Multiset.toFinset_sum_count_eq _).symm
-    _ = ∑ x in p.roots.toFinset, (p.roots.count x - 1 + 1) :=
-      (Eq.symm <| Finset.sum_congr rfl fun x hx => tsub_add_cancel_of_le <|
-        Nat.succ_le_iff.2 <| Multiset.count_pos.2 <| Multiset.mem_toFinset.1 hx)
-    _ = (∑ x in p.roots.toFinset, (p.rootMultiplicity x - 1)) + p.roots.toFinset.card := by
-      simp only [Finset.sum_add_distrib, Finset.card_eq_sum_ones, count_roots]
-    _ ≤ (∑ x in p.roots.toFinset, p.derivative.rootMultiplicity x) +
-          ((p.derivative.roots.toFinset \ p.roots.toFinset).card + 1) :=
-      (add_le_add
-        (Finset.sum_le_sum fun x _ => rootMultiplicity_sub_one_le_derivative_rootMultiplicity _ _)
-        p.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ)
-    _ ≤ (∑ x in p.roots.toFinset, p.derivative.roots.count x) +
-          ((∑ x in p.derivative.roots.toFinset \ p.roots.toFinset,
-            p.derivative.roots.count x) + 1) := by
-      simp only [← count_roots]
-      refine' add_le_add_left (add_le_add_right ((Finset.card_eq_sum_ones _).trans_le _) _) _
-      refine' Finset.sum_le_sum fun x hx => Nat.succ_le_iff.2 <| _
-      rw [Multiset.count_pos, ← Multiset.mem_toFinset]
-      exact (Finset.mem_sdiff.1 hx).1
-    _ = Multiset.card (derivative p).roots + 1 := by
-      rw [← add_assoc, ← Finset.sum_union Finset.disjoint_sdiff, Finset.union_sdiff_self_eq_union, ←
-        Multiset.toFinset_sum_count_eq, ← Finset.sum_subset (Finset.subset_union_right _ _)]
-      intro x _ hx₂
-      simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂
-#align polynomial.card_roots_le_derivative Polynomial.card_roots_le_derivative
-
-/-- The number of real roots of a polynomial is at most the number of roots of its derivative plus
-one. -/
-theorem card_rootSet_le_derivative {F : Type _} [CommRing F] [Algebra F ℝ] (p : F[X]) :
-    Fintype.card (p.rootSet ℝ) ≤ Fintype.card (p.derivative.rootSet ℝ) + 1 := by
-  simpa only [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, derivative_map] using
-    card_roots_toFinset_le_derivative (p.map (algebraMap F ℝ))
-#align polynomial.card_root_set_le_derivative Polynomial.card_rootSet_le_derivative
-
-end Polynomial
diff --git a/Mathlib/Analysis/Calculus/LocalExtr/Polynomial.lean b/Mathlib/Analysis/Calculus/LocalExtr/Polynomial.lean
new file mode 100644
index 0000000000000..9b0c84a254f07
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/LocalExtr/Polynomial.lean
@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2021 Benjamin Davidson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Davidson, Yury Kudryashov
+-/
+import Mathlib.Analysis.Calculus.LocalExtr.Rolle
+import Mathlib.Analysis.Calculus.Deriv.Polynomial
+import Mathlib.Topology.Algebra.Polynomial
+
+#align_import analysis.calculus.local_extr from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
+
+/-!
+# Rolle's Theorem for polynomials
+
+In this file we use Rolle's Theorem
+to relate the number of real roots of a real polynomial and its derivative.
+Namely, we prove the following facts.
+
+* `Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ`:
+  the number of roots of a real polynomial `p` is at most the number of roots of its derivative
+  that are not roots of `p` plus one.
+* `Polynomial.card_roots_toFinset_le_derivative`, `Polynomial.card_rootSet_le_derivative`:
+  the number of roots of a real polynomial
+  is at most the number of roots of its derivative plus one.
+* `Polynomial.card_roots_le_derivative`: same, but the roots are counted with multiplicities.
+
+## Keywords
+
+polynomial, Rolle's Theorem, root
+-/
+
+namespace Polynomial
+
+open scoped BigOperators
+
+/-- The number of roots of a real polynomial `p` is at most the number of roots of its derivative
+that are not roots of `p` plus one. -/
+theorem card_roots_toFinset_le_card_roots_derivative_diff_roots_succ (p : ℝ[X]) :
+    p.roots.toFinset.card ≤ (p.derivative.roots.toFinset \ p.roots.toFinset).card + 1 := by
+  cases' eq_or_ne (derivative p) 0 with hp' hp'
+  · rw [eq_C_of_derivative_eq_zero hp', roots_C, Multiset.toFinset_zero, Finset.card_empty]
+    exact zero_le _
+  have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
+  refine' Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => _
+  rw [Multiset.mem_toFinset, mem_roots hp] at hx hy
+  obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)
+  refine' ⟨z, _, hz1⟩
+  rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]
+#align polynomial.card_roots_to_finset_le_card_roots_derivative_diff_roots_succ Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ
+
+/-- The number of roots of a real polynomial is at most the number of roots of its derivative plus
+one. -/
+theorem card_roots_toFinset_le_derivative (p : ℝ[X]) :
+    p.roots.toFinset.card ≤ p.derivative.roots.toFinset.card + 1 :=
+  p.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ.trans <|
+    add_le_add_right (Finset.card_mono <| Finset.sdiff_subset _ _) _
+#align polynomial.card_roots_to_finset_le_derivative Polynomial.card_roots_toFinset_le_derivative
+
+/-- The number of roots of a real polynomial (counted with multiplicities) is at most the number of
+roots of its derivative (counted with multiplicities) plus one. -/
+theorem card_roots_le_derivative (p : ℝ[X]) :
+    Multiset.card p.roots ≤ Multiset.card (derivative p).roots + 1 :=
+  calc
+    Multiset.card p.roots = ∑ x in p.roots.toFinset, p.roots.count x :=
+      (Multiset.toFinset_sum_count_eq _).symm
+    _ = ∑ x in p.roots.toFinset, (p.roots.count x - 1 + 1) :=
+      (Eq.symm <| Finset.sum_congr rfl fun x hx => tsub_add_cancel_of_le <|
+        Nat.succ_le_iff.2 <| Multiset.count_pos.2 <| Multiset.mem_toFinset.1 hx)
+    _ = (∑ x in p.roots.toFinset, (p.rootMultiplicity x - 1)) + p.roots.toFinset.card := by
+      simp only [Finset.sum_add_distrib, Finset.card_eq_sum_ones, count_roots]
+    _ ≤ (∑ x in p.roots.toFinset, p.derivative.rootMultiplicity x) +
+          ((p.derivative.roots.toFinset \ p.roots.toFinset).card + 1) :=
+      (add_le_add
+        (Finset.sum_le_sum fun x _ => rootMultiplicity_sub_one_le_derivative_rootMultiplicity _ _)
+        p.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ)
+    _ ≤ (∑ x in p.roots.toFinset, p.derivative.roots.count x) +
+          ((∑ x in p.derivative.roots.toFinset \ p.roots.toFinset,
+            p.derivative.roots.count x) + 1) := by
+      simp only [← count_roots]
+      refine' add_le_add_left (add_le_add_right ((Finset.card_eq_sum_ones _).trans_le _) _) _
+      refine' Finset.sum_le_sum fun x hx => Nat.succ_le_iff.2 <| _
+      rw [Multiset.count_pos, ← Multiset.mem_toFinset]
+      exact (Finset.mem_sdiff.1 hx).1
+    _ = Multiset.card (derivative p).roots + 1 := by
+      rw [← add_assoc, ← Finset.sum_union Finset.disjoint_sdiff, Finset.union_sdiff_self_eq_union, ←
+        Multiset.toFinset_sum_count_eq, ← Finset.sum_subset (Finset.subset_union_right _ _)]
+      intro x _ hx₂
+      simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂
+#align polynomial.card_roots_le_derivative Polynomial.card_roots_le_derivative
+
+/-- The number of real roots of a polynomial is at most the number of roots of its derivative plus
+one. -/
+theorem card_rootSet_le_derivative {F : Type _} [CommRing F] [Algebra F ℝ] (p : F[X]) :
+    Fintype.card (p.rootSet ℝ) ≤ Fintype.card (p.derivative.rootSet ℝ) + 1 := by
+  simpa only [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, derivative_map] using
+    card_roots_toFinset_le_derivative (p.map (algebraMap F ℝ))
+#align polynomial.card_root_set_le_derivative Polynomial.card_rootSet_le_derivative
+
+end Polynomial
diff --git a/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean b/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean
new file mode 100644
index 0000000000000..bfd94a198ac9c
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/LocalExtr/Rolle.lean
@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Anatole Dedecker
+-/
+import Mathlib.Analysis.Calculus.LocalExtr.Basic
+import Mathlib.Topology.Algebra.Order.Rolle
+
+#align_import analysis.calculus.local_extr from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
+
+/-!
+# Rolle's Theorem
+
+In this file we prove Rolle's Theorem. The theorem says that for a function `f : ℝ → ℝ` such that
+
+* $f$ is differentiable on an open interval $(a, b)$, $a < b$;
+* $f$ is continuous on the corresponding closed interval $[a, b]$;
+* $f(a) = f(b)$,
+
+there exists a point $c∈(a, b)$ such that $f'(c)=0$.
+
+We prove four versions of this theorem.
+
+* `exists_hasDerivAt_eq_zero` is closest to the statement given above. It assumes that at every
+  point $x ∈ (a, b)$ function $f$ has derivative $f'(x)$, then concludes that $f'(c)=0$ for some
+  $c∈(a, b)$.
+* `exists_deriv_eq_zero` deals with `deriv f` instead of an arbitrary function `f'` and a predicate
+  `has_deriv_at`; since we use zero as the "junk" value for `deriv f c`, this version does not
+  assume that `f` is differentiable on the open interval.
+* `exists_hasDerivAt_eq_zero'` is similar to `exists_hasDerivAt_eq_zero` but instead of assuming
+  continuity on the closed interval $[a, b]$ it assumes that $f$ tends to the same limit as $x$
+  tends to $a$ from the right and as $x$ tends to $b$ from the left.
+* `exists_deriv_eq_zero'` relates to `exists_deriv_eq_zero` as `exists_hasDerivAt_eq_zero'`
+  relates to ``exists_hasDerivAt_eq_zero`.
+
+## References
+
+* [Rolle's Theorem](https://en.wikipedia.org/wiki/Rolle's_theorem);
+
+## Tags
+
+local extremum, Rolle's Theorem
+-/
+
+open Set Filter Topology
+
+variable {f f' : ℝ → ℝ} {a b l : ℝ}
+
+/-- **Rolle's Theorem** `HasDerivAt` version -/
+theorem exists_hasDerivAt_eq_zero (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b)
+    (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) : ∃ c ∈ Ioo a b, f' c = 0 :=
+  let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo hab hfc hfI
+  ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩
+#align exists_has_deriv_at_eq_zero exists_hasDerivAt_eq_zero
+
+/-- **Rolle's Theorem** `deriv` version -/
+theorem exists_deriv_eq_zero (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
+    ∃ c ∈ Ioo a b, deriv f c = 0 :=
+  let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo hab hfc hfI
+  ⟨c, cmem, hc.deriv_eq_zero⟩
+#align exists_deriv_eq_zero exists_deriv_eq_zero
+
+/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has derivative `f'`
+on `(a, b)` and has the same limit `l` at `𝓝[>] a` and `𝓝[<] b`, then `f' c = 0`
+for some `c ∈ (a, b)`.  -/
+theorem exists_hasDerivAt_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l))
+    (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) :
+    ∃ c ∈ Ioo a b, f' c = 0 :=
+  let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo_of_tendsto hab
+    (fun x hx ↦ (hff' x hx).continuousAt.continuousWithinAt) hfa hfb
+  ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩
+#align exists_has_deriv_at_eq_zero' exists_hasDerivAt_eq_zero'
+
+/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has the same limit
+`l` at `𝓝[>] a` and `𝓝[<] b`, then `deriv f c = 0` for some `c ∈ (a, b)`. This version
+does not require differentiability of `f` because we define `deriv f c = 0` whenever `f` is not
+differentiable at `c`. -/
+theorem exists_deriv_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l))
+    (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) : ∃ c ∈ Ioo a b, deriv f c = 0 := by
+  by_cases h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
+  · exact exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt
+  · obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
+    · push_neg at h; exact h
+    exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩
+#align exists_deriv_eq_zero' exists_deriv_eq_zero'
diff --git a/Mathlib/Analysis/Calculus/MeanValue.lean b/Mathlib/Analysis/Calculus/MeanValue.lean
index 601cab48d6c88..805fbcd5d5ed4 100644
--- a/Mathlib/Analysis/Calculus/MeanValue.lean
+++ b/Mathlib/Analysis/Calculus/MeanValue.lean
@@ -5,7 +5,9 @@ Authors: Sébastien Gouëzel, Yury Kudryashov
 -/
 import Mathlib.Analysis.Calculus.Deriv.AffineMap
 import Mathlib.Analysis.Calculus.Deriv.Slope
-import Mathlib.Analysis.Calculus.LocalExtr
+import Mathlib.Analysis.Calculus.Deriv.Mul
+import Mathlib.Analysis.Calculus.Deriv.Comp
+import Mathlib.Analysis.Calculus.LocalExtr.Rolle
 import Mathlib.Analysis.Convex.Slope
 import Mathlib.Analysis.Convex.Normed
 import Mathlib.Data.IsROrC.Basic
@@ -717,7 +719,7 @@ theorem exists_ratio_hasDerivAt_eq_ratio_slope :
     ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
   have hhc : ContinuousOn h (Icc a b) :=
     (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
-  rcases exists_hasDerivAt_eq_zero h h' hab hhc hI hhh' with ⟨c, cmem, hc⟩
+  rcases exists_hasDerivAt_eq_zero hab hhc hI hhh' with ⟨c, cmem, hc⟩
   exact ⟨c, cmem, sub_eq_zero.1 hc⟩
 #align exists_ratio_has_deriv_at_eq_ratio_slope exists_ratio_hasDerivAt_eq_ratio_slope
 
diff --git a/Mathlib/Analysis/Calculus/Taylor.lean b/Mathlib/Analysis/Calculus/Taylor.lean
index 91257f3e7b0b0..81028ff7e3ab1 100644
--- a/Mathlib/Analysis/Calculus/Taylor.lean
+++ b/Mathlib/Analysis/Calculus/Taylor.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Moritz Doll. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Doll
 -/
+import Mathlib.Analysis.Calculus.Deriv.Pow
 import Mathlib.Analysis.Calculus.IteratedDeriv
 import Mathlib.Analysis.Calculus.MeanValue
 import Mathlib.Data.Polynomial.Module
diff --git a/Mathlib/Analysis/Complex/Polynomial.lean b/Mathlib/Analysis/Complex/Polynomial.lean
index 89e6dec09952e..9456eff2902d5 100644
--- a/Mathlib/Analysis/Complex/Polynomial.lean
+++ b/Mathlib/Analysis/Complex/Polynomial.lean
@@ -5,6 +5,8 @@ Authors: Chris Hughes, Junyan Xu
 -/
 import Mathlib.Analysis.Complex.Liouville
 import Mathlib.FieldTheory.IsAlgClosed.Basic
+import Mathlib.Analysis.Calculus.Deriv.Polynomial
+import Mathlib.Topology.Algebra.Polynomial
 
 #align_import analysis.complex.polynomial from "leanprover-community/mathlib"@"17ef379e997badd73e5eabb4d38f11919ab3c4b3"
 
diff --git a/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean b/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
index 6251e05dd5ab8..79706255634e0 100644
--- a/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
+++ b/Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yury Kudryashov
 -/
 import Mathlib.Analysis.Calculus.Deriv.Inv
+import Mathlib.Analysis.Calculus.Deriv.Polynomial
 import Mathlib.Analysis.Calculus.ExtendDeriv
 import Mathlib.Analysis.Calculus.IteratedDeriv
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
diff --git a/Mathlib/Analysis/SpecialFunctions/Sqrt.lean b/Mathlib/Analysis/SpecialFunctions/Sqrt.lean
index df7389215ec27..556a062dc9131 100644
--- a/Mathlib/Analysis/SpecialFunctions/Sqrt.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Sqrt.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import Mathlib.Analysis.Calculus.ContDiff
+import Mathlib.Analysis.Calculus.Deriv.Pow
 
 #align_import analysis.special_functions.sqrt from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 
diff --git a/Mathlib/NumberTheory/Liouville/Basic.lean b/Mathlib/NumberTheory/Liouville/Basic.lean
index 8f5f39f2c6acc..09ca27c95aa3e 100644
--- a/Mathlib/NumberTheory/Liouville/Basic.lean
+++ b/Mathlib/NumberTheory/Liouville/Basic.lean
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Jujian Zhang
 -/
 import Mathlib.Analysis.Calculus.MeanValue
+import Mathlib.Analysis.Calculus.Deriv.Polynomial
 import Mathlib.Data.Polynomial.DenomsClearable
 import Mathlib.Data.Real.Irrational
+import Mathlib.Topology.Algebra.Polynomial
 
 #align_import number_theory.liouville.basic from "leanprover-community/mathlib"@"04e80bb7e8510958cd9aacd32fe2dc147af0b9f1"
 
diff --git a/Mathlib/NumberTheory/ZetaValues.lean b/Mathlib/NumberTheory/ZetaValues.lean
index b7ac4247b6da3..4d73597bbe92c 100644
--- a/Mathlib/NumberTheory/ZetaValues.lean
+++ b/Mathlib/NumberTheory/ZetaValues.lean
@@ -5,6 +5,7 @@ Authors: David Loeffler
 -/
 import Mathlib.NumberTheory.BernoulliPolynomials
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
+import Mathlib.Analysis.Calculus.Deriv.Polynomial
 import Mathlib.Analysis.Fourier.AddCircle
 import Mathlib.Analysis.PSeries
 
diff --git a/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean b/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean
index a97333484b04d..f59c89a9f8748 100644
--- a/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean
+++ b/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Mantle, Jake Levinson
 -/
 import Mathlib.RingTheory.Polynomial.Hermite.Basic
-import Mathlib.Analysis.Calculus.Deriv.Pow
 import Mathlib.Analysis.Calculus.Deriv.Add
+import Mathlib.Analysis.Calculus.Deriv.Polynomial
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 
diff --git a/Mathlib/Topology/Algebra/Order/Rolle.lean b/Mathlib/Topology/Algebra/Order/Rolle.lean
new file mode 100644
index 0000000000000..82c024a91771e
--- /dev/null
+++ b/Mathlib/Topology/Algebra/Order/Rolle.lean
@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2019 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Topology.Algebra.Order.ExtendFrom
+import Mathlib.Topology.Algebra.Order.Compact
+import Mathlib.Topology.Algebra.Order.T5
+import Mathlib.Topology.LocalExtr
+
+#align_import analysis.calculus.local_extr from "leanprover-community/mathlib"@"3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe"
+
+/-!
+# Rolle's Theorem (topological part)
+
+In this file we prove the purely topological part of Rolle's Theorem:
+a function that is continuous on an interval $[a, b]$, $a<b$,
+has a local extremum at a point $x ∈ (a, b)$ provided that $f(a)=f(b)$.
+We also prove several variations of this statement.
+
+In `Mathlib/Analysis/Calculus/LocalExtr/Rolle` we use these lemmas
+to prove several versions of Rolle's Theorem from calculus.
+
+## Keywords
+local minimum, local maximum, extremum, Rolle's Theorem
+-/
+
+open Filter Set Topology
+
+variable
+  [ConditionallyCompleteLinearOrder X] [DenselyOrdered X] [TopologicalSpace X] [OrderTopology X]
+  [LinearOrder Y] [TopologicalSpace Y] [OrderTopology Y]
+  {f : X → Y} {a b : X} {l : Y}
+
+/-- A continuous function on a closed interval with `f a = f b`
+takes either its maximum or its minimum value at a point in the interior of the interval. -/
+theorem exists_Ioo_extr_on_Icc (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
+    ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c := by
+  have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab)
+  -- Consider absolute min and max points
+  obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x :=
+    isCompact_Icc.exists_forall_le ne hfc
+  obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C :=
+    isCompact_Icc.exists_forall_ge ne hfc
+  by_cases hc : f c = f a
+  · by_cases hC : f C = f a
+    · have : ∀ x ∈ Icc a b, f x = f a := fun x hx => le_antisymm (hC ▸ Cge x hx) (hc ▸ cle x hx)
+      -- `f` is a constant, so we can take any point in `Ioo a b`
+      rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
+      refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
+      simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]
+    · refine' ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt _ hC, lt_of_le_of_ne Cmem.2 <| mt _ hC⟩, Or.inr Cge⟩
+      exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
+  · refine' ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt _ hc, lt_of_le_of_ne cmem.2 <| mt _ hc⟩, Or.inl cle⟩
+    exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
+#align exists_Ioo_extr_on_Icc exists_Ioo_extr_on_Icc
+
+/-- A continuous function on a closed interval with `f a = f b`
+has a local extremum at some point of the corresponding open interval. -/
+theorem exists_isLocalExtr_Ioo (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
+    ∃ c ∈ Ioo a b, IsLocalExtr f c :=
+  let ⟨c, cmem, hc⟩ := exists_Ioo_extr_on_Icc hab hfc hfI
+  ⟨c, cmem, hc.isLocalExtr <| Icc_mem_nhds cmem.1 cmem.2⟩
+#align exists_local_extr_Ioo exists_isLocalExtr_Ioo
+
+/-- If a function `f` is continuous on an open interval
+and tends to the same value at its endpoints, then it has an extremum on this open interval. -/
+lemma exists_isExtrOn_Ioo_of_tendsto (hab : a < b) (hfc : ContinuousOn f (Ioo a b))
+    (ha : Tendsto f (𝓝[>] a) (𝓝 l)) (hb : Tendsto f (𝓝[<] b) (𝓝 l)) :
+    ∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c := by
+  have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b) := extendFrom_extends hfc
+  obtain ⟨c, hc, hfc⟩ : ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c :=
+    exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hab.ne hfc ha hb)
+      ((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)
+  exact ⟨c, hc, (hfc.on_subset Ioo_subset_Icc_self).congr h (h hc)⟩
+
+/-- If a function `f` is continuous on an open interval
+and tends to the same value at its endpoints,
+then it has a local extremum on this open interval. -/
+lemma exists_isLocalExtr_Ioo_of_tendsto (hab : a < b) (hfc : ContinuousOn f (Ioo a b))
+    (ha : Tendsto f (𝓝[>] a) (𝓝 l)) (hb : Tendsto f (𝓝[<] b) (𝓝 l)) :
+    ∃ c ∈ Ioo a b, IsLocalExtr f c :=
+  let ⟨c, cmem, hc⟩ := exists_isExtrOn_Ioo_of_tendsto hab hfc ha hb
+  ⟨c, cmem, hc.isLocalExtr $ Ioo_mem_nhds cmem.1 cmem.2⟩