awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : AntitoneOn g s
⊢ MonotoneOn (-g) s

Tactic:
have : MonotoneOn (-g) s := fun x hx y hy hxy ↦ by simpa using hg hx hy hxy
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : AntitoneOn g s
this : MonotoneOn (-g) s
⊢ g' ≤ 0

Tactic:
simpa using hd.neg.nonneg_of_monotoneOn hx this

Premises used: HasDerivWithinAt.nonneg_of_monotoneOn, HasDerivWithinAt.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : AntitoneOn g s
⊢ derivWithin g s x ≤ 0

Tactic:
simpa [derivWithin.fun_neg] using hg.neg.derivWithin_nonneg

Premises used: AntitoneOn.neg, derivWithin.fun_neg, MonotoneOn.derivWithin_nonneg
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivAt g g' x
hg : Antitone g
⊢ HasDerivWithinAt g g' univ x

Tactic:
rw [← hasDerivWithinAt_univ] at hd

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivAt g g' x
hg : Antitone g
hd₁ : HasDerivWithinAt g g' univ x
⊢ Antitone g

Tactic:
rw [← hasDerivWithinAt_univ] at hd

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Antitone g
apply : AccPt x (𝓟 univ)
⊢ g' ≤ 0

Tactic:
apply hd.nonpos_of_antitoneOn _ (hg.antitoneOn _)

Premises used: Antitone.antitoneOn, HasDerivWithinAt.nonpos_of_antitoneOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Antitone g
⊢ AccPt x (𝓟 univ)

Tactic:
PerfectSpace.univ_preperfect _ (mem_univ _)

Premises used: PerfectSpace.univ_preperfect, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Antitone g
⊢ AccPt x (𝓟 univ)

Tactic:
exact PerfectSpace.univ_preperfect _ (mem_univ _)

Premises used: PerfectSpace.univ_preperfect, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Antitone g
rw : derivWithin g univ x ≤ 0
⊢ deriv g x ≤ 0

Tactic:
rw [← derivWithin_univ]

Premises used: derivWithin_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Antitone g
⊢ derivWithin g univ x ≤ 0

Tactic:
(hg.antitoneOn univ).derivWithin_nonpos

Premises used: Antitone.antitoneOn, AntitoneOn.derivWithin_nonpos, Set.univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Antitone g
⊢ derivWithin g univ x ≤ 0

Tactic:
exact (hg.antitoneOn univ).derivWithin_nonpos

Premises used: Antitone.antitoneOn, AntitoneOn.derivWithin_nonpos, Set.univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
f : ℝ → ℝ
f' : ℝ
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : f' < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, slope f x z < r

Tactic:
hasDerivWithinAt_iff_tendsto_slope.1 hf (IsOpen.mem_nhds isOpen_Iio hr)

Premises used: Set.Mem, Filter.Eventually, setOf, isOpen_Iio, Set.preimage, IsOpen.mem_nhds, Iff.mp, Set.Iio, hasDerivWithinAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
f : ℝ → ℝ
f' : ℝ
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hs : x ∉ s
hr : f' < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, slope f x z < r

Tactic:
(hasDerivWithinAt_iff_tendsto_slope' hs).1 hf (IsOpen.mem_nhds isOpen_Iio hr)

Premises used: Set.Mem, Filter.Eventually, setOf, isOpen_Iio, Set.preimage, IsOpen.mem_nhds, Iff.mp, Set.Iio, hasDerivWithinAt_iff_tendsto_slope'
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
f : ℝ → ℝ
f' x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : f' < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r

Tactic:
(hf.Ioi_of_Ici.limsup_slope_le' (lt_irrefl x) hr).frequently

Premises used: lt_irrefl, HasDerivWithinAt.limsup_slope_le', Filter.Eventually.frequently, HasDerivWithinAt.Ioi_of_Ici
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
⊢ 0 < r

Tactic:
have hr₀ : 0 < r := lt_of_le_of_lt (norm_nonneg f') hr
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r

Tactic:
have A : ∀ᶠ z in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
    (hasDerivWithinAt_iff_tendsto_slope.1 hf).norm (IsOpen.mem_nhds isOpen_Iio hr)
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ Membership.mem (γ := Set ℝ) {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} x

Tactic:
simp [hr₀]
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r

Tactic:
have B : ∀ᶠ z in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r :=
    mem_of_superset self_mem_nhdsWithin (singleton_subset_iff.2 <| by simp [hr₀])
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
⊢ {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s \ {x}] x ⊔ 𝓝[{x}] x

Tactic:
have C := mem_sup.2 ⟨A, B⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C : {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s \ {x}] x ⊔ 𝓝[{x}] x
⊢ {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x

Tactic:
rw [← nhdsWithin_union, diff_union_self, nhdsWithin_union, mem_sup] at C

Premises used: Set.diff_union_self, Filter.mem_sup, nhdsWithin_union
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
h : ∀ (a : ℝ), ‖(a - x)⁻¹ • (f a - f x)‖ ∈ Iio r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r

Tactic:
filter_upwards [C.1]

Premises used: And.left
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
h : ∀ (a : ℝ), ‖a - x‖⁻¹ * ‖f a - f x‖ < r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
⊢ ∀ (a : ℝ), ‖(a - x)⁻¹ • (f a - f x)‖ ∈ Iio r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r

Tactic:
simp only [norm_smul, mem_Iio, norm_inv]

Premises used: Set.mem_Iio, norm_smul, norm_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ (a : ℝ), ‖a - x‖⁻¹ * ‖f a - f x‖ < r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r

Tactic:
fun _ => id

Premises used: id
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 : ℝ | (fun (z : ℝ) ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ (a : ℝ), ‖a - x‖⁻¹ * ‖f a - f x‖ < r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r

Tactic:
exact fun _ => id

Premises used: id
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
apply : ∀ (x_1 : ℝ), ‖x_1 - x‖⁻¹ * ‖f x_1 - f x‖ < r → ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
apply (hf.limsup_norm_slope_le hr).mono

Premises used: HasDerivWithinAt.limsup_norm_slope_le, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
z : ℝ
hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r
⊢ 0 ≤ ‖z - x‖⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
z : ℝ
hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r
⊢ ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
exact lt_of_le_of_lt (mul_le_mul_of_nonneg_left (norm_sub_norm_le _ _) (by positivity)) hz

Premises used: lt_of_le_of_lt, norm_sub_norm_le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r

Tactic:
(hf.Ioi_of_Ici.limsup_norm_slope_le hr).frequently

Premises used: HasDerivWithinAt.limsup_norm_slope_le, Filter.Eventually.frequently, HasDerivWithinAt.Ioi_of_Ici
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
⊢ ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r

Tactic:
have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
this.mp (Eventually.mono self_mem_nhdsWithin fun z hxz hz ↦ ?_)

Premises used: Filter.Eventually.mono, self_mem_nhdsWithin, Filter.Frequently.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
refine : ∀ (z : ℝ) (hxz : x < z) (hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
refine this.mp (Eventually.mono self_mem_nhdsWithin fun z hxz hz ↦ ?_)

Premises used: Filter.Eventually.mono, self_mem_nhdsWithin, Filter.Frequently.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.Slope
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
rwa : ∀ (hz : |z - x|⁻¹ * (‖f z‖ - ‖f x‖) < r), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hz : (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r), (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
rwa [Real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz

Premises used: abs_of_pos, Real.norm_eq_abs, sub_pos_of_lt
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
f' : F
inst_7 : TrivialStar 𝕜
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
⊢ HasDerivAtFilter (fun (x : 𝕜) ↦ star (f x)) (star f') L

Tactic:
simpa using h.hasFDerivAtFilter.star.hasDerivAtFilter

Premises used: HasFDerivAtFilter.star, HasDerivAtFilter.hasFDerivAtFilter, HasFDerivAtFilter.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
f' : F
x : 𝕜
inst_7 : TrivialStar 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ star (f x)) (star f') s x

Tactic:
HasDerivAtFilter.star h

Premises used: HasDerivWithinAt, HasDerivAtFilter.star
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
f' : F
x : 𝕜
inst_7 : TrivialStar 𝕜
h : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : 𝕜) ↦ star (f x)) (star f') x

Tactic:
HasDerivAtFilter.star h

Premises used: HasDerivAt, HasDerivAtFilter.star
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
f' : F
x : 𝕜
inst_7 : TrivialStar 𝕜
h : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ star (f x)) (star f') x

Tactic:
HasDerivAtFilter.star h

Premises used: HasDerivAtFilter.star, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst_7 : TrivialStar 𝕜
s : Set 𝕜
pos : ∀ (hxs : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)
neg : ∀ (hxs : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)
⊢ derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)

Tactic:
by_cases hxs : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst_7 : TrivialStar 𝕜
s : Set 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)

Tactic:
DFunLike.congr_fun (fderivWithin_star hxs) _

Premises used: DFunLike.congr_fun, fderivWithin_star, derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst_7 : TrivialStar 𝕜
s : Set 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)

Tactic:
exact DFunLike.congr_fun (fderivWithin_star hxs) _

Premises used: DFunLike.congr_fun, fderivWithin_star
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst_7 : TrivialStar 𝕜
s : Set 𝕜
hxs : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ star (f y)) s x = star (derivWithin f s x)

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hxs]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst_7 : TrivialStar 𝕜
⊢ deriv (fun (y : 𝕜) ↦ star (f y)) x = star (deriv f x)

Tactic:
DFunLike.congr_fun fderiv_star _

Premises used: DFunLike.congr_fun, deriv, fderiv_star
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
f : 𝕜 → F
inst_7 : TrivialStar 𝕜
⊢ Eq (α := (x : 𝕜) → F) (deriv fun (y : 𝕜) ↦ star (f y)) fun (x : 𝕜) ↦ star (deriv f x)

Tactic:
funext fun _ => deriv.star

Premises used: deriv.star, funext
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
f' : F
hf : HasDerivAt f f' x
⊢ HasFDerivAt (𝕜 := 𝕜) (star ∘ f ∘ star)
    ((↑(starL 𝕜) : F →L⋆[𝕜] F) ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 f' ∘SL (↑(starL 𝕜) : 𝕜 →L⋆[𝕜] 𝕜)) (star x)

Tactic:
hf.hasFDerivAt.star_star

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.star_star
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
f' : F
hf : HasDerivAt f f' x
h :
  Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜) →
      Eq (α := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (star f'))
        ((↑(starL 𝕜) : F →L⋆[𝕜] F) ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 f' ∘SL (↑(starL 𝕜) : 𝕜 →L⋆[𝕜] 𝕜))
⊢ HasFDerivAt (𝕜 := 𝕜) (E := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) : 𝕜 → F)
    (ContinuousLinearMap.toSpanSingleton 𝕜 (star f') : 𝕜 →L[𝕜] F) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
convert! hf.hasFDerivAt.star_star

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.star_star
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
f' : F
hf : HasDerivAt f f' x
e_4 : Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜)
h :
  Eq.{v + 1} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 (star f') : (a : 𝕜) → F) 1 : F)
    (((↑(starL 𝕜) : F →L⋆[𝕜] F) ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 f' ∘SL (↑(starL 𝕜) : 𝕜 →L⋆[𝕜] 𝕜) :
          (a : 𝕜) → F)
        1 :
      F)
⊢ Eq (α := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (star f'))
    ((↑(starL 𝕜) : F →L⋆[𝕜] F) ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 f' ∘SL (↑(starL 𝕜) : 𝕜 →L⋆[𝕜] 𝕜))

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
x : 𝕜
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
f' : F
hf : HasDerivAt f f' x
e_4 : Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜)
⊢ Eq.{v + 1} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 (star f') : (a : 𝕜) → F) 1 : F)
    (((↑(starL 𝕜) : F →L⋆[𝕜] F) ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 f' ∘SL (↑(starL 𝕜) : 𝕜 →L⋆[𝕜] 𝕜) :
          (a : 𝕜) → F)
        1 :
      F)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) f' x
⊢ HasDerivAt (𝕜 := 𝕜)
    (star ∘ Function.comp (β := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜) :
      𝕜 → F)
    (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
hf.star_conj

Premises used: HasDerivAt.star_conj
-- Module: Mathlib.Analysis.Calculus.Deriv.Star
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : StarRing 𝕜
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
inst_4 : StarAddMonoid F
inst_5 : StarModule 𝕜 F
inst_6 : ContinuousStar F
inst_7 : NormedStarGroup 𝕜
f : 𝕜 → F
x : 𝕜
f' : F
hf : HasDerivAt (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) f' x
h : f = star ∘ Function.comp (β := 𝕜) (star ∘ f ∘ (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)) (⇑(starRingEnd 𝕜) : (a : 𝕜) → 𝕜)
⊢ HasDerivAt f (star f') ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x)

Tactic:
convert! hf.star_conj

Premises used: HasDerivAt.star_conj