awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
h : HasFDerivAt f f' x
rw rw₁ : Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) (fderiv 𝕜 f x)
⊢ fderiv 𝕜 f x = f'

Tactic:
rw [h.unique h.differentiableAt.hasFDerivAt]

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.unique
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
f' : E → E →L[𝕜] F
h : ∀ (x : E), HasFDerivAt f (f' x) x
⊢ fderiv 𝕜 f = f'

Tactic:
funext fun x => (h x).fderiv

Premises used: funext, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
h : HasFDerivWithinAt f f' s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 f s x = f'

Tactic:
(hxs.eq h h.differentiableWithinAt.hasFDerivWithinAt).symm

Premises used: HasFDerivWithinAt.differentiableWithinAt, Eq.symm, DifferentiableWithinAt.hasFDerivWithinAt, UniqueDiffWithinAt.eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
h : DifferentiableWithinAt 𝕜 f t x
st : s ⊆ t
rcases : ∀ (f' : E →L[𝕜] F) (hf' : HasFDerivWithinAt f f' t x), DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rcases h with ⟨f', hf'⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
st : s ⊆ t
f' : E →L[𝕜] F
hf' : HasFDerivWithinAt f f' t x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
⟨f', hf'.mono st⟩

Premises used: Exists.intro, DifferentiableWithinAt, HasFDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
st : s ⊆ t
f' : E →L[𝕜] F
hf' : HasFDerivWithinAt f f' t x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact ⟨f', hf'.mono st⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
t : Set E
hst : s ∈ 𝓝[t] x
⊢ DifferentiableWithinAt 𝕜 f t x

Tactic:
(h.hasFDerivWithinAt.mono_of_mem_nhdsWithin hst).differentiableWithinAt

Premises used: HasFDerivWithinAt.mono_of_mem_nhdsWithin, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
t : Set E
hst : 𝓝[s] x = 𝓝[t] x
⊢ DifferentiableWithinAt 𝕜 f t x

Tactic:
h.mono_of_mem_nhdsWithin <| hst ▸ self_mem_nhdsWithin

Premises used: Eq.rec, self_mem_nhdsWithin, DifferentiableWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
hst : 𝓝[s] x = 𝓝[t] x
⊢ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x

Tactic:
⟨fun h => h.congr_nhds hst, fun h => h.congr_nhds hst.symm⟩

Premises used: DifferentiableWithinAt.congr_nhds, Iff.intro, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
ht : t ∈ 𝓝 x
⊢ DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter ht]

Premises used: DifferentiableWithinAt, hasFDerivWithinAt_inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
ht : t ∈ 𝓝[s] x
⊢ DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter' ht]

Premises used: hasFDerivWithinAt_inter', DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
⟨fun h ↦ h.mono (subset_insert x s), fun h ↦ h.hasFDerivWithinAt.insert.differentiableWithinAt⟩

Premises used: HasFDerivWithinAt.insert, DifferentiableWithinAt.mono, HasFDerivWithinAt.differentiableWithinAt, Iff.intro, Set.subset_insert, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
y : E
h : DifferentiableWithinAt 𝕜 f (insert y s) x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
h.mono <| subset_insert _ _

Premises used: DifferentiableWithinAt.mono, Set.subset_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
inst_7 : T1Space E
y : E
⊢ DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_insert]

Premises used: DifferentiableWithinAt, hasFDerivWithinAt_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
h : DifferentiableAt 𝕜 f x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
(differentiableWithinAt_univ.2 h).mono (subset_univ _)

Premises used: Iff.mpr, Set.subset_univ, DifferentiableWithinAt.mono, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
h : Differentiable 𝕜 f
⊢ DifferentiableAt 𝕜 f x

Tactic:
h x
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderiv 𝕜 f x)

Tactic:
h.hasFDerivAt.hasFDerivWithinAt.fderivWithin hxs

Premises used: HasFDerivAt.hasFDerivWithinAt, HasFDerivWithinAt.fderivWithin, DifferentiableAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s t : Set E
h : DifferentiableOn 𝕜 f t
st : s ⊆ t
⊢ DifferentiableOn 𝕜 f s

Tactic:
fun x hx => (h x (st hx)).mono st

Premises used: DifferentiableWithinAt.mono, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
⊢ DifferentiableOn 𝕜 f univ ↔ Differentiable 𝕜 f

Tactic:
simp only [DifferentiableOn, Differentiable, differentiableWithinAt_univ, mem_univ,
    forall_true_left]

Premises used: Differentiable, forall_true_left, DifferentiableOn, Set.mem_univ, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s : Set E
h : Differentiable 𝕜 f
⊢ DifferentiableOn 𝕜 f s

Tactic:
(differentiableOn_univ.2 h).mono (subset_univ _)

Premises used: Iff.mpr, Set.subset_univ, differentiableOn_univ, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ (u : Set E), IsOpen[inst_3] u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
rcases :
  ∀ (t : Set E) (t_open : IsOpen[inst_3] t) (xt : x ∈ t) (ht : DifferentiableOn 𝕜 f (s ∩ t)),
    DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rcases h x xs with ⟨t, t_open, xt, ht⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ (u : Set E), IsOpen[inst_3] u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
t : Set E
t_open : IsOpen[inst_3] t
xt : x ∈ t
ht : DifferentiableOn 𝕜 f (s ∩ t)
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
(differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 (ht x ⟨xs, xt⟩)

Premises used: differentiableWithinAt_inter, And.intro, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ (u : Set E), IsOpen[inst_3] u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
t : Set E
t_open : IsOpen[inst_3] t
xt : x ∈ t
ht : DifferentiableOn 𝕜 f (s ∩ t)
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact (differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 (ht x ⟨xs, xt⟩)

Premises used: differentiableWithinAt_inter, And.intro, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
st : t ∈ 𝓝[s] x
ht : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f t x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
((DifferentiableWithinAt.hasFDerivWithinAt h).mono_of_mem_nhdsWithin st).fderivWithin ht

Premises used: HasFDerivWithinAt.mono_of_mem_nhdsWithin, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
st : s ⊆ t
ht : UniqueDiffWithinAt 𝕜 s x
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
h : DifferentiableWithinAt 𝕜 f t x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f t x)

Tactic:
fderivWithin_of_mem_nhdsWithin (nhdsWithin_mono _ st self_mem_nhdsWithin) ht h

Premises used: fderivWithin_of_mem_nhdsWithin, self_mem_nhdsWithin, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
ht : t ∈ 𝓝 x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (s ∩ t) x) (fderivWithin 𝕜 f s x)

Tactic:
simp [fderivWithin, hasFDerivWithinAt_inter ht, DifferentiableWithinAt]

Premises used: fderivWithin, DifferentiableWithinAt, hasFDerivWithinAt_inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s t : Set E
ht : t ∈ 𝓝 x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (s ∩ t) x) (fderivWithin 𝕜 f s x)

Tactic:
classical
  simp [fderivWithin, hasFDerivWithinAt_inter ht, DifferentiableWithinAt]

Premises used: fderivWithin, DifferentiableWithinAt, hasFDerivWithinAt_inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
h : s ∈ 𝓝 x
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f univ x)
rw₁ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f (univ ∩ s) x) (fderivWithin 𝕜 f univ x)
rw₂ rw₃ : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f univ x) (fderivWithin 𝕜 f univ x)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderiv 𝕜 f x)

Tactic:
rw [← fderivWithin_univ, ← univ_inter s, fderivWithin_inter h]

Premises used: fderivWithin_univ, Set.univ_inter, fderivWithin_inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
hs : IsOpen[inst_3] s
hx : x ∈ s
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderiv 𝕜 f x)

Tactic:
fderivWithin_of_mem_nhds (hs.mem_nhds hx)

Premises used: fderivWithin_of_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableAt 𝕜 f x
rw : Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f univ x)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderiv 𝕜 f x)

Tactic:
rw [← fderivWithin_univ]

Premises used: fderivWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableAt 𝕜 f x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f univ x)

Tactic:
fderivWithin_subset (subset_univ _) hs h.differentiableWithinAt

Premises used: Set.subset_univ, DifferentiableAt.differentiableWithinAt, fderivWithin_subset
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
inst_11 : T2Space F
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableAt 𝕜 f x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 f univ x)

Tactic:
exact fderivWithin_subset (subset_univ _) hs h.differentiableWithinAt

Premises used: Set.subset_univ, DifferentiableAt.differentiableWithinAt, fderivWithin_subset
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s : Set (E →L[𝕜] F)
x : E
pos :
  ∀ (hx : DifferentiableAt 𝕜 f x),
    fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
neg :
  ∀ (hx : ¬DifferentiableAt 𝕜 f x),
    fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
by_cases hx : DifferentiableAt 𝕜 f x

Premises used: DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s : Set (E →L[𝕜] F)
x : E
hx : DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
simp [fderiv_zero_of_not_differentiableAt, *]

Premises used: fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s : Set (E →L[𝕜] F)
x : E
hx : ¬DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
simp [fderiv_zero_of_not_differentiableAt, *]

Premises used: fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
t : Set E
s : Set (E →L[𝕜] F)
x : E
pos :
  ∀ (hx : DifferentiableWithinAt 𝕜 f t x),
    fderivWithin 𝕜 f t x ∈ s ↔
      DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
neg :
  ∀ (hx : ¬DifferentiableWithinAt 𝕜 f t x),
    fderivWithin 𝕜 f t x ∈ s ↔
      DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
⊢ fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 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.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
t : Set E
s : Set (E →L[𝕜] F)
x : E
hx : DifferentiableWithinAt 𝕜 f t x
⊢ fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

Tactic:
simp [fderivWithin_zero_of_not_differentiableWithinAt, *]

Premises used: fderivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
t : Set E
s : Set (E →L[𝕜] F)
x : E
hx : ¬DifferentiableWithinAt 𝕜 f t x
⊢ fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

Tactic:
simp [fderivWithin_zero_of_not_differentiableWithinAt, *]

Premises used: fderivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
x : E
hx : x ∈ s ∪ t
inl : ∀ (hx : x ∈ s), DifferentiableWithinAt 𝕜 f (s ∪ t) x
inr : ∀ (hx : x ∈ t), DifferentiableWithinAt 𝕜 f (s ∪ t) x
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x

Tactic:
obtain (hx | hx) := hx
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
x : E
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x

Tactic:
(hf x hx).differentiableAt (hs.mem_nhds hx) |>.differentiableWithinAt

Premises used: DifferentiableWithinAt.differentiableAt, DifferentiableAt.differentiableWithinAt, IsOpen.mem_nhds