[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
⊢ HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x
[PROOFSTEP]
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' 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 
  field_simp [hx, hy, hz]
  ring
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
this : (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) =o[𝓝 (x, x)] fun p => (p.fst - p.snd) * 1
⊢ HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x
[PROOFSTEP]
refine' this.congr' _ (eventually_of_forall fun _ => mul_one _)
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
this : (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) =o[𝓝 (x, x)] fun p => (p.fst - p.snd) * 1
⊢ (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) =ᶠ[𝓝 (x, x)] fun p =>
    p.fst⁻¹ - p.snd⁻¹ - ↑(smulRight 1 (-(x ^ 2)⁻¹)) (p.fst - p.snd)
[PROOFSTEP]
refine' Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) _
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
this : (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) =o[𝓝 (x, x)] fun p => (p.fst - p.snd) * 1
⊢ ∀ (x_1 : 𝕜 × 𝕜),
    ({y | y ≠ 0} ×ˢ {y | y ≠ 0}) x_1 →
      (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) x_1 =
        (fun p => p.fst⁻¹ - p.snd⁻¹ - ↑(smulRight 1 (-(x ^ 2)⁻¹)) (p.fst - p.snd)) x_1
[PROOFSTEP]
rintro ⟨y, z⟩ ⟨hy, hz⟩
[GOAL]
case mk.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
this : (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) =o[𝓝 (x, x)] fun p => (p.fst - p.snd) * 1
y z : 𝕜
hy : (y, z).fst ∈ {y | y ≠ 0}
hz : (y, z).snd ∈ {y | y ≠ 0}
⊢ (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) (y, z) =
    (fun p => p.fst⁻¹ - p.snd⁻¹ - ↑(smulRight 1 (-(x ^ 2)⁻¹)) (p.fst - p.snd)) (y, z)
[PROOFSTEP]
simp only [mem_setOf_eq] at hy hz 
[GOAL]
case mk.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
this : (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) =o[𝓝 (x, x)] fun p => (p.fst - p.snd) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) (y, z) =
    (fun p => p.fst⁻¹ - p.snd⁻¹ - ↑(smulRight 1 (-(x ^ 2)⁻¹)) (p.fst - p.snd)) (y, z)
[PROOFSTEP]
field_simp [hx, hy, hz]
[GOAL]
case mk.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
this : (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) =o[𝓝 (x, x)] fun p => (p.fst - p.snd) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (y - z) * (y * z - x * x) * (y * z * (x ^ 2 * x ^ 2)) =
    ((z - y) * (x ^ 2 * x ^ 2) - y * z * (-(y * x ^ 2) + x ^ 2 * z)) * (x * x * (y * z))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
⊢ (fun p => (p.fst - p.snd) * ((x * x)⁻¹ - (p.fst * p.snd)⁻¹)) =o[𝓝 (x, x)] fun p => (p.fst - p.snd) * 1
[PROOFSTEP]
refine' (isBigO_refl (fun p : 𝕜 × 𝕜 => p.1 - p.2) _).mul_isLittleO ((isLittleO_one_iff 𝕜).2 _)
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
⊢ Tendsto (fun p => (x * x)⁻¹ - (p.fst * p.snd)⁻¹) (𝓝 (x, x)) (𝓝 0)
[PROOFSTEP]
rw [← sub_self (x * x)⁻¹]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hx : x ≠ 0
⊢ Tendsto (fun p => (x * x)⁻¹ - (p.fst * p.snd)⁻¹) (𝓝 (x, x)) (𝓝 ((x * x)⁻¹ - (x * x)⁻¹))
[PROOFSTEP]
exact tendsto_const_nhds.sub ((continuous_mul.tendsto (x, x)).inv₀ <| mul_ne_zero hx hx)
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
⊢ deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hne)
[GOAL]
case inl
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
s t : Set 𝕜
L : Filter 𝕜
⊢ deriv (fun x => x⁻¹) 0 = -(0 ^ 2)⁻¹
[PROOFSTEP]
simp [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv.1 (not_not.2 rfl))]
[GOAL]
case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
hne : x ≠ 0
⊢ deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹
[PROOFSTEP]
exact (hasDerivAt_inv hne).deriv
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹
[PROOFSTEP]
rw [DifferentiableAt.derivWithin (differentiableAt_inv.2 x_ne_zero) hxs]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹
[PROOFSTEP]
exact deriv_inv
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
⊢ fderiv 𝕜 (fun x => x⁻¹) x = smulRight 1 (-(x ^ 2)⁻¹)
[PROOFSTEP]
rw [← deriv_fderiv, deriv_inv]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x => x⁻¹) s x = smulRight 1 (-(x ^ 2)⁻¹)
[PROOFSTEP]
rw [DifferentiableAt.fderivWithin (differentiableAt_inv.2 x_ne_zero) hxs]
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (fun x => x⁻¹) x = smulRight 1 (-(x ^ 2)⁻¹)
[PROOFSTEP]
exact fderiv_inv
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
c : 𝕜 → 𝕜
h : E → 𝕜
c' : 𝕜
z : E
S : Set E
hc : HasDerivWithinAt c c' s x
hx : c x ≠ 0
⊢ HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) s x
[PROOFSTEP]
convert (hasDerivAt_inv hx).comp_hasDerivWithinAt x hc using 1
[GOAL]
case h.e'_7
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
c : 𝕜 → 𝕜
h : E → 𝕜
c' : 𝕜
z : E
S : Set E
hc : HasDerivWithinAt c c' s x
hx : c x ≠ 0
⊢ -c' / c x ^ 2 = -(c x ^ 2)⁻¹ * c'
[PROOFSTEP]
field_simp
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
c : 𝕜 → 𝕜
h : E → 𝕜
c' : 𝕜
z : E
S : Set E
hc : HasDerivAt c c' x
hx : c x ≠ 0
⊢ HasDerivAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
c : 𝕜 → 𝕜
h : E → 𝕜
c' : 𝕜
z : E
S : Set E
hc : HasDerivWithinAt c c' univ x
hx : c x ≠ 0
⊢ HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) univ x
[PROOFSTEP]
exact hc.inv hx
[GOAL]
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x
[PROOFSTEP]
convert hc.mul ((hasDerivAt_inv hx).comp_hasDerivWithinAt x hd) using 1
[GOAL]
case h.e'_6
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ (fun y => c y / d y) = fun y => c y * ((fun y => y⁻¹) ∘ d) y
[PROOFSTEP]
simp only [div_eq_mul_inv, (· ∘ ·)]
[GOAL]
case h.e'_7
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : 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') / d x ^ 2 = c' * ((fun y => y⁻¹) ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_7
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : 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') * (d x * d x ^ 2) = (c' * d x ^ 2 + -(c x * d' * d x)) * d x ^ 2
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ HasStrictDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
[PROOFSTEP]
convert hc.mul ((hasStrictDerivAt_inv hx).comp x hd) using 1
[GOAL]
case h.e'_6
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ (fun y => c y / d y) = fun y => c y * (Inv.inv ∘ d) y
[PROOFSTEP]
simp only [div_eq_mul_inv, (· ∘ ·)]
[GOAL]
case h.e'_7
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : 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') / d x ^ 2 = c' * (Inv.inv ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_7
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : 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') * (d x * d x ^ 2) = (c' * d x ^ 2 + -(c x * d' * d x)) * d x ^ 2
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
hx : d x ≠ 0
⊢ HasDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
[PROOFSTEP]
rw [← hasDerivWithinAt_univ] at *
[GOAL]
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : 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') / d x ^ 2) univ x
[PROOFSTEP]
exact hc.div hd hx
