awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
this : Icc a b ∈ 𝓝 c
⊢ f' c - m = 0

Tactic:
(hc.isLocalMin this).hasDerivAt_eq_zero ((hg c cmem).hasDerivAt this)

Premises used: IsLocalMin.hasDerivAt_eq_zero, IsMinOn.isLocalMin, HasDerivWithinAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
this : Icc a b ∈ 𝓝 c
⊢ f' c - m = 0

Tactic:
exact (hc.isLocalMin this).hasDerivAt_eq_zero ((hg c cmem).hasDerivAt this)

Premises used: IsLocalMin.hasDerivAt_eq_zero, IsMinOn.isLocalMin, HasDerivWithinAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : m < f' a
hmb : f' b < m
⊢ m ∈ f' '' Ioo a b

Tactic:
let ⟨c, cmem, hc⟩ :=
    exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x hx).neg) (neg_lt_neg hma)
      (neg_lt_neg hmb)
  ⟨c, cmem, neg_injective hc⟩

Premises used: exists_hasDerivWithinAt_eq_of_gt_of_lt, neg_injective, _private.0.exists_hasDerivWithinAt_eq_of_lt_of_gt.match_1, Membership.mem, neg_lt_neg, HasDerivWithinAt.neg, And.intro, Exists.intro, Set.image, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hs₁ : ∀ x ∈ f' '' s, ∀ y ∈ f' '' s, x < y → Ioo x y ⊆ f' '' s
⊢ (f' '' s).OrdConnected

Tactic:
apply ordConnected_of_Ioo

Premises used: Set.ordConnected_of_Ioo
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hs₁ : ∀ (hab : a ≤ b), m ∈ f' '' s
hs₂ : ∀ (hab : b ≤ a), m ∈ f' '' s
⊢ m ∈ f' '' s

Tactic:
rcases le_total a b with hab | hab

Premises used: le_total
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
⊢ Icc a b ⊆ s

Tactic:
have : Icc a b ⊆ s := hs.out ha hb
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
hs₁ : ∀ (c : ℝ) (cmem : c ∈ Ioo a b) (hc : f' c = m), m ∈ f' '' s
⊢ m ∈ f' '' s

Tactic:
rcases exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x <| this hx).mono this) hma
        hmb with
      ⟨c, cmem, hc⟩

Premises used: exists_hasDerivWithinAt_eq_of_gt_of_lt, HasDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
c : ℝ
cmem : c ∈ Ioo a b
hc : f' c = m
⊢ m ∈ f' '' s

Tactic:
⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩

Premises used: Set.Ioo_subset_Icc_self, Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
c : ℝ
cmem : c ∈ Ioo a b
hc : f' c = m
⊢ m ∈ f' '' s

Tactic:
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
⊢ Icc b a ⊆ s

Tactic:
have : Icc b a ⊆ s := hs.out hb ha
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
hs₁ : ∀ (c : ℝ) (cmem : c ∈ Ioo b a) (hc : f' c = m), m ∈ f' '' s
⊢ m ∈ f' '' s

Tactic:
rcases exists_hasDerivWithinAt_eq_of_lt_of_gt hab (fun x hx => (hf x <| this hx).mono this) hmb
        hma with
      ⟨c, cmem, hc⟩

Premises used: exists_hasDerivWithinAt_eq_of_lt_of_gt, HasDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
c : ℝ
cmem : c ∈ Ioo b a
hc : f' c = m
⊢ m ∈ f' '' s

Tactic:
⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩

Premises used: Set.Ioo_subset_Icc_self, Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
c : ℝ
cmem : c ∈ Ioo b a
hc : f' c = m
⊢ m ∈ f' '' s

Tactic:
exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : DifferentiableOn ℝ f s
⊢ (derivWithin f s '' s).OrdConnected

Tactic:
hs.image_hasDerivWithinAt fun x hx => (hf x hx).hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, Set.OrdConnected.image_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, DifferentiableAt ℝ f x
⊢ (deriv f '' s).OrdConnected

Tactic:
hs.image_hasDerivWithinAt fun x hx => (hf x hx).hasDerivAt.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, DifferentiableAt.hasDerivAt, Set.OrdConnected.image_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ Convex ℝ (f' '' s)

Tactic:
(hs.ordConnected.image_hasDerivWithinAt hf).convex

Premises used: Set.OrdConnected.convex, Convex.ordConnected, Set.OrdConnected.image_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : DifferentiableOn ℝ f s
⊢ Convex ℝ (derivWithin f s '' s)

Tactic:
(hs.ordConnected.image_derivWithin hf).convex

Premises used: Set.OrdConnected.image_derivWithin, Set.OrdConnected.convex, Convex.ordConnected
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, DifferentiableAt ℝ f x
⊢ Convex ℝ (deriv f '' s)

Tactic:
(hs.ordConnected.image_deriv hf).convex

Premises used: Set.OrdConnected.image_deriv, Set.OrdConnected.convex, Convex.ordConnected
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a ≤ m
hmb : m ≤ f' b
⊢ m ∈ f' '' Icc a b

Tactic:
(ordConnected_Icc.image_hasDerivWithinAt hf).out (mem_image_of_mem _ (left_mem_Icc.2 hab))
    (mem_image_of_mem _ (right_mem_Icc.2 hab)) ⟨hma, hmb⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.OrdConnected.out, Set.ordConnected_Icc, Set.left_mem_Icc, Set.mem_image_of_mem, And.intro, Set.OrdConnected.image_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : ∀ x ∈ s, f' x ≠ m
contrapose! : ∀ (hf' : (∃ x ∈ s, m ≤ f' x) ∧ ∃ x ∈ s, f' x ≤ m), ∃ x ∈ s, f' x = m
⊢ (∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x

Tactic:
contrapose! hf'
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : (∃ x ∈ s, m ≤ f' x) ∧ ∃ x ∈ s, f' x ≤ m
rcases : ∀ (b : ℝ) (hb : b ∈ s) (hmb : m ≤ f' b) (a : ℝ) (ha : a ∈ s) (hma : f' a ≤ m), ∃ x ∈ s, f' x = m
⊢ ∃ x ∈ s, f' x = m

Tactic:
rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x ∈ s, f' x = m

Tactic:
(hs.ordConnected.image_hasDerivWithinAt hf).out (mem_image_of_mem f' ha)
    (mem_image_of_mem f' hb) ⟨hma, hmb⟩

Premises used: Set.Mem, setOf, Set.OrdConnected.out, Set.mem_image_of_mem, And.intro, Convex.ordConnected, Set.image, Set.OrdConnected.image_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x ∈ s, f' x = m

Tactic:
exact (hs.ordConnected.image_hasDerivWithinAt hf).out (mem_image_of_mem f' ha)
    (mem_image_of_mem f' hb) ⟨hma, hmb⟩

Premises used: Set.OrdConnected.out, Set.mem_image_of_mem, And.intro, Convex.ordConnected, Set.OrdConnected.image_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
n : ℕ∞
x : ℝ
hx : x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : ℝ) ↦ |x|) x

Tactic:
contDiffAt_norm ℝ hx

Premises used: Real, contDiffAt_norm
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ∞
f : E → ℝ
x : E
hf : ContDiffAt ℝ (↑n : WithTop ℕ∞) f x
h₀ : f x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : E) ↦ |f x|) x

Tactic:
hf.norm ℝ h₀

Premises used: Real, ContDiffAt.norm
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
n : ℕ∞
x : ℝ
hx : x ≠ 0
s : Set ℝ
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : ℝ) ↦ |x|) s x

Tactic:
(contDiffAt_abs hx).contDiffWithinAt

Premises used: ContDiffAt.contDiffWithinAt, contDiffAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ∞
f : E → ℝ
s : Set E
x : E
hf : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) f s x
h₀ : f x ≠ 0
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ |f y|) s x

Tactic:
(contDiffAt_abs h₀).comp_contDiffWithinAt x hf

Premises used: abs, ContDiffAt.comp_contDiffWithinAt, contDiffAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
n : ℕ∞
s : Set ℝ
hs : ∀ x ∈ s, x ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : ℝ) ↦ |x|) s

Tactic:
fun x hx ↦ contDiffWithinAt_abs (hs x hx) s

Premises used: ContDiffOn, contDiffWithinAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ∞
f : E → ℝ
s : Set E
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
h₀ : ∀ x ∈ s, f x ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (y : E) ↦ |f y|) s

Tactic:
fun x hx ↦ (hf x hx).abs (h₀ x hx)

Premises used: ContDiffOn, ContDiffWithinAt.abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ∞
f : E → ℝ
hf : ContDiff ℝ (↑n : ℕ∞ω) f
h₀ : ∀ (x : E), f x ≠ 0
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (y : E) ↦ |f y|

Tactic:
contDiff_iff_contDiffAt.2 fun x ↦ hf.contDiffAt.abs (h₀ x)

Premises used: Iff.mpr, ContDiffAt.abs, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : x < 0
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (-1) x

Tactic:
(hasStrictDerivAt_neg x).congr_of_eventuallyEq <|
    EqOn.eventuallyEq_of_mem (fun _ hy ↦ (abs_of_neg (mem_Iio.1 hy)).symm) (Iio_mem_nhds hx)

Premises used: Set.mem_Iio, Iio_mem_nhds, abs_of_neg, Set.EqOn.eventuallyEq_of_mem, Iff.mp, Eq.symm, HasStrictDerivAt.congr_of_eventuallyEq, hasStrictDerivAt_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : x < 0
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (-1) x

Tactic:
(hasStrictDerivAt_abs_neg hx).hasDerivAt

Premises used: hasStrictDerivAt_abs_neg, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) 1 x

Tactic:
(hasStrictDerivAt_id x).congr_of_eventuallyEq <|
    EqOn.eventuallyEq_of_mem (fun _ hy ↦ (abs_of_pos (mem_Iio.1 hy)).symm) (Ioi_mem_nhds hx)

Premises used: Ioi_mem_nhds, Set.mem_Iio, Set.EqOn.eventuallyEq_of_mem, Iff.mp, abs_of_pos, Eq.symm, hasStrictDerivAt_id, HasStrictDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : 0 < x
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) 1 x

Tactic:
(hasStrictDerivAt_abs_pos hx).hasDerivAt

Premises used: hasStrictDerivAt_abs_pos, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : x ≠ 0
inl : ∀ (hx : x < 0), HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x
inr : ∀ (hx : 0 < x), HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x

Tactic:
obtain hx | hx := hx.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x

Tactic:
simpa [hx] using hasStrictDerivAt_abs_neg hx

Premises used: hasStrictDerivAt_abs_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x

Tactic:
simpa [hx] using hasStrictDerivAt_abs_pos hx

Premises used: hasStrictDerivAt_abs_pos
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x

Tactic:
(hasStrictDerivAt_abs hx).hasDerivAt

Premises used: hasStrictDerivAt_abs, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
⊢ HasStrictFDerivAt (F := ℝ) (fun (x : E) ↦ |f x|) (ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f') x

Tactic:
(hasStrictDerivAt_abs_neg h₀).hasStrictFDerivAt.comp x hf

Premises used: HasStrictDerivAt.hasStrictFDerivAt, hasStrictDerivAt_abs_neg, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
h :
  instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      -f' = ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f'
⊢ HasStrictFDerivAt (fun (x : E) ↦ |f x|) (-f') x

Tactic:
convert! (hasStrictDerivAt_abs_neg h₀).hasStrictFDerivAt.comp x hf using 1

Premises used: HasStrictDerivAt.hasStrictFDerivAt, hasStrictDerivAt_abs_neg, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  ∀ (y : E),
    Eq (α := ℝ) ((-f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f' : (a : E) → ℝ) y : ℝ)
⊢ -f' = ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f'

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : E
⊢ Eq (α := ℝ) ((-f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f' : (a : E) → ℝ) y : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
⊢ HasFDerivAt (F := ℝ) ((fun (x : ℝ) ↦ |x|) ∘ f) (ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f') x

Tactic:
(hasDerivAt_abs_neg h₀).hasFDerivAt.comp x hf

Premises used: hasDerivAt_abs_neg, HasDerivAt.hasFDerivAt, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
h :
  instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      -f' = ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f'
⊢ HasFDerivAt (fun (x : E) ↦ |f x|) (-f') x

Tactic:
convert! (hasDerivAt_abs_neg h₀).hasFDerivAt.comp x hf using 1

Premises used: hasDerivAt_abs_neg, HasDerivAt.hasFDerivAt, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  ∀ (y : E),
    Eq (α := ℝ) ((-f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f' : (a : E) → ℝ) y : ℝ)
⊢ -f' = ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f'

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x < 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : E
⊢ Eq (α := ℝ) ((-f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f' : (a : E) → ℝ) y : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
⊢ HasStrictFDerivAt (F := ℝ) (fun (x : E) ↦ |f x|) (ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f') x

Tactic:
(hasStrictDerivAt_abs_pos h₀).hasStrictFDerivAt.comp x hf

Premises used: hasStrictDerivAt_abs_pos, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
h :
  instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      f' = ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f'
⊢ HasStrictFDerivAt (fun (x : E) ↦ |f x|) f' x

Tactic:
convert! (hasStrictDerivAt_abs_pos h₀).hasStrictFDerivAt.comp x hf using 1

Premises used: hasStrictDerivAt_abs_pos, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  ∀ (y : E),
    Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f' : (a : E) → ℝ) y : ℝ)
⊢ f' = ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f'

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : E
⊢ Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f' : (a : E) → ℝ) y : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
⊢ HasFDerivAt (F := ℝ) ((fun (x : ℝ) ↦ |x|) ∘ f) (ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f') x

Tactic:
(hasDerivAt_abs_pos h₀).hasFDerivAt.comp x hf

Premises used: HasDerivAt.hasFDerivAt, hasDerivAt_abs_pos, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
h :
  instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      f' = ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f'
⊢ HasFDerivAt (fun (x : E) ↦ |f x|) f' x

Tactic:
convert! (hasDerivAt_abs_pos h₀).hasFDerivAt.comp x hf using 1

Premises used: HasDerivAt.hasFDerivAt, hasDerivAt_abs_pos, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  ∀ (y : E),
    Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f' : (a : E) → ℝ) y : ℝ)
⊢ f' = ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f'

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : E
⊢ Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ 1 ∘SL f' : (a : E) → ℝ) y : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
⊢ HasStrictFDerivAt (F := ℝ) (fun (x : E) ↦ |f x|)
    (ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f') x

Tactic:
(hasStrictDerivAt_abs h₀).hasStrictFDerivAt.comp x hf

Premises used: hasStrictDerivAt_abs, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
h :
  instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' =
        ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f'
⊢ HasStrictFDerivAt (fun (x : E) ↦ |f x|) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f')
    x

Tactic:
convert! (hasStrictDerivAt_abs h₀).hasStrictFDerivAt.comp x hf using 1

Premises used: hasStrictDerivAt_abs, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.comp