awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
h : ContDiffAt 𝕜' n f x
⊢ ContDiffAt 𝕜 n f x

Tactic:
contDiffWithinAt_univ.1 <| h.contDiffWithinAt.restrict_scalars _

Premises used: contDiffWithinAt_univ, ContDiffWithinAt.restrict_scalars, Iff.mp, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
h : ContDiff 𝕜' n f
⊢ ContDiff 𝕜 n f

Tactic:
contDiff_iff_contDiffAt.2 fun _ => h.contDiffAt.restrict_scalars _

Premises used: Iff.mpr, ContDiffAt.restrict_scalars, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Polynomial
Goal:
R : Type u_1
𝕜 : Type u_2
inst : CommSemiring R
inst_1 : NontriviallyNormedField 𝕜
inst_2 : Algebra R 𝕜
n : WithTop ℕ∞
f g : R[X]
fc : ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) f
gc : ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) g
⊢ ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) (f + g)

Tactic:
simpa using fc.add gc

Premises used: ContDiff.add
-- Module: Mathlib.Analysis.Calculus.ContDiff.Polynomial
Goal:
R : Type u_1
𝕜 : Type u_2
inst : CommSemiring R
inst_1 : NontriviallyNormedField 𝕜
inst_2 : Algebra R 𝕜
n_1 : WithTop ℕ∞
n : ℕ
a : R
⊢ ContDiff 𝕜 (F := 𝕜) n_1 fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) ((monomial n : (a : R) → R[X]) a : R[X])

Tactic:
simpa using contDiff_const.mul (contDiff_id.pow _)

Premises used: ContDiff.pow, contDiff_id, contDiff_const, ContDiff.mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Polynomial
Goal:
R : Type u_1
𝕜 : Type u_2
inst : CommSemiring R
inst_1 : NontriviallyNormedField 𝕜
inst_2 : Algebra R 𝕜
f : R[X]
n : WithTop ℕ∞
add :
  ∀ (f g : R[X]) (fc : ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) f)
    (gc : ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) g),
    ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) (f + g)
monomial :
  ∀ (n_1 : ℕ) (a : R),
    ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) ((Polynomial.monomial n_1 : (a : R) → R[X]) a : R[X])
⊢ ContDiff 𝕜 (F := 𝕜) n fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) f

Tactic:
induction f using Polynomial.induction_on' with
  | add f g fc gc => simpa using fc.add gc
  | monomial n a => simpa using contDiff_const.mul (contDiff_id.pow _)

Premises used: ContDiff.pow, contDiff_id, contDiff_const, Polynomial.monomial, ContDiff.mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
n : WithTop ℕ∞
s : Set E'
f : E' → F'
x : E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hf : HasFTaylorSeriesUpToOn.{u_1, u_2, u_3} (𝕜 := 𝕂) n f p s
hn : n ≠ 0
hs : s ∈ 𝓝 x
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f
    ((continuousMultilinearCurryFin1 𝕂 E' F' : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ E') F') → E' →L[𝕂] F')
      (p x 1))
    x

Tactic:
hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt (hf.eventually_hasFDerivAt hn hs) <|
    (continuousMultilinearCurryFin1 𝕂 E' F').continuousAt.comp <|
      (hf.cont 1 <| ENat.one_le_iff_ne_zero_withTop.mpr hn).continuousAt hs

Premises used: Iff.mpr, hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, HasFTaylorSeriesUpToOn.cont, continuousMultilinearCurryFin1, ENat.one_le_iff_ne_zero_withTop, LinearIsometryEquiv.continuousAt, ContinuousAt.comp, OfNat.ofNat, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : WithTop ℕ∞
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
hn : n ≠ 0
rcases :
  ∀ (u : Set E') (H : u ∈ 𝓝[insert x univ] x) (p : E' → FormalMultilinearSeries 𝕂 E' F')
    (hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p u), HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x

Tactic:
rcases hf.of_le (ENat.one_le_iff_ne_zero_withTop.mpr hn) 1 le_rfl with ⟨u, H, p, hp⟩

Premises used: Iff.mpr, le_rfl, ENat.one_le_iff_ne_zero_withTop, ContDiffAt.of_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : WithTop ℕ∞
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
hn : n ≠ 0
u : Set E'
H : u ∈ 𝓝[insert x univ] x
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p u
⊢ u ∈ 𝓝 x

Tactic:
simp only [nhdsWithin_univ, mem_univ, insert_eq_of_mem] at H

Premises used: nhdsWithin_univ, Set.insert_eq_of_mem, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : WithTop ℕ∞
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
hn : n ≠ 0
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p u
H : u ∈ 𝓝 x
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f
    ((continuousMultilinearCurryFin1 𝕂 E' F' : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ E') F') → E' →L[𝕂] F')
      (p x 1))
    x

Tactic:
have := hp.hasStrictFDerivAt one_ne_zero H
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : WithTop ℕ∞
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
f' : E' →L[𝕂] F'
x : E'
hf : ContDiffAt 𝕂 n f x
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x
hn : n ≠ 0
u : Set E'
p : E' → FormalMultilinearSeries 𝕂 E' F'
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p u
H : u ∈ 𝓝 x
this :
  HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f
    ((continuousMultilinearCurryFin1 𝕂 E' F' : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ E') F') → E' →L[𝕂] F')
      (p x 1))
    x
rwa rwa₁ rwa₂ rwa₃ :
  HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f
    ((continuousMultilinearCurryFin1 𝕂 E' F' : (a : ContinuousMultilinearMap 𝕂 (fun (i : Fin 1) ↦ E') F') → E' →L[𝕂] F')
      (p x 1))
    x
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f f' x

Tactic:
rwa [hf'.unique this.hasFDerivAt]

Premises used: HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.unique
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : WithTop ℕ∞
𝕂 : Type u_1
inst : RCLike 𝕂
F' : Type u_3
inst_1 : NormedAddCommGroup F'
inst_2 : NormedSpace 𝕂 F'
f : 𝕂 → F'
f' : F'
x : 𝕂
hf : ContDiffAt 𝕂 n f x
hf' : HasDerivAt f f' x
hn : n ≠ 0
⊢ HasStrictDerivAt f f' x

Tactic:
hf.hasStrictFDerivAt' hf' hn

Premises used: ContDiffAt.hasStrictFDerivAt', HasDerivAtFilter, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : WithTop ℕ∞
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
x : E'
hf : ContDiffAt 𝕂 n f x
hn : n ≠ 0
⊢ HasStrictFDerivAt f (fderiv 𝕂 f x) x

Tactic:
hf.hasStrictFDerivAt' (hf.differentiableAt hn).hasFDerivAt hn

Premises used: ContDiffAt.differentiableAt, ContDiffAt.hasStrictFDerivAt', DifferentiableAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : WithTop ℕ∞
𝕂 : Type u_1
inst : RCLike 𝕂
F' : Type u_3
inst_1 : NormedAddCommGroup F'
inst_2 : NormedSpace 𝕂 F'
f : 𝕂 → F'
x : 𝕂
hf : ContDiffAt 𝕂 n f x
hn : n ≠ 0
⊢ HasStrictDerivAt f (deriv f x) x

Tactic:
(hf.hasStrictFDerivAt hn).hasStrictDerivAt

Premises used: deriv, ContDiffAt.hasStrictFDerivAt, HasStrictFDerivAt.hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : ℕ∞ω
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
x : E'
hf : ContDiff 𝕂 n f
hn : n ≠ 0
⊢ HasStrictFDerivAt f (fderiv 𝕂 f x) x

Tactic:
hf.contDiffAt.hasStrictFDerivAt hn

Premises used: ContDiffAt.hasStrictFDerivAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
n : ℕ∞ω
𝕂 : Type u_1
inst : RCLike 𝕂
F' : Type u_3
inst_1 : NormedAddCommGroup F'
inst_2 : NormedSpace 𝕂 F'
f : 𝕂 → F'
x : 𝕂
hf : ContDiff 𝕂 n f
hn : n ≠ 0
⊢ HasStrictDerivAt f (deriv f x) x

Tactic:
hf.contDiffAt.hasStrictDerivAt hn

Premises used: ContDiffAt.hasStrictDerivAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : nnnorm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin 1) ↦ E) F) (p x 1) < K
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
⊢ ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y

Tactic:
have hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y := fun y hy =>
    (hf.hasFDerivWithinAt one_ne_zero (subset_insert x s hy)).mono (subset_insert x s)
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : nnnorm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin 1) ↦ E) F) (p x 1) < K
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
⊢ ContinuousWithinAt f' s x

Tactic:
have hcont : ContinuousWithinAt f' s x :=
    (continuousMultilinearCurryFin1 ℝ E F).continuousAt.comp_continuousWithinAt
      ((hf.cont _ le_rfl _ (mem_insert _ _)).mono (subset_insert x s))
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : nnnorm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin 1) ↦ E) F) (p x 1) < K
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
⊢ ‖f' x‖₊ < K

Tactic:
simpa only [f', LinearIsometryEquiv.nnnorm_map]

Premises used: LinearIsometryEquiv.nnnorm_map
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
hK : nnnorm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin 1) ↦ E) F) (p x 1) < K
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
⊢ ‖f' x‖₊ < K

Tactic:
replace hK : ‖f' x‖₊ < K := by simpa only [f', LinearIsometryEquiv.nnnorm_map]
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
hK : ‖f' x‖₊ < K
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
hs.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt
      (eventually_nhdsWithin_iff.2 <| Eventually.of_forall hder) hcont K hK

Premises used: Iff.mpr, Filter.Eventually.of_forall, eventually_nhdsWithin_iff, Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
K : ℝ≥0
f' : (y : E) → E →L[ℝ] F :=
  fun (y : E) ↦
    (continuousMultilinearCurryFin1 ℝ E F : (a : ContinuousMultilinearMap ℝ (fun (i : Fin 1) ↦ E) F) → E →L[ℝ] F)
      (p y 1)
hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
hK : ‖f' x‖₊ < K
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
exact
    hs.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt
      (eventually_nhdsWithin_iff.2 <| Eventually.of_forall hder) hcont K hK

Premises used: Iff.mpr, Filter.Eventually.of_forall, eventually_nhdsWithin_iff, Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
p : E → FormalMultilinearSeries ℝ E F
s : Set E
x : E
hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)
hs : Convex ℝ s
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
(exists_gt _).imp <| hf.exists_lipschitzOnWith_of_nnnorm_lt hs

Premises used: HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt, NoMaxOrder.exists_gt, Exists.imp
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
rcases :
  ∀ (t : Set E) (hst : t ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries ℝ E F)
    (hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p t), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rcases hf 1 le_rfl with ⟨t, hst, p, hp⟩

Premises used: le_rfl, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p t
rcases :
  ∀ (ε : ℝ) (ε0 : ε > 0) (hε : Metric.ball x ε ∩ insert x s ⊆ t), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rcases Metric.mem_nhdsWithin_iff.mp hst with ⟨ε, ε0, hε⟩

Premises used: Metric.mem_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
t : Set E
hst : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries ℝ E F
hp : HasFTaylorSeriesUpToOn (↑1 : WithTop ℕ∞) f p t
ε : ℝ
ε0 : ε > 0
hε : Metric.ball x ε ∩ insert x s ⊆ t
⊢ HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)

Tactic:
replace hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s) := hp.mono hε
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)
⊢ HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))

Tactic:
rw [← insert_eq_of_mem (Metric.mem_ball_self ε0), ← insert_inter_distrib] at hp

Premises used: Metric.mem_ball_self, Set.insert_eq_of_mem, Set.insert_inter_distrib
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
rcases :
  ∀ (K : ℝ≥0) (t : Set E) (hst : t ∈ 𝓝[Metric.ball x ε ∩ s] x) (hft : LipschitzOnWith K f t),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rcases hp.exists_lipschitzOnWith ((convex_ball _ _).inter hs) with ⟨K, t, hst, hft⟩

Premises used: Convex.inter, convex_ball, HasFTaylorSeriesUpToOn.exists_lipschitzOnWith
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[Metric.ball x ε ∩ s] x
hft : LipschitzOnWith K f t
⊢ t ∈ 𝓝[s] x

Tactic:
rw [inter_comm, ← nhdsWithin_restrict' _ (Metric.ball_mem_nhds _ ε0)] at hst

Premises used: nhdsWithin_restrict', Metric.ball_mem_nhds, Set.inter_comm
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[Metric.ball x ε ∩ s] x
hft : LipschitzOnWith K f t
hst₁ : t ∈ 𝓝[s] x
⊢ LipschitzOnWith K f t

Tactic:
rw [inter_comm, ← nhdsWithin_restrict' _ (Metric.ball_mem_nhds _ ε0)] at hst

Premises used: nhdsWithin_restrict', Metric.ball_mem_nhds, Set.inter_comm
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[s] x
hft : LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
⟨K, t, hst, hft⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
x : E
hf : ContDiffWithinAt ℝ 1 f s x
hs : Convex ℝ s
p : E → FormalMultilinearSeries ℝ E F
ε : ℝ
ε0 : ε > 0
hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))
K : ℝ≥0
t : Set E
hst : t ∈ 𝓝[s] x
hft : LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
exact ⟨K, t, hst, hft⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
x : E'
hf : ContDiffAt 𝕂 1 f x
K : ℝ≥0
hK : nnnorm (E := E' →L[𝕂] F') (fderiv 𝕂 f x) < K
⊢ ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
(hf.hasStrictFDerivAt one_ne_zero).exists_lipschitzOnWith_of_nnnorm_lt K hK

Premises used: ContDiffAt.hasStrictFDerivAt, one_ne_zero, HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
x : E'
hf : ContDiffAt 𝕂 1 f x
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
(hf.hasStrictFDerivAt one_ne_zero).exists_lipschitzOnWith

Premises used: HasStrictFDerivAt.exists_lipschitzOnWith, ContDiffAt.hasStrictFDerivAt, one_ne_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
hs : Convex ℝ s
hf : ContDiffOn ℝ 1 f s
x : E
hx : x ∈ s
obtain :
  ∀ (K : ℝ≥0) (t : Set E) (ht : t ∈ 𝓝[s] x) (hf : LipschitzOnWith K f t),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
obtain ⟨K, t, ht, hf⟩ := ContDiffWithinAt.exists_lipschitzOnWith (hf x hx) hs

Premises used: ContDiffWithinAt.exists_lipschitzOnWith
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
s : Set E
hs : Convex ℝ s
hf_1 : ContDiffOn ℝ 1 f s
x : E
hx : x ∈ s
K : ℝ≥0
t : Set E
ht : t ∈ 𝓝[s] x
hf : LipschitzOnWith K f t
w : ℝ≥0
w₁ : Set E
h : t ∈ 𝓝[s] x ∧ LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
use K, t
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
hf : ContDiff 𝕂 1 f
x : E'
rcases :
  ∀ (K : ℝ≥0) (t : Set E') (ht : t ∈ 𝓝 x) (hf : LipschitzOnWith K f t), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
rcases hf.contDiffAt.exists_lipschitzOnWith with ⟨K, t, ht, hf⟩

Premises used: ContDiffAt.exists_lipschitzOnWith, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.RCLike
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace 𝕂 E'
F' : Type u_3
inst_3 : NormedAddCommGroup F'
inst_4 : NormedSpace 𝕂 F'
f : E' → F'
hf_1 : ContDiff 𝕂 1 f
x : E'
K : ℝ≥0
t : Set E'
ht : t ∈ 𝓝 x
hf : LipschitzOnWith K f t
w : ℝ≥0
w₁ : Set E'
h : t ∈ 𝓝 x ∧ LipschitzOnWith K f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
use K, t