-- Mathlib/Geometry/Euclidean/Inversion/Calculus.lean
theorem hasFDerivAt_inversion (hx : x ≠ c) :
    HasFDerivAt (inversion c R)
      ((R / dist x c) ^ 2 • (reflection (ℝ ∙ (x - c))ᗮ : F →L[ℝ] F)) x

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
⊢ HasFDerivAt (fun x => (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ?intro.refine_1 (c + x)

Tactic:
simp_rw [dist_eq_norm, div_pow, div_eq_mul_inv]

Result:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
⊢ HasFDerivAt (fun x => (R ^ 2 * (‖x - c‖ ^ 2)⁻¹) • (x -ᵥ c) +ᵥ c) ?intro.refine_1 (c + x)

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
A : HasFDerivAt (fun x => _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
B :
  HasFDerivAt (fun y => R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) y)
    (R ^ 2 •
      -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
        2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F))
    (c + x)
⊢ HasFDerivAt (fun x => (R ^ 2 * (‖x - c‖ ^ 2)⁻¹) • (x -ᵥ c) +ᵥ c) ?intro.refine_1 (c + x)

Tactic:
exact (B.smul A).add_const c

Result:
no goals

Proof state:
case intro.refine_2.refine_1
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
this✝ :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight
        (_root_.id (c + x) - c))
    (c + x)
this : ((‖x‖ ^ 2) ^ 2)⁻¹ * ‖x‖ ^ 2 = (‖x‖ ^ 2)⁻¹
⊢ EqOn
    ⇑((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
        (R ^ 2 •
              -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
                2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight
          (_root_.id (c + x) - c))
    ⇑((R / dist ((fun x => c + x) x) c) ^ 2 •
        ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv,
            continuous_toFun := ⋯, continuous_invFun := ⋯ })
    {x}

Tactic:
simp [reflection_orthogonalComplement_singleton_eq_neg, real_inner_self_eq_norm_sq,
  two_mul, this, div_eq_mul_inv, mul_add, add_smul, mul_pow]

Result:
no goals

Proof state:
case intro
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
⊢ HasFDerivAt (inversion c R)
    ((R / dist ((fun x => c + x) x) c) ^ 2 •
      ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv,
          continuous_toFun := ⋯, continuous_invFun := ⋯ })
    ((fun x => c + x) x)

Tactic:
have : HasFDerivAt (inversion c R) (?_ : F →L[ℝ] F) (c + x) := by
  simp +unfoldPartialApp only [inversion]
  simp_rw [dist_eq_norm, div_pow, div_eq_mul_inv]
  have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c
  have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul
    (R ^ 2)
  exact (B.smul A).add_const c

Result:
case intro.refine_2
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ HasFDerivAt (inversion c R)
    ((R / dist ((fun x => c + x) x) c) ^ 2 •
      ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv,
          continuous_toFun := ⋯, continuous_invFun := ⋯ })
    ((fun x => c + x) x)

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
⊢ HasFDerivAt (inversion c R) ?intro.refine_1 (c + x)

Tactic:
simp +unfoldPartialApp only [inversion]

Result:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
⊢ HasFDerivAt (fun x => (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ?intro.refine_1 (c + x)

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ ((‖x‖ ^ 2) ^ 2)⁻¹ * ‖x‖ ^ 2 = (‖x‖ ^ 2)⁻¹

Tactic:
rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
A : HasFDerivAt (fun x => _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ ‖_root_.id (c + x) - c‖ ^ 2 ≠ 0

Tactic:
simpa using hx

Result:
no goals