awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : -c' / HPow.hPow (β := ℕ) (c x) 2 = -(HPow.hPow (β := ℕ) (c x) 2)⁻¹ * c'
⊢ HasDerivWithinAt c⁻¹ (-c' / HPow.hPow (β := ℕ) (c x) 2) s x

Tactic:
convert! (hasDerivAt_inv hx).comp_hasDerivWithinAt x hc using 1

Premises used: hasDerivAt_inv, HasDerivAt.comp_hasDerivWithinAt
-- 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
⊢ -c' / HPow.hPow (β := ℕ) (c x) 2 = -(HPow.hPow (β := ℕ) (c x) 2)⁻¹ * c'

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivAt c c' x
hx : c x ≠ 0
rw :
  ∀ (hc : HasDerivWithinAt c c' univ x) (hx : c x ≠ 0), HasDerivWithinAt c⁻¹ (-c' / HPow.hPow (β := ℕ) (c x) 2) univ x
⊢ HasDerivAt c⁻¹ (-c' / HPow.hPow (β := ℕ) (c x) 2) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' univ x
hx : c x ≠ 0
⊢ HasDerivWithinAt c⁻¹ (-c' / HPow.hPow (β := ℕ) (c x) 2) univ x

Tactic:
hc.inv hx

Premises used: HasDerivWithinAt.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' univ x
hx : c x ≠ 0
⊢ HasDerivWithinAt c⁻¹ (-c' / HPow.hPow (β := ℕ) (c x) 2) univ x

Tactic:
exact hc.inv hx

Premises used: HasDerivWithinAt.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2
⊢ derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2

Tactic:
(hc.hasDerivWithinAt.inv hx).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2

Tactic:
exact (hc.hasDerivWithinAt.inv hx).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
⊢ derivWithin c⁻¹ s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2

Tactic:
derivWithin_fun_inv' hc hx

Premises used: derivWithin_fun_inv'
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableAt 𝕜 c x
hx : c x ≠ 0
⊢ deriv (fun (x : 𝕜) ↦ (c x)⁻¹) x = -deriv c x / HPow.hPow (β := ℕ) (c x) 2

Tactic:
(hc.hasDerivAt.inv hx).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableAt 𝕜 c x
hx : c x ≠ 0
⊢ deriv c⁻¹ x = -deriv c x / HPow.hPow (β := ℕ) (c x) 2

Tactic:
(hc.hasDerivAt.inv hx).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun (i : 𝕜) ↦ c i * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) i)
    (c' * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')) s x

Tactic:
hc.fun_mul ((hasDerivAt_inv hx).comp_hasDerivWithinAt x hd)

Premises used: hasDerivAt_inv, HasDerivWithinAt.fun_mul, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
h : Eq (α := 𝕜 → 𝕜') (fun (y : 𝕜) ↦ c y / d y) fun (i : 𝕜) ↦ c i * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) i
h₁ :
  (c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2 =
    c' * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) s x

Tactic:
convert! hc.fun_mul ((hasDerivAt_inv hx).comp_hasDerivWithinAt x hd) using 1

Premises used: hasDerivAt_inv, HasDerivWithinAt.fun_mul, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ Eq (α := 𝕜 → 𝕜') (fun (y : 𝕜) ↦ c y / d y) fun (i : 𝕜) ↦ c i * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) i

Tactic:
simp only [div_eq_mul_inv, (· ∘ ·)]

Premises used: Function.comp, div_eq_mul_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
h : c' * d x - c x * d' = c' * d x + -(c x * d')
⊢ (c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2 =
    c' * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')

Tactic:
simp [field]
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ c' * d x - c x * d' = c' * d x + -(c x * d')

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ HasDerivWithinAt (c / d) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) s x

Tactic:
hc.fun_div hd hx

Premises used: HasDerivWithinAt.fun_div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ HasStrictDerivAt (fun (i : 𝕜) ↦ c i * (Inv.inv ∘ d) i)
    (c' * (Inv.inv ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')) x

Tactic:
hc.fun_mul ((hasStrictDerivAt_inv hx).comp x hd)

Premises used: HasStrictDerivAt.comp, hasStrictDerivAt_inv, HasStrictDerivAt.fun_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
h : Eq (α := 𝕜 → 𝕜') (fun (y : 𝕜) ↦ c y / d y) fun (i : 𝕜) ↦ c i * (Inv.inv ∘ d) i
h₁ :
  (c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2 =
    c' * (Inv.inv ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) x

Tactic:
convert! hc.fun_mul ((hasStrictDerivAt_inv hx).comp x hd) using 1

Premises used: HasStrictDerivAt.comp, hasStrictDerivAt_inv, HasStrictDerivAt.fun_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ Eq (α := 𝕜 → 𝕜') (fun (y : 𝕜) ↦ c y / d y) fun (i : 𝕜) ↦ c i * (Inv.inv ∘ d) i

Tactic:
simp only [div_eq_mul_inv, (· ∘ ·)]

Premises used: Function.comp, div_eq_mul_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
h : c' * d x - c x * d' = c' * d x + -(c x * d')
⊢ (c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2 =
    c' * (Inv.inv ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')

Tactic:
simp [field]
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ c' * d x - c x * d' = c' * d x + -(c x * d')

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ HasStrictDerivAt (c / d) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) x

Tactic:
hc.fun_div hd hx

Premises used: HasStrictDerivAt.fun_div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
hx : d x ≠ 0
rw :
  ∀ (hc : HasDerivWithinAt c c' univ x) (hd : HasDerivWithinAt d d' univ x) (hx : d x ≠ 0),
    HasDerivWithinAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) univ x
⊢ HasDerivAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) univ x

Tactic:
hc.div hd hx

Premises used: HasDerivWithinAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) univ x

Tactic:
exact hc.div hd hx

Premises used: HasDerivWithinAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
hx : d x ≠ 0
⊢ HasDerivAt (c / d) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) x

Tactic:
hc.fun_div hd hx

Premises used: HasDerivAt.fun_div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
⊢ DifferentiableWithinAt.{u, u, u_1} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ c x / d x) s x

Tactic:
(hc.hasDerivWithinAt.div hd.hasDerivWithinAt hx).differentiableWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.differentiableWithinAt, HasDerivWithinAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
⊢ DifferentiableWithinAt 𝕜 (c / d) s x

Tactic:
hc.fun_div hd hx

Premises used: DifferentiableWithinAt.fun_div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
hx : d x ≠ 0
⊢ DifferentiableAt.{u, u, u_1} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ c x / d x) x

Tactic:
(hc.hasDerivAt.div hd.hasDerivAt hx).differentiableAt

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, HasDerivAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
hx : d x ≠ 0
⊢ DifferentiableAt 𝕜 (c / d) x

Tactic:
hc.fun_div hd hx

Premises used: DifferentiableAt.fun_div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableOn 𝕜 c s
hd : DifferentiableOn 𝕜 d s
hx : ∀ x ∈ s, d x ≠ 0
⊢ DifferentiableOn.{u, u, u_1} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ c x / d x) s

Tactic:
fun x h =>
  (hc x h).div (hd x h) (hx x h)

Premises used: DifferentiableWithinAt.div, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableOn 𝕜 c s
hd : DifferentiableOn 𝕜 d s
hx : ∀ x ∈ s, d x ≠ 0
⊢ DifferentiableOn 𝕜 (c / d) s

Tactic:
fun x h =>
  (hc x h).div (hd x h) (hx x h)

Premises used: DifferentiableWithinAt.div, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : Differentiable 𝕜 c
hd : Differentiable 𝕜 d
hx : ∀ (x : 𝕜), d x ≠ 0
⊢ Differentiable.{u, u, u_1} 𝕜 (F := 𝕜') fun (x : 𝕜) ↦ c x / d x

Tactic:
fun x => (hc x).div (hd x) (hx x)

Premises used: Differentiable, DifferentiableAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : Differentiable 𝕜 c
hd : Differentiable 𝕜 d
hx : ∀ (x : 𝕜), d x ≠ 0
⊢ Differentiable 𝕜 (c / d)

Tactic:
fun x => (hc x).div (hd x) (hx x)

Premises used: Differentiable, DifferentiableAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
      (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
      (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2
⊢ derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
    (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
    (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2

Tactic:
(hc.hasDerivWithinAt.div hd.hasDerivWithinAt hx).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
    (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2

Tactic:
exact (hc.hasDerivWithinAt.div hd.hasDerivWithinAt hx).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
    (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
⊢ derivWithin (c / d) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2

Tactic:
derivWithin_fun_div hc hd hx

Premises used: derivWithin_fun_div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
hx : d x ≠ 0
⊢ deriv (fun (x : 𝕜) ↦ c x / d x) x = (deriv c x * d x - c x * deriv d x) / HPow.hPow (β := ℕ) (d x) 2

Tactic:
(hc.hasDerivAt.div hd.hasDerivAt hx).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
hx : d x ≠ 0
⊢ deriv (c / d) x = (deriv c x * d x - c x * deriv d x) / HPow.hPow (β := ℕ) (d x) 2

Tactic:
(hc.hasDerivAt.div hd.hasDerivAt hx).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.div
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
d : 𝕜 → 𝕜'
c : 𝕜'
hd : DifferentiableAt 𝕜 d x
hx : d x ≠ 0
⊢ deriv (fun (x : 𝕜) ↦ c / d x) x = -c * deriv d x / HPow.hPow (β := ℕ) (d x) 2

Tactic:
simp [deriv_fun_div (differentiableAt_const c) hd hx]

Premises used: deriv_fun_div, differentiableAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Inv
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ c / x) x = -c / HPow.hPow (β := ℕ) x 2

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
f' x : 𝕜
hf : HasStrictDerivAt f f' x
hf' : f' ≠ 0
⊢ HasStrictFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 f' hf')) : 𝕜 →L[𝕜] 𝕜)
    x

Tactic:
hf

Premises used: HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, HasStrictFDerivAt, LinearMap.smulRight, LinearMap.toSpanSingleton, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
f' x : 𝕜
hf : HasDerivAt f f' x
hf' : f' ≠ 0
⊢ HasFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 f' hf')) : 𝕜 →L[𝕜] 𝕜) x

Tactic:
hf

Premises used: HasFDerivAt, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, LinearMap.smulRight, LinearMap.toSpanSingleton, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Inverse
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
f' a : 𝕜
hg : ContinuousAt g a
hf : HasStrictDerivAt f f' (g a)
hf' : f' ≠ 0
hfg : ∀ᶠ (y : 𝕜) in 𝓝 a, f (g y) = y
⊢ HasStrictDerivAt g f'⁻¹ a

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

Premises used: HasStrictFDerivAt.of_local_left_inverse, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, LinearMap.smulRight, HasStrictDerivAt, HasStrictDerivAt.hasStrictFDerivAt_equiv, 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' : HasStrictDerivAt (↑f : 𝕜 → 𝕜) f' ((↑f.symm : 𝕜 → 𝕜) a)
⊢ HasStrictDerivAt (↑f.symm : 𝕜 → 𝕜) f'⁻¹ a

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

Premises used: OpenPartialHomeomorph.continuousAt, HasStrictDerivAt.of_local_left_inverse, OpenPartialHomeomorph.eventually_right_inverse, OpenPartialHomeomorph.symm
-- 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
x : 𝕜
⊢ (ContinuousLinearMap.toSpanSingleton 𝕜 f'⁻¹ : (a : 𝕜) → 𝕜)
      ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → 𝕜) x : 𝕜) =
    x

Tactic:
simp [hf']
-- 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₁ : h' / f' = (ContinuousLinearMap.toSpanSingleton 𝕜 f'⁻¹ ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 h' : (a : 𝕜) → 𝕜) 1
⊢ HasDerivAt g (h' / f') a

Tactic:
convert hf.hasFDerivAt.of_comp_of_leftInverse hst hh hcomp (f'symm := .toSpanSingleton 𝕜 f'⁻¹)
    (fun _ ↦ by simp [hf']) |>.hasDerivAt using 1

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.hasDerivAt, HasFDerivAt.of_comp_of_leftInverse