awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s : Set E
x : E
L : E →L[𝕜] F_1
v : E
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
hf : HasFDerivWithinAt f L s (F 0)
A : HasDerivWithinAt F (0 + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 1 v) (F ⁻¹' s) 0
⊢ HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F_1) v) s x v
have A₁ : HasDerivWithinAt F v (F ⁻¹' s) 0
Tactic: simp only [one_smul, zero_add] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
x : E
L : E →L[𝕜] F
hf : HasFDerivAt f L x
v : E
⊢ HasLineDerivAt 𝕜 f ((L : (a : E) → F) v) x v
have rw : HasLineDerivWithinAt 𝕜 f ((L : (a : E) → F) v) univ x v
Tactic: rw [← hasLineDerivWithinAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v
have h₁ : Membership.mem (γ := Filter 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)
Tactic: apply derivWithin_of_mem_nhds
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
s : Set E
x v : E
h : s ∈ 𝓝 x
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s)
have apply : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun (t : 𝕜) ↦ x + t • v
Tactic: apply (Continuous.continuousAt _).preimage_mem_nhds (by simpa using h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
f' : F
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
⊢ HasLineDerivWithinAt 𝕜 f f' s x v ↔ HasLineDerivWithinAt 𝕜 f f' t x v
have h₁ : EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
Tactic: apply hasDerivWithinAt_congr_set
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
f' : F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ ContinuousAt F 0
have h₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F
Tactic: apply Continuous.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
f' : F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
have B : ContinuousAt F 0
Tactic: have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
f' : F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ s =ᶠ[𝓝 (F 0)] t
have h₁ : F 0 = x
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
f' : F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
have this : s =ᶠ[𝓝 (F 0)] t
Tactic: have : s =ᶠ[𝓝 (F 0)] t := by convert! h; simp [F]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
⊢ lineDerivWithin 𝕜 f s x v = lineDerivWithin 𝕜 f t x v
have h₁ : EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
Tactic: apply derivWithin_congr_set
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ ContinuousAt F 0
have h₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F
Tactic: apply Continuous.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
have B : ContinuousAt F 0
Tactic: have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ s =ᶠ[𝓝 (F 0)] t
have h₁ : F 0 = x
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : E → F_1
s t : Set E
x v : E
h : s =ᶠ[𝓝 x] t
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ EventuallyEq.{u_1, 0} (α := 𝕜) (𝓝 0) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' s) ((fun (t : 𝕜) ↦ x + t • v) ⁻¹' t)
have this : s =ᶠ[𝓝 (F 0)] t
Tactic: have : s =ᶠ[𝓝 (F 0)] t := by convert! h; simp [F]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
⊢ HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v
have h₁ : EventuallyEq.{u_1, u_2} (β := F) (𝓝 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦ f₁ (x + t • v)
Tactic: apply hasDerivAt_iff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ ContinuousAt F 0
have h₁ : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] F
Tactic: apply Continuous.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
⊢ EventuallyEq.{u_1, u_2} (β := F_1) (𝓝 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦ f₁ (x + t • v)
have B : ContinuousAt F 0
Tactic: have B : ContinuousAt F 0 := by apply Continuous.continuousAt; fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ f₀ =ᶠ[𝓝 (F 0)] f₁
have h₁ : F 0 = x
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F_1 : Type u_2
inst_1 : NormedAddCommGroup F_1
inst_2 : NormedSpace 𝕜 F_1
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F_1
f' : F_1
x v : E
h : f₀ =ᶠ[𝓝 x] f₁
F : (t : 𝕜) → E := fun (t : 𝕜) ↦ x + t • v
B : ContinuousAt F 0
⊢ EventuallyEq.{u_1, u_2} (β := F_1) (𝓝 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦ f₁ (x + t • v)
have this : f₀ =ᶠ[𝓝 (F 0)] f₁
Tactic: have : f₀ =ᶠ[𝓝 (F 0)] f₁ := by convert! h; simp [F]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v
have h₁ : EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦
  f₁ (x + t • v)
Tactic: apply hasDerivWithinAt_iff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
h₁ :
  EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦
    f₁ (x + t • v)
⊢ HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v
have hx₁ : f₀ (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v) = f₁ (x + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)
Tactic: apply hasDerivWithinAt_iff
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f₀ f₁ : E → F
f' : F
s : Set E
x v : E
h : f₀ =ᶠ[𝓝[s] x] f₁
hx : f₀ x = f₁ x
⊢ EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₀ (x + t • v)) fun (t : 𝕜) ↦
    f₁ (x + t • v)
have A : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun (t : 𝕜) ↦ x + t • v
Tactic: have A : Continuous (fun (t : 𝕜) ↦ x + t • v) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v
have apply : EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₁ (x + t • v)) fun (t : 𝕜) ↦
  f (x + t • v)
Tactic: apply derivWithin_eq ?_ (by simpa using hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ EventuallyEq.{u_1, u_2} (β := F) (𝓝[(fun (t : 𝕜) ↦ x + t • v) ⁻¹' s] 0) (fun (t : 𝕜) ↦ f₁ (x + t • v)) fun (t : 𝕜) ↦
    f (x + t • v)
have A : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun (t : 𝕜) ↦ x + t • v
Tactic: have A : Continuous (fun (t : 𝕜) ↦ x + t • v) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f f₁ : E → F
x v : E
h : f₁ =ᶠ[𝓝 x] f
⊢ lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v
have rw : lineDerivWithin 𝕜 f₁ univ x v = lineDeriv 𝕜 f x v
Tactic: rw [← lineDerivWithin_univ, ← lineDerivWithin_univ, h.lineDerivWithin_eq_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f f₁ : E → F
x v : E
h : f₁ =ᶠ[𝓝 x] f
rw : lineDerivWithin 𝕜 f₁ univ x v = lineDeriv 𝕜 f x v
⊢ lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v
have rw₁ : lineDerivWithin 𝕜 f₁ univ x v = lineDerivWithin 𝕜 f univ x v
Tactic: rw [← lineDerivWithin_univ, ← lineDerivWithin_univ, h.lineDerivWithin_eq_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f f₁ : E → F
x v : E
h : f₁ =ᶠ[𝓝 x] f
rw : lineDerivWithin 𝕜 f₁ univ x v = lineDeriv 𝕜 f x v
rw₁ : lineDerivWithin 𝕜 f₁ univ x v = lineDerivWithin 𝕜 f univ x v
⊢ lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v
have rw₂ : lineDerivWithin 𝕜 f univ x v = lineDerivWithin 𝕜 f univ x v
Tactic: rw [← lineDerivWithin_univ, ← lineDerivWithin_univ, h.lineDerivWithin_eq_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖f'‖ ≤ C * ‖v‖
have apply : ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
Tactic: apply HasDerivAt.le_of_lip' hf (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
have A : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun (t : 𝕜) ↦ x₀ + t • v
Tactic: have A : Continuous (fun (t : 𝕜) ↦ x₀ + t • v) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
have this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
Tactic: have : ∀ᶠ x in 𝓝 (x₀ + (0 : 𝕜) • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖ := by simpa using hlip
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
have h : ∀ (t : 𝕜)
  (ht :
    Membership.mem (γ := Set 𝕜)
      (preimage.{u_1, u_3} (β := E) (fun (t : 𝕜) ↦ x₀ + t • v) {x : E | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}) t),
  ‖f (x₀ + t • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖t - 0‖
Tactic: filter_upwards [(A.continuousAt (x := 0)).preimage_mem_nhds this] with t ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
t : 𝕜
ht :
  Membership.mem (γ := Set 𝕜)
    (preimage.{u_1, u_3} (β := E) (fun (t : 𝕜) ↦ x₀ + t • v) {x : E | ‖f x - f x₀‖ ≤ C * ‖x - x₀‖}) t
⊢ ‖f (x₀ + t • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖t - 0‖
have ht₁ : ‖f (x₀ + t • v) - f x₀‖ ≤ C * (‖v‖ * ‖t‖)
Tactic: simp only [preimage_setOf_eq, add_sub_cancel_left, norm_smul, mem_setOf_eq, mul_comm (‖t‖)] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ (↑C : ℝ) * ‖v‖
have refine : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
Tactic: refine hf.le_of_lip' C.coe_nonneg ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
have h : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x : E | x ∈ s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖) x} x} a
Tactic: filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
f' : F
x₀ : E
hf : HasLineDerivAt 𝕜 f f' x₀ v
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | x ∈ s → Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖) x} x} a
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ (↑C : ℝ) * ‖x - x₀‖
have h₁ : ∀ a ∈ s, ‖f a - f x₀‖ ≤ (↑C : ℝ) * ‖a - x₀‖
Tactic: filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖
have apply : ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
Tactic: apply norm_deriv_le_of_lip' (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
have A : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun (t : 𝕜) ↦ x₀ + t • v
Tactic: have A : Continuous (fun (t : 𝕜) ↦ x₀ + t • v) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
A :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (t : 𝕜) ↦ x₀ + t • v
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, ‖f (x₀ + x • v) - f (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v)‖ ≤ C * ‖v‖ * ‖x - 0‖
have this : ∀ᶠ (x : E) in 𝓝 (x₀ + HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
Tactic: have : ∀ᶠ x in 𝓝 (x₀ + (0 : 𝕜) • v), ‖f x - f x₀‖ ≤ C * ‖x - x₀‖ := by simpa using hlip