awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g h : 𝕜 → 𝕜
f' h' a : 𝕜
hst : ContinuousAt g a
hf : HasDerivAt f f' (g a)
hh : HasDerivAt h h' a
hf' : f' ≠ 0
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ h' / f' = (ContinuousLinearMap.toSpanSingleton 𝕜 f'⁻¹ ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 h' : (a : 𝕜) → 𝕜) 1

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
f' a : 𝕜
hg : ContinuousAt g a
hf : HasDerivAt f f' (g a)
hf' : f' ≠ 0
hfg : ∀ᶠ (y : 𝕜) in 𝓝 a, f (g y) = y
⊢ HasDerivAt g f'⁻¹ a

Tactic:
(hf.hasFDerivAt_equiv hf').of_local_left_inverse hg hfg

Premises used: Set.Mem, HasDerivAt, setOf, HasFDerivAt.of_local_left_inverse, HasDerivAtFilter, HasDerivAt.hasFDerivAt_equiv, ContinuousLinearMap.toSpanSingleton, LinearMap.smulRight, LinearMap.toSpanSingleton, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f : OpenPartialHomeomorph 𝕜 𝕜
a f' : 𝕜
ha : a ∈ f.target
hf' : f' ≠ 0
htff' : HasDerivAt (↑f : 𝕜 → 𝕜) f' ((↑f.symm : 𝕜 → 𝕜) a)
⊢ HasDerivAt (↑f.symm : 𝕜 → 𝕜) f'⁻¹ a

Tactic:
htff'.of_local_left_inverse (f.symm.continuousAt ha) hf' (f.eventually_right_inverse ha)

Premises used: OpenPartialHomeomorph.continuousAt, OpenPartialHomeomorph.eventually_right_inverse, HasDerivAt.of_local_left_inverse, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
simp : ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
⊢ dist x_1 x_2 ≤
    (↑‖f'‖₊⁻¹ : ℝ) *
      dist.{v} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_1 : F)
        ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_2 : F)

Tactic:
simp [dist_eq_norm_sub, ← sub_smul, norm_smul]

Premises used: norm_smul, dist_eq_norm_sub, sub_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
field_simp : ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖
⊢ ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
⊢ ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
c : F
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
simp : ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
⊢ dist x_1 x_2 ≤
    (↑‖f'‖₊⁻¹ : ℝ) *
      dist.{v} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_1 : F)
        ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_2 : F)

Tactic:
simp [dist_eq_norm_sub, ← sub_smul, norm_smul]

Premises used: norm_smul, dist_eq_norm_sub, sub_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
c : F
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
field_simp : ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖
⊢ ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
c : F
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
⊢ ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
x_1 x_2 : 𝕜
simp : ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
⊢ dist x_1 x_2 ≤
    (↑‖f'‖₊⁻¹ : ℝ) *
      dist.{v} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_1 : F)
        ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_2 : F)

Tactic:
simp [dist_eq_norm_sub, ← sub_smul, norm_smul]

Premises used: norm_smul, dist_eq_norm_sub, sub_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
x_1 x_2 : 𝕜
field_simp : ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖
⊢ ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
x_1 x_2 : 𝕜
⊢ ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
h : HasDerivAt f f' x
hf' : f' ≠ 0
⊢ Tendsto f (𝓝[≠] x) (𝓝[≠] f x)

Tactic:
simpa only [compl_eq_univ_diff] using (hasDerivWithinAt_univ.2 h).tendsto_nhdsWithin_nhdsNE hf'

Premises used: Iff.mpr, hasDerivWithinAt_univ, HasDerivWithinAt.tendsto_nhdsWithin_nhdsNE, Set.compl_eq_univ_diff
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
c : F
h : HasDerivAt f f' x
hf' : f' ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ≠ c

Tactic:
simpa only [compl_eq_univ_diff] using (hasDerivWithinAt_univ.2 h).eventually_ne hf'

Premises used: Iff.mpr, HasDerivWithinAt.eventually_ne, hasDerivWithinAt_univ, Set.compl_eq_univ_diff
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
h : HasDerivAt f f' x
hf' : f' ≠ 0
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z ∉ t

Tactic:
simpa only [compl_eq_univ_diff] using (hasDerivWithinAt_univ.2 h).eventually_notMem hf' t ht

Premises used: Iff.mpr, HasDerivWithinAt.eventually_notMem, hasDerivWithinAt_univ, Set.compl_eq_univ_diff
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
pos : ∀ (hf : DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
neg : ∀ (hf : ¬DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
⊢ derivWithin f s x = 0

Tactic:
by_cases hf : DifferentiableWithinAt 𝕜 f s x

Premises used: DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
hf : DifferentiableWithinAt 𝕜 f s x
pos : ∀ (h : derivWithin f s x ≠ 0), ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ≠ c
⊢ derivWithin f s x = 0

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
hf : DifferentiableWithinAt 𝕜 f s x
h : derivWithin f s x ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ≠ c

Tactic:
hf.hasDerivWithinAt.eventually_ne h

Premises used: HasDerivWithinAt.eventually_ne, DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
hf : DifferentiableWithinAt 𝕜 f s x
h : derivWithin f s x ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ≠ c

Tactic:
exact hf.hasDerivWithinAt.eventually_ne h

Premises used: HasDerivWithinAt.eventually_ne, DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

Tactic:
derivWithin_zero_of_not_differentiableWithinAt hf

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y = c
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

Tactic:
exact derivWithin_zero_of_not_differentiableWithinAt hf

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
pos : ∀ (hf : DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
neg : ∀ (hf : ¬DifferentiableWithinAt 𝕜 f s x), derivWithin f s x = 0
⊢ derivWithin f s x = 0

Tactic:
by_cases hf : DifferentiableWithinAt 𝕜 f s x

Premises used: DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : DifferentiableWithinAt 𝕜 f s x
pos : ∀ (h : derivWithin f s x ≠ 0), ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ∉ t
⊢ derivWithin f s x = 0

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
hf : DifferentiableWithinAt 𝕜 f s x
h : derivWithin f s x ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ∉ t

Tactic:
hf.hasDerivWithinAt.eventually_notMem h t ht

Premises used: HasDerivWithinAt.eventually_notMem, DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
hf : DifferentiableWithinAt 𝕜 f s x
h : derivWithin f s x ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ∉ t

Tactic:
exact hf.hasDerivWithinAt.eventually_notMem h t ht

Premises used: HasDerivWithinAt.eventually_notMem, DifferentiableWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

Tactic:
derivWithin_zero_of_not_differentiableWithinAt hf

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

Tactic:
exact derivWithin_zero_of_not_differentiableWithinAt hf

Premises used: derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
h : ∃ᶠ (y : 𝕜) in 𝓝[≠] x, f y = c
rw : ∃ᶠ (y : 𝕜) in 𝓝[univ \ {x}] x, f y = c
rw₁ : F
⊢ deriv f x = 0

Tactic:
rw [← derivWithin_univ, derivWithin_zero_of_frequently_const]

Premises used: derivWithin_zero_of_frequently_const, derivWithin_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
h rwa rwa₁ rwa₂ rwa₃ : ∃ᶠ (y : 𝕜) in 𝓝[≠] x, f y = c
⊢ ∃ᶠ (y : 𝕜) in 𝓝[univ \ {x}] x, f y = c

Tactic:
rwa [← compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[≠] x, f y ∈ t
rw : ∃ᶠ (y : 𝕜) in 𝓝[univ \ {x}] x, f y ∈ t
⊢ deriv f x = 0

Tactic:
rw [← derivWithin_univ, derivWithin_zero_of_frequently_mem t ht]

Premises used: derivWithin_zero_of_frequently_mem, derivWithin_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h rwa rwa₁ rwa₂ rwa₃ : ∃ᶠ (y : 𝕜) in 𝓝[≠] x, f y ∈ t
⊢ ∃ᶠ (y : 𝕜) in 𝓝[univ \ {x}] x, f y ∈ t

Tactic:
rwa [← compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
⊢ HasDerivWithinAt id (0 * derivWithin g s a) s a

Tactic:
have := (hf.comp a hg.hasDerivWithinAt hst).congr_of_eventuallyEq_of_mem hfg.symm ha
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
this : HasDerivWithinAt id (0 * derivWithin g s a) s a
⊢ False

Tactic:
simpa using hsu.eq_deriv _ this (hasDerivWithinAt_id _ _)

Premises used: UniqueDiffWithinAt.eq_deriv, hasDerivWithinAt_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
hf : HasDerivAt f 0 (g a)
hfg : f ∘ g =ᶠ[𝓝 a] id
hg : DifferentiableAt 𝕜 g a
⊢ HasDerivAt id (0 * deriv g a) a

Tactic:
have := (hf.comp a hg.hasDerivAt).congr_of_eventuallyEq hfg.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
hf : HasDerivAt f 0 (g a)
hfg : f ∘ g =ᶠ[𝓝 a] id
hg : DifferentiableAt 𝕜 g a
this : HasDerivAt id (0 * deriv g a) a
⊢ False

Tactic:
simpa using this.unique (hasDerivAt_id a)

Premises used: HasDerivAt.unique, hasDerivAt_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
e : 𝕜 →L[𝕜] F
⊢ HasDerivAtFilter.{u, v} (F := F) ((⇑e : (a : 𝕜) → F) : (a : 𝕜) → F) ((e : (a : 𝕜) → F) 1 : F) L

Tactic:
e.hasFDerivAtFilter.hasDerivAtFilter

Premises used: ContinuousLinearMap.hasFDerivAtFilter, HasFDerivAtFilter.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
e : 𝕜 →L[𝕜] F
⊢ HasStrictDerivAt.{u, v} (F := F) ((⇑e : (a : 𝕜) → F) : (a : 𝕜) → F) ((e : (a : 𝕜) → F) 1 : F) x

Tactic:
e.hasDerivAtFilter

Premises used: ContinuousLinearMap.hasDerivAtFilter, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
e : 𝕜 →L[𝕜] F
⊢ HasDerivAt.{u, v} (F := F) ((⇑e : (a : 𝕜) → F) : (a : 𝕜) → F) ((e : (a : 𝕜) → F) 1 : F) x

Tactic:
e.hasDerivAtFilter

Premises used: ContinuousLinearMap.hasDerivAtFilter, HasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
e : 𝕜 →L[𝕜] F
⊢ HasDerivWithinAt.{u, v} (F := F) ((⇑e : (a : 𝕜) → F) : (a : 𝕜) → F) ((e : (a : 𝕜) → F) 1 : F) s x

Tactic:
e.hasDerivAtFilter

Premises used: ContinuousLinearMap.hasDerivAtFilter, HasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
e : 𝕜 →L[𝕜] F
⊢ Eq.{v + 1} (α := F) (deriv (⇑e : (a : 𝕜) → F) x : F) ((e : (a : 𝕜) → F) 1 : F)

Tactic:
e.hasDerivAt.deriv

Premises used: ContinuousLinearMap.hasDerivAt, HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
e : 𝕜 →L[𝕜] F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (derivWithin (⇑e : (a : 𝕜) → F) s x : F) ((e : (a : 𝕜) → F) 1 : F)

Tactic:
e.hasDerivWithinAt.derivWithin hxs

Premises used: HasDerivWithinAt.derivWithin, ContinuousLinearMap.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
e : 𝕜 →ₗ[𝕜] F
⊢ HasDerivAtFilter.{u, v} (F := F) ((⇑e : (a : 𝕜) → F) : (a : 𝕜) → F) ((e : (a : 𝕜) → F) 1 : F) L

Tactic:
e.toContinuousLinearMap₁.hasDerivAtFilter

Premises used: ContinuousLinearMap.hasDerivAtFilter, LinearMap.toContinuousLinearMap₁
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
e : 𝕜 →ₗ[𝕜] F
⊢ HasStrictDerivAt.{u, v} (F := F) ((⇑e : (a : 𝕜) → F) : (a : 𝕜) → F) ((e : (a : 𝕜) → F) 1 : F) x

Tactic:
e.hasDerivAtFilter

Premises used: HasStrictDerivAt, LinearMap.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
e : 𝕜 →ₗ[𝕜] F
⊢ HasDerivAt.{u, v} (F := F) ((⇑e : (a : 𝕜) → F) : (a : 𝕜) → F) ((e : (a : 𝕜) → F) 1 : F) x

Tactic:
e.hasDerivAtFilter

Premises used: HasDerivAt, LinearMap.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
e : 𝕜 →ₗ[𝕜] F
⊢ HasDerivWithinAt.{u, v} (F := F) ((⇑e : (a : 𝕜) → F) : (a : 𝕜) → F) ((e : (a : 𝕜) → F) 1 : F) s x

Tactic:
e.hasDerivAtFilter

Premises used: HasDerivWithinAt, LinearMap.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
e : 𝕜 →ₗ[𝕜] F
⊢ Eq.{v + 1} (α := F) (deriv (⇑e : (a : 𝕜) → F) x : F) ((e : (a : 𝕜) → F) 1 : F)

Tactic:
e.hasDerivAt.deriv

Premises used: HasDerivAt.deriv, LinearMap.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Linear
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
e : 𝕜 →ₗ[𝕜] F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (derivWithin (⇑e : (a : 𝕜) → F) s x : F) ((e : (a : 𝕜) → F) 1 : F)

Tactic:
e.hasDerivWithinAt.derivWithin hxs

Premises used: HasDerivWithinAt.derivWithin, LinearMap.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
simp : (g b - g a) * f a - (f b - f a) * g a = (g b - g a) * f b - (f b - f a) * g b
⊢ h a = h b

Tactic:
simp only [h]
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
⊢ (g b - g a) * f a - (f b - f a) * g a = (g b - g a) * f b - (f b - f a) * g b

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
⊢ h a = h b

Tactic:
have hI : h a = h b := by simp only [h]; ring
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f' x - (f b - f a) * g' x
⊢ ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x

Tactic:
have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := fun x hx =>
    ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
⊢ ContinuousOn h (Icc a b)

Tactic:
have hhc : ContinuousOn h (Icc a b) :=
    (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
hhc : ContinuousOn h (Icc a b)
rcases : ∀ (c : ℝ) (cmem : c ∈ Ioo a b) (hc : h' c = 0), ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

Tactic:
rcases exists_hasDerivAt_eq_zero hab hhc hI hhh' with ⟨c, cmem, hc⟩

Premises used: exists_hasDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f x - (f b - f a) * g x
hI : h a = h b
h' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
hhc : ContinuousOn h (Icc a b)
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

Tactic:
⟨c, cmem, sub_eq_zero.1 hc⟩

Premises used: sub_eq_zero, And.intro, Exists.intro, Iff.mp