-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem hasStrictDerivAt_inv (hx : x ≠ 0) : HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ Tendsto (fun p => (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 0)

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

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ Tendsto (fun p => (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 ((x * x)⁻¹ - (x * x)⁻¹))

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ HasStrictDerivAt Inv.inv (-(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
  field_simp [hx, hy, hz]
  ring

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1

Proof state:
𝕜 : 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)

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
⊢ ∀ (x_1 : 𝕜 × 𝕜),
    ({y | y ≠ 0} ×ˢ {y | y ≠ 0}) x_1 →
      (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) x_1 =
        (fun p => p.1⁻¹ - p.2⁻¹ - (smulRight 1 (-(x ^ 2)⁻¹)) (p.1 - p.2)) x_1

Tactic:
rintro ⟨y, z⟩ ⟨hy, hz⟩

Result:
case mk.intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
y z : 𝕜
hy : (y, z).1 ∈ {y | y ≠ 0}
hz : (y, z).2 ∈ {y | y ≠ 0}
⊢ (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z) =
    (fun p => p.1⁻¹ - p.2⁻¹ - (smulRight 1 (-(x ^ 2)⁻¹)) (p.1 - p.2)) (y, z)

Proof state:
case mk.intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
y z : 𝕜
hy : (y, z).1 ∈ {y | y ≠ 0}
hz : (y, z).2 ∈ {y | y ≠ 0}
⊢ (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z) =
    (fun p => p.1⁻¹ - p.2⁻¹ - (smulRight 1 (-(x ^ 2)⁻¹)) (p.1 - p.2)) (y, z)

Tactic:
simp only [mem_setOf_eq] at hy hz

Result:
case mk.intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z) =
    (fun p => p.1⁻¹ - p.2⁻¹ - (smulRight 1 (-(x ^ 2)⁻¹)) (p.1 - p.2)) (y, z)

Proof state:
case mk.intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z) =
    (fun p => p.1⁻¹ - p.2⁻¹ - (smulRight 1 (-(x ^ 2)⁻¹)) (p.1 - p.2)) (y, z)

Tactic:
field_simp [hx, hy, hz]

Result:
case mk.intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (y - z) * (y * z - x * x) * (y * z * x ^ 2) = ((z - y) * x ^ 2 - y * z * (z - y)) * (x * x * (y * z))

Proof state:
case mk.intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (y - z) * (y * z - x * x) * (y * z * x ^ 2) = ((z - y) * x ^ 2 - y * z * (z - y)) * (x * x * (y * z))

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
⊢ (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =ᶠ[𝓝 (x, x)] fun p =>
    p.1⁻¹ - p.2⁻¹ - (smulRight 1 (-(x ^ 2)⁻¹)) (p.1 - p.2)

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

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
⊢ ∀ (x_1 : 𝕜 × 𝕜),
    ({y | y ≠ 0} ×ˢ {y | y ≠ 0}) x_1 →
      (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) x_1 =
        (fun p => p.1⁻¹ - p.2⁻¹ - (smulRight 1 (-(x ^ 2)⁻¹)) (p.1 - p.2)) x_1

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1

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

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ Tendsto (fun p => (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 0)

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
⊢ HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x

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

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
⊢ (fun p => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =ᶠ[𝓝 (x, x)] fun p =>
    p.1⁻¹ - p.2⁻¹ - (smulRight 1 (-(x ^ 2)⁻¹)) (p.1 - p.2)