-- 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:
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)

Tactic:
refine this.congr_fderiv (LinearMap.ext_on_codisjoint
  (Submodule.isCompl_orthogonal_of_completeSpace (K := ℝ ∙ x)).codisjoint
  (LinearMap.eqOn_span' ?_) fun y hy ↦ ?_)

Result:
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)
⊢ 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}

case intro.refine_2.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)
y : F
hy : y ∈ ↑(Submodule.span ℝ {x})ᗮ
⊢ ((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))
      y =
    ((R / dist ((fun x => c + x) x) c) ^ 2 •
        ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv,
            continuous_toFun := ⋯, continuous_invFun := ⋯ })
      y

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)
⊢ HasFDerivAt (fun x => (R ^ 2 * (‖x - c‖ ^ 2)⁻¹) • (x -ᵥ c) +ᵥ c) ?intro.refine_1 (c + x)

Tactic:
have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul
  (R ^ 2)

Result:
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)

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

Tactic:
rcases add_left_surjective c x with ⟨x, rfl⟩

Result:
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)

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 ^ 2 * (‖x - c‖ ^ 2)⁻¹) • (x -ᵥ c) +ᵥ c) ?intro.refine_1 (c + x)

Tactic:
have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c

Result:
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)
⊢ HasFDerivAt (fun x => (R ^ 2 * (‖x - c‖ ^ 2)⁻¹) • (x -ᵥ c) +ᵥ c) ?intro.refine_1 (c + x)

Proof state:
case intro.refine_2.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)
y : F
hy : y ∈ ↑(Submodule.span ℝ {x})ᗮ
⊢ ((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))
      y =
    ((R / dist ((fun x => c + x) x) c) ^ 2 •
        ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv,
            continuous_toFun := ⋯, continuous_invFun := ⋯ })
      y

Tactic:
simp [Submodule.mem_orthogonal_singleton_iff_inner_right.1 hy,
  reflection_mem_subspace_eq_self hy, div_eq_mul_inv, mul_pow]

Result:
no goals