awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
rw₁ : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
⊢ derivWithin f s x = 0
have rw₂ : Eq.{v + 1} (α := F) 0 0
Tactic: rw [derivWithin, fderivWithin_zero_of_notMem_closure h, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x = 0
have unfold : Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
Tactic: unfold deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
have rw : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
Tactic: rw [fderiv_zero_of_not_differentiableAt h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f' : F
hf' : f' ≠ 0
⊢ Topology.IsInducing.{u, v} (X := 𝕜) (Y := F) (⇑(toSpanSingleton 𝕜 f') : (a : 𝕜) → F)
have refine : AntilipschitzWith.{u, v} (α := 𝕜) (β := F) ‖f'‖₊⁻¹ (⇑(toSpanSingleton 𝕜 f') : (a : 𝕜) → F)
Tactic: refine AntilipschitzWith.isInducing (K := ‖f'‖₊⁻¹) ?_ (map_continuous _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x
have rw : HasDerivWithinAt f f' (Ici x \ {x}) x ↔ HasDerivWithinAt f f' (Ici x) x
Tactic: rw [← Ici_diff_left, hasDerivWithinAt_diff_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : PartialOrder 𝕜
rw : HasDerivWithinAt f f' (Ici x \ {x}) x ↔ HasDerivWithinAt f f' (Ici x) x
⊢ HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x
have rw₁ : HasDerivWithinAt f f' (Ici x) x ↔ HasDerivWithinAt f f' (Ici x) x
Tactic: rw [← Ici_diff_left, hasDerivWithinAt_diff_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x
have rw : HasDerivWithinAt f f' (Iic x \ {x}) x ↔ HasDerivWithinAt f f' (Iic x) x
Tactic: rw [← Iic_diff_right, hasDerivWithinAt_diff_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : PartialOrder 𝕜
rw : HasDerivWithinAt f f' (Iic x \ {x}) x ↔ HasDerivWithinAt f f' (Iic x) x
⊢ HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x
have rw₁ : HasDerivWithinAt f f' (Iic x) x ↔ HasDerivWithinAt f f' (Iic x) x
Tactic: rw [← Iic_diff_right, hasDerivWithinAt_diff_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x y : 𝕜
⊢ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) y = y • deriv f x
have rw : Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) y : F)
  (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) (HSMul.hSMul (β := 𝕜) y 1) : F)
Tactic: rw [← fderiv_apply_one_eq_deriv, ← map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.derivWithin f s x = deriv f x
have unfold : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: unfold _root_.derivWithin deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
have rw : Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: rw [h.fderivWithin hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ derivWithin f univ = deriv f
have h : ∀ (x : 𝕜), derivWithin f univ x = deriv f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ derivWithin f univ x = deriv f x
have h : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f univ x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: unfold derivWithin deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f univ x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
have h : Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: rw [fderivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
ht : t ∈ 𝓝 x
⊢ derivWithin f (s ∩ t) x = derivWithin f s x
have unfold : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f (s ∩ t) x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: unfold derivWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
ht : t ∈ 𝓝 x
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f (s ∩ t) x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
have rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: rw [fderivWithin_inter ht]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
f' : 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
x : 𝕜
hx : x ∈ s
⊢ deriv f x = f' x
have rw : derivWithin f s x = f' x
Tactic: rw [← derivWithin_of_isOpen hs hx, (hf' _ hx).derivWithin <| hs.uniqueDiffWithinAt hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
f' : 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
x : 𝕜
hx : x ∈ s
rw : derivWithin f s x = f' x
⊢ deriv f x = f' x
have rw₁ : f' x = f' x
Tactic: rw [← derivWithin_of_isOpen hs hx, (hf' _ hx).derivWithin <| hs.uniqueDiffWithinAt hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
have pos : ∀ (hx : DifferentiableAt 𝕜 f x),
  deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
Tactic: by_cases hx : DifferentiableAt 𝕜 f x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
pos :
  ∀ (hx : DifferentiableAt 𝕜 f x),
    deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
have neg : ∀ (hx : ¬DifferentiableAt 𝕜 f x),
  deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
Tactic: by_cases hx : DifferentiableAt 𝕜 f x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
have pos : ∀ (hx : DifferentiableWithinAt 𝕜 f t x),
  derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
Tactic: by_cases hx : DifferentiableWithinAt 𝕜 f t x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
pos :
  ∀ (hx : DifferentiableWithinAt 𝕜 f t x),
    derivWithin f t x ∈ s ↔
      DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
have neg : ∀ (hx : ¬DifferentiableWithinAt 𝕜 f t x),
  derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
Tactic: by_cases hx : DifferentiableWithinAt 𝕜 f t x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
have pos : ∀ (H : DifferentiableWithinAt ℝ f (Ioi x) x), derivWithin f (Ioi x) x = derivWithin f (Ici x) x
Tactic: by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
pos : ∀ (H : DifferentiableWithinAt ℝ f (Ioi x) x), derivWithin f (Ioi x) x = derivWithin f (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
have neg : ∀ (H : ¬DifferentiableWithinAt ℝ f (Ioi x) x), derivWithin f (Ioi x) x = derivWithin f (Ici x) x
Tactic: by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
have A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
Tactic: have A := H.hasDerivWithinAt.Ici_of_Ioi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
have B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
Tactic: have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
have neg : ¬DifferentiableWithinAt ℝ f (Ici x) x
Tactic: rw [derivWithin_zero_of_not_differentiableWithinAt H,
      derivWithin_zero_of_not_differentiableWithinAt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x
have neg : ∀ (H : ¬DifferentiableWithinAt ℝ f (Ici x) x), ¬DifferentiableWithinAt ℝ f (Ici x) x
Tactic: rwa [differentiableWithinAt_Ioi_iff_Ici] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x
have unfold : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f₁ s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: unfold derivWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f₁ s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
have rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: rw [hs.fderivWithin_eq hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x
have unfold : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f₁ s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: unfold derivWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f₁ s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
have rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: rw [fderivWithin_congr hs hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f g : 𝕜 → F
s : Set 𝕜
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
⊢ _root_.deriv f x = _root_.deriv g x
have rw : derivWithin f s x = derivWithin g s x
Tactic: rw [← derivWithin_of_isOpen hs hx, ← derivWithin_of_isOpen hs hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ deriv f₁ x = deriv f x
have unfold : Eq.{v + 1} (α := F) (((fderiv 𝕜 f₁ x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: unfold deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
hL : f₁ =ᶠ[𝓝 x] f
⊢ Eq.{v + 1} (α := F) (((fderiv 𝕜 f₁ x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
have rwa : Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
  (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
Tactic: rwa [Filter.EventuallyEq.fderiv_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s t : Set 𝕜
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ derivWithin f₁ t =ᶠ[𝓝[s] x] derivWithin f t
have unfold : EventuallyEq.{u, v} (β := F) (𝓝[s] x) (fun (x : 𝕜) ↦ ((fderivWithin 𝕜 f₁ t x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1)
  fun (x : 𝕜) ↦ ((fderivWithin 𝕜 f t x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1
Tactic: unfold derivWithin
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
h : f₁ =ᶠ[𝓝[≠] x] f
⊢ deriv f₁ =ᶠ[𝓝[≠] x] deriv f
have rw : ∀ (h : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x),
  ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x
Tactic: rw [Filter.EventuallyEq, ← eventually_nhdsNE_eventually_nhds_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
h : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x
have h₁ : ∀ (y : 𝕜) (hy : ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x), ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x
Tactic: filter_upwards [h] with y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
c : F
⊢ Eq (α := (x : 𝕜) → F) (derivWithin (fun (x : 𝕜) ↦ c) s) 0
have h : ∀ (x : 𝕜), Eq.{v + 1} (α := F) (derivWithin (fun (x : 𝕜) ↦ c) s x) (0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
⊢ HasDerivAt.{u, u_1} (𝕜 := 𝕜) (F := F') ((⇑L : (a : F) → F') ∘ f ∘ (⇑σ' : (a : 𝕜) → 𝕜) : 𝕜 → F')
    ((L : (a : F) → F') f' : F') ((σ : (a : 𝕜) → 𝕜) x : 𝕜)
have this : RingHomIsometric σ'
Tactic: have : RingHomIsometric σ' := .inv σ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
⊢ HasDerivAt.{u, u_1} (𝕜 := 𝕜) (F := F') ((⇑L : (a : F) → F') ∘ f ∘ (⇑σ' : (a : 𝕜) → 𝕜) : 𝕜 → F')
    ((L : (a : F) → F') f' : F') ((σ : (a : 𝕜) → 𝕜) x : 𝕜)
have hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
Tactic: have hR (k : 𝕜) : R k = σ' k := rfl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
⊢ HasFDerivAt.{u, u, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := F') ((⇑L : (a : F) → F') ∘ f ∘ (⇑σ' : (a : 𝕜) → 𝕜) : 𝕜 → F')
    (toSpanSingleton 𝕜 ((L : (a : F) → F') f') : 𝕜 →L[𝕜] F') ((σ : (a : 𝕜) → 𝕜) x : 𝕜)
have h : Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜) →
    toSpanSingleton 𝕜 ((L : (a : F) → F') f') = L ∘SL toSpanSingleton 𝕜 f' ∘SL R
Tactic: convert! HasFDerivAt.comp_semilinear L R (f' := toSpanSingleton 𝕜 f') ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
h :
  Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜) →
      toSpanSingleton 𝕜 ((L : (a : F) → F') f') = L ∘SL toSpanSingleton 𝕜 f' ∘SL R
⊢ HasFDerivAt.{u, u, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := F') ((⇑L : (a : F) → F') ∘ f ∘ (⇑σ' : (a : 𝕜) → 𝕜) : 𝕜 → F')
    (toSpanSingleton 𝕜 ((L : (a : F) → F') f') : 𝕜 →L[𝕜] F') ((σ : (a : 𝕜) → 𝕜) x : 𝕜)
have convert_3 : HasFDerivAt (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') ((R : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))
Tactic: convert! HasFDerivAt.comp_semilinear L R (f' := toSpanSingleton 𝕜 f') ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
e_4 : Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜)
⊢ toSpanSingleton 𝕜 ((L : (a : F) → F') f') = L ∘SL toSpanSingleton 𝕜 f' ∘SL R
have h : Eq.{u_1 + 1} (α := F') (((toSpanSingleton 𝕜 ((L : (a : F) → F') f') : 𝕜 →L[𝕜] F') : (a : 𝕜) → F') 1 : F')
  ((L ∘SL toSpanSingleton 𝕜 f' ∘SL R : (a : 𝕜) → F') 1 : F')
Tactic: ext