awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hd : HasDerivWithinAt f 0 s x
H : UniqueDiffWithinAt 𝕜 s x
⊢ deriv f x = 0

Tactic:
(em' (DifferentiableAt 𝕜 f x)).elim deriv_zero_of_not_differentiableAt fun h =>
    H.eq_deriv _ h.hasDerivAt.hasDerivWithinAt hd

Premises used: HasDerivAt.hasDerivWithinAt, DifferentiableAt.hasDerivAt, deriv_zero_of_not_differentiableAt, DifferentiableAt, UniqueDiffWithinAt.eq_deriv, Or.elim, em'
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
st : t ∈ 𝓝[s] x
ht : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f s x = derivWithin f t x

Tactic:
((DifferentiableWithinAt.hasDerivWithinAt h).mono_of_mem_nhdsWithin st).derivWithin ht

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
st : s ⊆ t
ht : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f s x = derivWithin f t x

Tactic:
((DifferentiableWithinAt.hasDerivWithinAt h).mono st).derivWithin ht

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
y : 𝕜
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ derivWithin f s x = derivWithin f t x

Tactic:
simp only [derivWithin, fderivWithin_congr_set' y h]

Premises used: fderivWithin_congr_set', derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
h : s =ᶠ[𝓝 x] t
⊢ derivWithin f s x = derivWithin f t x

Tactic:
simp only [derivWithin, fderivWithin_congr_set h]

Premises used: derivWithin, fderivWithin_congr_set
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
h : ∀ (x : 𝕜), derivWithin f univ x = deriv f x
⊢ derivWithin f univ = deriv f

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h :
  Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f univ x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
⊢ derivWithin f univ x = deriv f x

Tactic:
unfold derivWithin deriv

Premises used: deriv, derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h h₁ :
  Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f univ x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)

Tactic:
rw [fderivWithin_univ]

Premises used: fderivWithin_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
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)
⊢ derivWithin f (s ∩ t) x = derivWithin f s x

Tactic:
unfold derivWithin

Premises used: derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
rw 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)
⊢ 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:
rw [fderivWithin_inter ht]

Premises used: fderivWithin_inter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 x
⊢ derivWithin f s x = deriv f x

Tactic:
simp only [derivWithin, deriv, fderivWithin_of_mem_nhds h]

Premises used: deriv, fderivWithin_of_mem_nhds, derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hx : x ∈ s
⊢ derivWithin f s x = deriv f x

Tactic:
derivWithin_of_mem_nhds (hs.mem_nhds hx)

Premises used: IsOpen.mem_nhds, derivWithin_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
rw₁ rw₂ : f' x = f' x
⊢ deriv f x = f' x

Tactic:
rw [← derivWithin_of_isOpen hs hx, (hf' _ hx).derivWithin <| hs.uniqueDiffWithinAt hx]

Premises used: IsOpen.uniqueDiffWithinAt, HasDerivWithinAt.derivWithin, derivWithin_of_isOpen
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
neg :
  ∀ (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

Tactic:
by_cases hx : DifferentiableAt 𝕜 f x

Premises used: DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
hx : DifferentiableAt 𝕜 f x
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
simp [deriv_zero_of_not_differentiableAt, *]

Premises used: deriv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
hx : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
simp [deriv_zero_of_not_differentiableAt, *]

Premises used: deriv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
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
⊢ 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

Premises used: DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
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:
simp [derivWithin_zero_of_not_differentiableWithinAt, *]

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
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:
simp [derivWithin_zero_of_not_differentiableWithinAt, *]

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst_3 : PartialOrder 𝕜
⊢ DifferentiableWithinAt 𝕜 f (Ioi x) x ↔ DifferentiableWithinAt 𝕜 f (Ici x) x

Tactic:
⟨fun h => h.hasDerivWithinAt.Ici_of_Ioi.differentiableWithinAt, fun h =>
    h.hasDerivWithinAt.Ioi_of_Ici.differentiableWithinAt⟩

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.Ici_of_Ioi, HasDerivWithinAt.differentiableWithinAt, Iff.intro, HasDerivWithinAt.Ioi_of_Ici
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
neg : ∀ (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

Tactic:
by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x

Premises used: Real, Set.Ioi, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x

Tactic:
have A := H.hasDerivWithinAt.Ici_of_Ioi
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
⊢ HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x

Tactic:
have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
simpa using (uniqueDiffOn_Ici x).eq self_mem_Ici A B

Premises used: UniqueDiffOn.eq, uniqueDiffOn_Ici, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
neg : ¬DifferentiableWithinAt ℝ f (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
rw [derivWithin_zero_of_not_differentiableWithinAt H,
      derivWithin_zero_of_not_differentiableWithinAt]

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
neg neg₁ neg₂ neg₃ : ∀ (H : ¬DifferentiableWithinAt ℝ f (Ici x) x), ¬DifferentiableWithinAt ℝ f (Ici x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x

Tactic:
rwa [differentiableWithinAt_Ioi_iff_Ici] at H

Premises used: differentiableWithinAt_Ioi_iff_Ici
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f₀ f₁ : 𝕜 → F
f₀' f₁' : F
L : Filter (𝕜 × 𝕜)
h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁
h₁ : f₀' = f₁'
⊢ ∀ (x : 𝕜),
    Eq.{v + 1} (α := F) ((toSpanSingleton 𝕜 f₀' : (a : 𝕜) → F) x : F) ((toSpanSingleton 𝕜 f₁' : (a : 𝕜) → F) x : F)

Tactic:
simp [h₁]
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
hL : Prod.map f₁ f₁ =ᶠ[L] Prod.map f f
rwa rwa₁ rwa₂ rwa₃ : HasDerivAtFilter f f' L
⊢ HasDerivAtFilter f₁ f' L

Tactic:
rwa [hL.hasDerivAtFilter_iff rfl]

Premises used: rfl, Filter.EventuallyEq.hasDerivAtFilter_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
s t : Set 𝕜
h : HasDerivWithinAt f f' s x
ht : ∀ x ∈ t, f₁ x = f x
hx : f₁ x = f x
h₁ : t ⊆ s
⊢ HasDerivWithinAt f₁ f' t x

Tactic:
HasFDerivWithinAt.congr_mono h ht hx h₁

Premises used: HasDerivWithinAt, HasDerivAtFilter, HasFDerivWithinAt.congr_mono
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
hs : ∀ x ∈ s, f₁ x = f x
hx : f₁ x = f x
⊢ HasDerivWithinAt f₁ f' s x

Tactic:
h.congr_mono hs hx (Subset.refl _)

Premises used: HasDerivWithinAt.congr_mono, Set.Subset.refl
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
hs : ∀ x ∈ s, f₁ x = f x
hx : x ∈ s
⊢ HasDerivWithinAt f₁ f' s x

Tactic:
h.congr hs (hs _ hx)

Premises used: HasDerivWithinAt.congr
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ HasDerivWithinAt f₁ f' s x

Tactic:
HasDerivAtFilter.congr_of_eventuallyEq h <| h₁.prodMap hx

Premises used: HasDerivWithinAt, HasDerivAtFilter.congr_of_eventuallyEq, Filter.EventuallyEq.prodMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x

Tactic:
⟨fun h' ↦ h'.congr_of_eventuallyEq h₁.symm hx.symm, fun h' ↦ h'.congr_of_eventuallyEq h₁ hx⟩

Premises used: Iff.intro, HasDerivWithinAt.congr_of_eventuallyEq, Eq.symm, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ HasDerivWithinAt f₁ f' s x

Tactic:
h.congr_of_eventuallyEq h₁ (h₁.eq_of_nhdsWithin hx)

Premises used: Filter.EventuallyEq.eq_of_nhdsWithin, HasDerivWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x

Tactic:
⟨fun h' ↦ h'.congr_of_eventuallyEq_of_mem h₁.symm hx,
  fun h' ↦ h'.congr_of_eventuallyEq_of_mem h₁ hx⟩

Premises used: HasDerivWithinAt.congr_of_eventuallyEq_of_mem, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
h : HasStrictDerivAt f f' x
h₁ : f =ᶠ[𝓝 x] f₁
⊢ HasStrictDerivAt f₁ f' x

Tactic:
HasDerivAtFilter.congr_of_eventuallyEq h (h₁.symm.prodMap_nhds h₁.symm)

Premises used: HasDerivAtFilter.congr_of_eventuallyEq, Filter.EventuallyEq.prodMap_nhds, HasStrictDerivAt, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' g' : F
x : 𝕜
h : HasStrictDerivAt f f' x
h' : f' = g'
⊢ HasStrictDerivAt f g' x

Tactic:
h.hasStrictFDerivAt.congr_fderiv <| congr_arg _ h'

Premises used: HasStrictDerivAt.hasStrictFDerivAt, congr_arg, HasDerivAtFilter, HasStrictFDerivAt.congr_fderiv, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' g' : F
x : 𝕜
h : HasDerivAt f f' x
h' : f' = g'
⊢ HasDerivAt f g' x

Tactic:
HasFDerivAt.congr_fderiv h <| congr_arg _ h'

Premises used: HasFDerivAt.congr_fderiv, HasDerivAt, congr_arg, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' g' : F
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
h' : f' = g'
⊢ HasDerivWithinAt f g' s x

Tactic:
HasFDerivWithinAt.congr_fderiv h <| congr_arg _ h'

Premises used: HasFDerivWithinAt.congr_fderiv, HasDerivWithinAt, congr_arg, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
h : HasDerivAt f f' x
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ HasDerivAt f₁ f' x

Tactic:
HasDerivAtFilter.congr_of_eventuallyEq h <| h₁.prodMap <| h₁.filter_mono <| pure_le_nhds _

Premises used: Filter.EventuallyEq.filter_mono, pure_le_nhds, HasDerivAt, HasDerivAtFilter.congr_of_eventuallyEq, Filter.EventuallyEq.prodMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f₀ f₁ : 𝕜 → F
f' : F
x : 𝕜
h : f₀ =ᶠ[𝓝 x] f₁
⊢ HasDerivAt f₀ f' x ↔ HasDerivAt f₁ f' x

Tactic:
⟨fun h' ↦ h'.congr_of_eventuallyEq h.symm, fun h' ↦ h'.congr_of_eventuallyEq h⟩

Premises used: HasDerivAt.congr_of_eventuallyEq, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
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)
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
unfold derivWithin

Premises used: derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
rw 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)
⊢ 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]

Premises used: Filter.EventuallyEq.fderivWithin_eq
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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 : x ∈ s
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
hs.derivWithin_eq <| hs.self_of_nhdsWithin hx

Premises used: Filter.Eventually.self_of_nhdsWithin, Filter.EventuallyEq.derivWithin_eq
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝 x] f
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
(hs.filter_mono nhdsWithin_le_nhds).derivWithin_eq hs.self_of_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.Eventually.self_of_nhds, Filter.EventuallyEq.derivWithin_eq, nhdsWithin_le_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
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)
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
unfold derivWithin

Premises used: derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
rw 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)
⊢ 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]

Premises used: fderivWithin_congr
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
rw : derivWithin f s x = derivWithin g s x
⊢ _root_.deriv f x = _root_.deriv g x

Tactic:
rw [← derivWithin_of_isOpen hs hx, ← derivWithin_of_isOpen hs hx]

Premises used: derivWithin_of_isOpen
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
⊢ derivWithin f s x = derivWithin g s x

Tactic:
derivWithin_congr hfg (hfg hx)

Premises used: derivWithin_congr
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
⊢ derivWithin f s x = derivWithin g s x

Tactic:
exact derivWithin_congr hfg (hfg hx)

Premises used: derivWithin_congr
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
hL : f₁ =ᶠ[𝓝 x] f
unfold :
  Eq.{v + 1} (α := F) (((fderiv 𝕜 f₁ x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
⊢ deriv f₁ x = deriv f x

Tactic:
unfold deriv

Premises used: deriv