awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
f : E → ℝ
a b : E
f' : ℝ
h : IsLocalMin f a
hd : HasLineDerivAt ℝ f f' a b
⊢ f' = 0

Tactic:
IsLocalExtr.hasLineDerivAt_eq_zero (.inl h) hd

Premises used: IsLocalExtr.hasLineDerivAt_eq_zero, Or.inl
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
f : E → ℝ
a : E
h : IsLocalMin f a
⊢ lineDeriv ℝ f a = 0

Tactic:
IsLocalExtr.lineDeriv_eq_zero (.inl h)

Premises used: IsLocalExtr.lineDeriv_eq_zero, Or.inl
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
f : E → ℝ
a b : E
f' : ℝ
h : IsLocalMax f a
hd : HasLineDerivAt ℝ f f' a b
⊢ f' = 0

Tactic:
IsLocalExtr.hasLineDerivAt_eq_zero (.inr h) hd

Premises used: IsLocalExtr.hasLineDerivAt_eq_zero, Or.inr
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
f : E → ℝ
a : E
h : IsLocalMax f a
⊢ lineDeriv ℝ f a = 0

Tactic:
IsLocalExtr.lineDeriv_eq_zero (.inr h)

Premises used: IsLocalExtr.lineDeriv_eq_zero, Or.inr
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
inl :
  ∀ (hp' : Eq (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])),
    p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
inr :
  ∀ (hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])),
    p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1

Tactic:
rcases eq_or_ne (derivative p) 0 with hp' | hp'

Premises used: Polynomial.derivative, eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Eq (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
inl :
  Finset.card (α := ℝ) (Multiset.toFinset (roots ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) ≤
    Finset.card (α := ℝ)
        (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) \
          Multiset.toFinset (roots ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) +
      1
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1

Tactic:
rw [eq_C_of_derivative_eq_zero hp']

Premises used: Polynomial.eq_C_of_derivative_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Eq (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
⊢ Finset.card (α := ℝ) (Multiset.toFinset (roots ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) ≤
    Finset.card (α := ℝ)
        (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) \
          Multiset.toFinset (roots ((C : (a : ℝ) → ℝ[X]) (p.coeff 0)))) +
      1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
⊢ Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) 0 : ℝ[X])

Tactic:
rwa [derivative_zero]

Premises used: Polynomial.derivative_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
⊢ p ≠ 0

Tactic:
have hp : p ≠ 0 := ne_of_apply_ne derivative (by rwa [derivative_zero])
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1

Tactic:
Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => ?_

Premises used: Finset.card_le_diff_of_interleaved
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
inr :
  ∀ (x : ℝ) (hx : x ∈ p.roots.toFinset) (y : ℝ) (hy : y ∈ p.roots.toFinset) (hxy : x < y)
    (hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y),
    ∃ (z : ℝ),
      Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
⊢ p.roots.toFinset.card ≤ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1

Tactic:
refine Finset.card_le_diff_of_interleaved fun x hx y hy hxy hxy' => ?_

Premises used: Finset.card_le_diff_of_interleaved
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : x ∈ p.roots.toFinset
y : ℝ
hy : y ∈ p.roots.toFinset
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
inr :
  ∀ (hx : p.IsRoot x) (y : ℝ) (hy : p.IsRoot y) (hxy : x < y) (hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y),
    ∃ (z : ℝ),
      Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
⊢ ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y

Tactic:
rw [Multiset.mem_toFinset, mem_roots hp] at hx hy

Premises used: Polynomial.mem_roots, Multiset.mem_toFinset
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
inr :
  ∀ (z : ℝ) (hz1 : z ∈ Set.Ioo x y) (hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0),
    ∃ (z : ℝ),
      Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y
⊢ ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y

Tactic:
obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero hxy p.continuousOn (hx.trans hy.symm)

Premises used: exists_deriv_eq_zero, Polynomial.continuousOn, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0
⊢ ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y

Tactic:
⟨z, ?_, hz1⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0
inr : Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z
⊢ ∃ (z : ℝ),
    Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z ∧ x < z ∧ z < y

Tactic:
refine ⟨z, ?_, hz1⟩
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
hp' : Ne (α := ℝ[X]) ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X]) (0 : ℝ[X])
hp : p ≠ 0
x : ℝ
hx : p.IsRoot x
y : ℝ
hy : p.IsRoot y
hxy : x < y
hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y
z : ℝ
hz1 : z ∈ Set.Ioo x y
hz2 : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0
inr : Membership.mem (γ := Multiset ℝ) (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) z
inr₁ : IsRoot ((derivative : (a : ℝ[X]) → ℝ[X]) p) z
inr₂ : eval z ((derivative : (a : ℝ[X]) → ℝ[X]) p) = 0
inr₃ inr₄ inr₅ inr₆ : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x p) z) 0
⊢ Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) z

Tactic:
rwa [Multiset.mem_toFinset, mem_roots hp', IsRoot, ← p.deriv]

Premises used: Polynomial.IsRoot, Polynomial.mem_roots, Polynomial.deriv, Multiset.mem_toFinset
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
grw grw₁ :
  Finset.card (α := ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) + 1 ≤
    Finset.card (α := ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) + 1
⊢ (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1 ≤
    Finset.card (α := ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) + 1

Tactic:
grw [Finset.sdiff_subset]

Premises used: Finset.sdiff_subset
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, (Multiset.count x p.roots - 1 + 1) =
    ∑ x ∈ p.roots.toFinset, (rootMultiplicity x p - 1) + p.roots.toFinset.card

Tactic:
simp only [Finset.sum_add_distrib, Finset.card_eq_sum_ones, count_roots]

Premises used: Finset.card_eq_sum_ones, Finset.sum_add_distrib, Polynomial.count_roots
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
simp :
  ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ) (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset, 1)
        1 ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ)
        (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset,
          Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)))
        1
⊢ ∑ x ∈ p.roots.toFinset, rootMultiplicity x ((derivative : (a : ℝ[X]) → ℝ[X]) p) +
      ((Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset).card + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ)
        (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset,
          Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)))
        1

Tactic:
simp only [← count_roots, Finset.card_eq_sum_ones]

Premises used: Finset.card_eq_sum_ones, Polynomial.count_roots
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
bc :
  ∀ (x : ℝ) (hx : x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset),
    1 ≤ Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ) (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset, 1)
        1 ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ)
        (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset,
          Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)))
        1

Tactic:
gcongr with x hx
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset
bc : Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) x
⊢ 1 ≤ Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))

Tactic:
rw [Nat.succ_le_iff, Multiset.count_pos, ← Multiset.mem_toFinset]

Premises used: Multiset.count_pos, Nat.succ_le_iff, Multiset.mem_toFinset
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset
⊢ Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) x

Tactic:
(Finset.mem_sdiff.1 hx).1

Premises used: Finset.mem_sdiff, And.left, Iff.mp
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
x : ℝ
hx : x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset
⊢ Membership.mem (γ := Finset ℝ) (Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))) x

Tactic:
exact (Finset.mem_sdiff.1 hx).1

Premises used: Finset.mem_sdiff, And.left, Iff.mp
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
rw :
  ∀ x ∈ p.roots.toFinset ∪ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)),
    x ∉ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) →
      Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) = 0
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) +
      HAdd.hAdd (α := ℕ)
        (∑ x ∈ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) \ p.roots.toFinset,
          Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)))
        1 =
    Multiset.card (α := ℝ) (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) + 1

Tactic:
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]

Premises used: Finset.union_sdiff_self_eq_union, Multiset.toFinset_sum_count_eq, add_assoc, Finset.sum_union, Finset.disjoint_sdiff, Finset.sum_subset, Finset.subset_union_right
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
x : ℝ
_ :
  x ∈ p.roots.toFinset ∪ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) →
    x ∉ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) →
      Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) = 0
⊢ x ∈ p.roots.toFinset ∪ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) →
    x ∉ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) →
      Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) = 0

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
p : ℝ[X]
x : ℝ
h : x ∈ p.roots.toFinset ∪ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))
hx₂ : x ∉ Multiset.toFinset (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p))
⊢ Multiset.count x (roots ((derivative : (a : ℝ[X]) → ℝ[X]) p)) = 0

Tactic:
simpa only [Multiset.mem_toFinset, Multiset.count_eq_zero] using hx₂

Premises used: Multiset.count_eq_zero, Multiset.mem_toFinset
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial
Goal:
F : Type u_1
inst : CommRing F
inst_1 : Algebra F ℝ
p : F[X]
⊢ Fintype.card (↑(p.rootSet ℝ) : Type) ≤
    Fintype.card (↑(rootSet.{u_1, 0} (T := F) ((derivative : (a : F[X]) → F[X]) p) ℝ) : Type) + 1

Tactic:
simpa only [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, derivative_map] using
    card_roots_toFinset_le_derivative (p.map (algebraMap F ℝ))

Premises used: Finset.coe_sort_coe, Real, Algebra.algebraMap, Polynomial.rootSet_def, Polynomial.map, Polynomial.derivative_map, Fintype.card_coe, Polynomial.card_roots_toFinset_le_derivative
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f f' : ℝ → ℝ
a b : ℝ
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

Tactic:
let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo hab hfc hfI
  ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩

Premises used: _private.0.exists_hasDerivAt_eq_zero.match_1, exists_isLocalExtr_Ioo, Membership.mem, Exists, And, And.intro, Exists.intro, IsLocalExtr.hasDerivAt_eq_zero, OfNat.ofNat, Eq, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo hab hfc hfI
  ⟨c, cmem, hc.deriv_eq_zero⟩

Premises used: _private.0.exists_hasDerivAt_eq_zero.match_1, exists_isLocalExtr_Ioo, deriv, Membership.mem, Exists, IsLocalExtr.deriv_eq_zero, And, And.intro, Exists.intro, OfNat.ofNat, Eq, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f f' : ℝ → ℝ
a b l : ℝ
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

Tactic:
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⟩

Premises used: _private.0.exists_hasDerivAt_eq_zero'.match_1, ContinuousAt.continuousWithinAt, Membership.mem, Exists, exists_isLocalExtr_Ioo_of_tendsto, HasDerivAt.continuousAt, And, And.intro, Exists.intro, IsLocalExtr.hasDerivAt_eq_zero, OfNat.ofNat, Eq, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
pos : ∀ (h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x), ∃ c ∈ Ioo a b, deriv f c = 0
neg : ∀ (h : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x), ∃ c ∈ Ioo a b, deriv f c = 0
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
by_cases! h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x

Premises used: Set.Ioo
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, exists_hasDerivAt_eq_zero'
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
exact exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, exists_hasDerivAt_eq_zero'
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
⊢ ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x

Tactic:
h
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
h : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
neg : ∀ (c : ℝ) (hc : c ∈ Ioo a b) (hcdiff : ¬DifferentiableAt ℝ f c), ∃ c ∈ Ioo a b, deriv f c = 0
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x := h

Premises used: Set.Ioo
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
c : ℝ
hc : c ∈ Ioo a b
hcdiff : ¬DifferentiableAt ℝ f c
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩

Premises used: deriv_zero_of_not_differentiableAt, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Rolle
Goal:
f : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[>] a) (𝓝 l)
hfb : Tendsto f (𝓝[<] b) (𝓝 l)
c : ℝ
hc : c ∈ Ioo a b
hcdiff : ¬DifferentiableAt ℝ f c
⊢ ∃ c ∈ Ioo a b, deriv f c = 0

Tactic:
exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
⊢ logDeriv f x = deriv f x / f x

Tactic:
rfl

Premises used: logDeriv, rfl
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ logDeriv f x = 0

Tactic:
simp only [logDeriv_apply, deriv_zero_of_not_differentiableAt h, zero_div]

Premises used: deriv_zero_of_not_differentiableAt, zero_div, logDeriv_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv id x = 1 / x

Tactic:
simp [logDeriv_apply]

Premises used: logDeriv_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv (fun (x : 𝕜) ↦ x) x = 1 / x

Tactic:
logDeriv_id x

Premises used: logDeriv_id
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
a : 𝕜'
h : ∀ (x : 𝕜), Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ a) x) (0 x)
⊢ Eq (α := (x : 𝕜) → 𝕜') (logDeriv fun (x : 𝕜) ↦ a) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
a : 𝕜'
x : 𝕜
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ a) x) (0 x)

Tactic:
simp [logDeriv_apply]

Premises used: logDeriv_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ logDeriv (fun (z : 𝕜) ↦ f z * g z) x = logDeriv f x + logDeriv g x

Tactic:
simp [field, logDeriv_apply, *]

Premises used: logDeriv_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ logDeriv (fun (z : 𝕜) ↦ f z / g z) x = logDeriv f x - logDeriv g x

Tactic:
simp [field, logDeriv_apply, *]

Premises used: logDeriv_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
a : 𝕜'
ha : a ≠ 0
⊢ logDeriv (fun (z : 𝕜) ↦ f z * a) x = logDeriv f x

Tactic:
simp only [logDeriv_apply, deriv_mul_const_field, mul_div_mul_right _ _ ha]

Premises used: mul_div_mul_right, deriv_mul_const_field, logDeriv_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
a : 𝕜'
ha : a ≠ 0
⊢ logDeriv (fun (z : 𝕜) ↦ a * f z) x = logDeriv f x

Tactic:
simp only [logDeriv_apply, deriv_const_mul_field, mul_div_mul_left _ _ ha]

Premises used: deriv_const_mul_field, logDeriv_apply, mul_div_mul_left
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i x ≠ 0
hd : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → DifferentiableAt 𝕜 (f i) x
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ ∅, f i x) x) (∑ i ∈ ∅, logDeriv (f i) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : ∀ i ∈ Finset.cons a s ha, f i x ≠ 0
hd : ∀ i ∈ Finset.cons a s ha, DifferentiableAt 𝕜 (f i) x
⊢ f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0

Tactic:
rw [Finset.forall_mem_cons] at hf hd

Premises used: Finset.forall_mem_cons