𝕜 : 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
𝕜 : 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
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
𝕜 : 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)
𝕜 : 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
refine' (isBigO_refl (fun p : 𝕜 × 𝕜 => p.1 - p.2) _).mul_isLittleO ((isLittleO_one_iff 𝕜).2 _)
𝕜 : 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)⁻¹))
𝕜 : 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)
rw [← sub_self (x * x)⁻¹]
no goals
𝕜 : 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)⁻¹))
exact tendsto_const_nhds.sub ((continuous_mul.tendsto (x, x)).inv₀ <| mul_ne_zero hx hx)
𝕜 : 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)
𝕜 : 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
refine' this.congr' _ (eventually_of_forall fun _ => mul_one _)
𝕜 : 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
𝕜 : 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)
refine' Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) _
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)
𝕜 : 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
rintro ⟨y, z⟩ ⟨hy, hz⟩
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)
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)
simp only [mem_setOf_eq] at hy hz
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))
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)
field_simp [hx, hy, hz]
no goals
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))
ring