awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)

Tactic:
exact (hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf.hasDerivWithinAt hs).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasFDerivWithinAt.comp_hasDerivWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t y
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
⊢ DifferentiableWithinAt 𝕜 l t (f x)

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t y
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
hl₁ : DifferentiableWithinAt 𝕜 l t (f x)
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t y
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
hl₁ : DifferentiableWithinAt 𝕜 l t (f x)
hf₁ : DifferentiableWithinAt 𝕜 f s x
⊢ MapsTo f s t

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t y
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
hl₁ : DifferentiableWithinAt 𝕜 l t (f x)
hf₁ : DifferentiableWithinAt 𝕜 f s x
hs₁ : MapsTo f s t
⊢ y = f x

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)

Tactic:
fderivWithin_comp_derivWithin x hl hf hs

Premises used: fderivWithin_comp_derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)

Tactic:
exact fderivWithin_comp_derivWithin x hl hf hs

Premises used: fderivWithin_comp_derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
hl : DifferentiableAt 𝕜 l (f x)
hf : DifferentiableAt 𝕜 f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : (a : F) → E) (deriv f x)

Tactic:
(hl.hasFDerivAt.comp_hasDerivAt x hf.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasFDerivAt.comp_hasDerivAt, DifferentiableAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l y
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ DifferentiableAt 𝕜 l (f x)

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l y
hf : DifferentiableAt 𝕜 f x
hy : y = f x
hl₁ : DifferentiableAt 𝕜 l (f x)
⊢ DifferentiableAt 𝕜 f x

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l y
hf : DifferentiableAt 𝕜 f x
hy : y = f x
hl₁ : DifferentiableAt 𝕜 l (f x)
hf₁ : DifferentiableAt 𝕜 f x
⊢ y = f x

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l (f x)
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : (a : F) → E) (deriv f x)

Tactic:
fderiv_comp_deriv x hl hf

Premises used: fderiv_comp_deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l (f x)
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : (a : F) → E) (deriv f x)

Tactic:
exact fderiv_comp_deriv x hl hf

Premises used: fderiv_comp_deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.CompMul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
f' : E
s : Set 𝕜
x : 𝕜
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ f (c * x)) (c • f') s x ↔ HasDerivWithinAt f f' (c • s) (c * x)

Tactic:
simp only [hasDerivWithinAt_iff_hasFDerivWithinAt, ← smul_eq_mul,
    ← hasFDerivWithinAt_comp_smul_smul_iff, ContinuousLinearMap.toSpanSingleton_smul]

Premises used: hasDerivWithinAt_iff_hasFDerivWithinAt, ContinuousLinearMap.toSpanSingleton_smul, hasFDerivWithinAt_comp_smul_smul_iff, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.CompMul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
simp : derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)
⊢ derivWithin (fun (x : 𝕜) ↦ f (c * x)) s x = c • derivWithin f (c • s) (c * x)

Tactic:
simp only [← smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.CompMul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
rw : derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = derivWithin (c • f) (c • s) (c • x)
rw₁ :
  ((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 =
    derivWithin (c • f) (c • s) (c • x)
rw₂ :
  Eq.{u_2 + 1} (α := E)
    (((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
    (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
rw₃ :
  Eq.{u_2 + 1} (α := E) (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
    (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
rw₄ rw₅ :
  Eq.{u_2 + 1} (α := E) (((fderivWithin 𝕜 (fun (i : 𝕜) ↦ c • f i) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
    (((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (i : 𝕜) ↦ c • f i) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 :
      E)
⊢ derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)

Tactic:
rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]

Premises used: derivWithin_const_smul_field, fderivWithin_comp_smul_eq_fderivWithin_smul, derivWithin, Pi.smul_def
-- Module: Mathlib.Analysis.Calculus.Deriv.CompMul
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ f (c * x)) x = c • deriv f (c * x)

Tactic:
simp only [← smul_eq_mul, deriv, fderiv_comp_smul, ContinuousLinearMap.smul_apply]

Premises used: ContinuousLinearMap.smul_apply, deriv, smul_eq_mul, fderiv_comp_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
⊢ HasStrictDerivAt Inv.inv (-(HPow.hPow (β := ℕ) x 2)⁻¹) x

Tactic:
.of_isLittleO <| this.congr' ?_ (Eventually.of_forall fun _ => mul_one _)

Premises used: HSub.hSub, Filter.Eventually.of_forall, Prod.fst, Asymptotics.IsLittleO.congr', HasDerivAtFilter, HasFDerivAtFilter.of_isLittleO, mul_one, HasStrictDerivAt, Prod.snd
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
refine :
  (𝓝 (x, x)).EventuallyEq (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹) ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜)
⊢ HasStrictDerivAt Inv.inv (-(HPow.hPow (β := ℕ) x 2)⁻¹) x

Tactic:
refine .of_isLittleO <| this.congr' ?_ (Eventually.of_forall fun _ => mul_one _)

Premises used: HSub.hSub, Filter.Eventually.of_forall, Prod.fst, Asymptotics.IsLittleO.congr', mul_one, Prod.snd
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
⊢ (𝓝 (x, x)).EventuallyEq (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹) ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜)

Tactic:
Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, isOpen_ne, And.intro, IsOpen.mem_nhds, IsOpen.prod
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
refine :
  ∀ (x_1 : 𝕜 × 𝕜),
    SProd.sprod (α := Set 𝕜) (β := Set 𝕜) {y : 𝕜 | y ≠ 0} {y : 𝕜 | y ≠ 0} x_1 →
      Eq.{u + 1} (α := 𝕜) ((fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) x_1)
        ((fun (p : 𝕜 × 𝕜) ↦
            HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹)
              ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜))
          x_1)
⊢ (𝓝 (x, x)).EventuallyEq (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹) ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜)

Tactic:
refine Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) ?_
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
simp : (y - z) * (y * z - HPow.hPow (β := ℕ) x 2) = HPow.hPow (β := ℕ) x 2 * (z - y) + y * z * (y - z)
⊢ Eq.{u + 1} (α := 𝕜) ((fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z))
    ((fun (p : 𝕜 × 𝕜) ↦
        HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹)
          ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜))
      (y, z))

Tactic:
simp [field]
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (y - z) * (y * z - HPow.hPow (β := ℕ) x 2) = HPow.hPow (β := ℕ) x 2 * (z - y) + y * z * (y - z)

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
p :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
⊢ HasStrictDerivAt Inv.inv (-(HPow.hPow (β := ℕ) x 2)⁻¹) x

Tactic:
suffices
    (fun p : 𝕜 × 𝕜 => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p =>
      (p.1 - p.2) * 1 by
    refine .of_isLittleO <| this.congr' ?_ (Eventually.of_forall fun _ => mul_one _)
    refine Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) ?_
    rintro ⟨y, z⟩ ⟨hy, hz⟩
    simp only [mem_setOf_eq] at hy hz
    simp [field]
    ring
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1

Tactic:
(isBigO_refl (fun p : 𝕜 × 𝕜 => p.1 - p.2) _).mul_isLittleO ((isLittleO_one_iff 𝕜).2 ?_)

Premises used: Iff.mpr, HSub.hSub, Prod.fst, Asymptotics.IsBigO.mul_isLittleO, Asymptotics.isLittleO_one_iff, Prod.snd, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
refine : Tendsto (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 0)
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1

Tactic:
refine (isBigO_refl (fun p : 𝕜 × 𝕜 => p.1 - p.2) _).mul_isLittleO ((isLittleO_one_iff 𝕜).2 ?_)

Premises used: Iff.mpr, HSub.hSub, Prod.fst, Asymptotics.IsBigO.mul_isLittleO, Asymptotics.isLittleO_one_iff, Prod.snd, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
rw : Tendsto (fun (p : 𝕜 × 𝕜) ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 ((x * x)⁻¹ - (x * x)⁻¹))
⊢ Tendsto (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 0)

Tactic:
rw [← sub_self (x * x)⁻¹]

Premises used: HMul.hMul, sub_self, Inv.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ Tendsto (fun (p : 𝕜 × 𝕜) ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 ((x * x)⁻¹ - (x * x)⁻¹))

Tactic:
tendsto_const_nhds.sub ((continuous_mul.tendsto (x, x)).inv₀ <| mul_ne_zero hx hx)

Premises used: tendsto_const_nhds, continuous_mul, Prod.mk, Continuous.tendsto, Filter.Tendsto.inv₀, mul_ne_zero, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ Tendsto (fun (p : 𝕜 × 𝕜) ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 ((x * x)⁻¹ - (x * x)⁻¹))

Tactic:
exact tendsto_const_nhds.sub ((continuous_mul.tendsto (x, x)).inv₀ <| mul_ne_zero hx hx)

Premises used: tendsto_const_nhds, continuous_mul, Prod.mk, Continuous.tendsto, Filter.Tendsto.inv₀, mul_ne_zero, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
x_ne_zero : x ≠ 0
⊢ HasDerivAt (fun (y : 𝕜) ↦ y⁻¹) (-(HPow.hPow (β := ℕ) x 2)⁻¹) x

Tactic:
(hasStrictDerivAt_inv x_ne_zero).hasDerivAt

Premises used: hasStrictDerivAt_inv, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
x_ne_zero : x ≠ 0
s : Set 𝕜
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ x⁻¹) (-(HPow.hPow (β := ℕ) x 2)⁻¹) s x

Tactic:
(hasDerivAt_inv x_ne_zero).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, hasDerivAt_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) x ↔ x ≠ 0

Tactic:
⟨fun H => NormedField.continuousAt_inv.1 H.continuousAt, fun H =>
    (hasDerivAt_inv H).differentiableAt⟩

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.continuousAt, hasDerivAt_inv, NormedField.continuousAt_inv, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inl : deriv (fun (x : 𝕜) ↦ x⁻¹) 0 = -(HPow.hPow (α := 𝕜) (β := ℕ) 0 2)⁻¹
inr : ∀ (hne : x ≠ 0), deriv (fun (x : 𝕜) ↦ x⁻¹) x = -(HPow.hPow (β := ℕ) x 2)⁻¹
⊢ deriv (fun (x : 𝕜) ↦ x⁻¹) x = -(HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
rcases eq_or_ne x 0 with (rfl | hne)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inl : 0 = -(HPow.hPow (α := 𝕜) (β := ℕ) 0 2)⁻¹
⊢ deriv (fun (x : 𝕜) ↦ x⁻¹) 0 = -(HPow.hPow (α := 𝕜) (β := ℕ) 0 2)⁻¹

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))]

Premises used: Iff.mpr, deriv_zero_of_not_differentiableAt, Classical.not_not, mt, rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
⊢ 0 = -(HPow.hPow (α := 𝕜) (β := ℕ) 0 2)⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hne : x ≠ 0
⊢ deriv (fun (x : 𝕜) ↦ x⁻¹) x = -(HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
(hasDerivAt_inv hne).deriv

Premises used: HasDerivAt.deriv, hasDerivAt_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hne : x ≠ 0
⊢ deriv (fun (x : 𝕜) ↦ x⁻¹) x = -(HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
exact (hasDerivAt_inv hne).deriv

Premises used: HasDerivAt.deriv, hasDerivAt_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
⊢ Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (deriv fun (x : 𝕜) ↦ x⁻¹) fun (x : 𝕜) ↦ -(HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
funext fun _ => deriv_inv

Premises used: deriv_inv, funext
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
rw : deriv Inv.inv x = -(HPow.hPow (β := ℕ) x 2)⁻¹
⊢ derivWithin (fun (x : 𝕜) ↦ x⁻¹) s x = -(HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
rw [DifferentiableAt.derivWithin (differentiableAt_inv x_ne_zero) hxs]

Premises used: DifferentiableAt.derivWithin, differentiableAt_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv Inv.inv x = -(HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
deriv_inv

Premises used: deriv_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv Inv.inv x = -(HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
exact deriv_inv

Premises used: deriv_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
x_ne_zero : x ≠ 0
⊢ HasFDerivAt (𝕜 := 𝕜) (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹)) x

Tactic:
hasDerivAt_inv x_ne_zero

Premises used: HasFDerivAt, hasDerivAt_inv, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
x_ne_zero : x ≠ 0
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹)) x

Tactic:
hasStrictDerivAt_inv x_ne_zero

Premises used: HasDerivAtFilter, HasStrictFDerivAt, hasStrictDerivAt_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹)) s x

Tactic:
(hasFDerivAt_inv x_ne_zero).hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, hasFDerivAt_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
rw :
  Eq (α := 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (deriv (fun (x : 𝕜) ↦ x⁻¹) x))
    (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))
rw₁ rw₂ :
  Eq (α := 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))
    (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) x : 𝕜 →L[𝕜] 𝕜)
    (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : 𝕜 →L[𝕜] 𝕜)

Tactic:
rw [← toSpanSingleton_deriv, deriv_inv]

Premises used: deriv_inv, toSpanSingleton_deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
rw : Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 Inv.inv x : 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderivWithin 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) s x : 𝕜 →L[𝕜] 𝕜)
    (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : 𝕜 →L[𝕜] 𝕜)

Tactic:
rw [DifferentiableAt.fderivWithin (differentiableAt_inv x_ne_zero) hxs]

Premises used: DifferentiableAt.fderivWithin, differentiableAt_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 Inv.inv x : 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))

Tactic:
fderiv_inv

Premises used: fderiv_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 Inv.inv x : 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))

Tactic:
exact fderiv_inv

Premises used: fderiv_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' s x
hx : c x ≠ 0
⊢ HasDerivWithinAt ((fun (y : 𝕜) ↦ y⁻¹) ∘ c) (-(HPow.hPow (β := ℕ) (c x) 2)⁻¹ * c') s x

Tactic:
(hasDerivAt_inv hx).comp_hasDerivWithinAt x hc

Premises used: hasDerivAt_inv, HasDerivAt.comp_hasDerivWithinAt