-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Calculus (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
refine_2 :
  EqOn (α := F) (β := F)
    (⇑(↑(HSMul.hSMul (β := F →L[ℝ] F)
                (HPow.hPow (β := ℕ) R 2 *
                  ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
                (ContinuousLinearMap.id ℝ F) +
              (HPow.hPow (β := ℕ) R 2 •
                    -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
                      HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                        (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                          ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c))
                          (ContinuousLinearMap.id ℝ F))).smulRight
                (_root_.id (c + x) - c)) :
          F →ₗ[ℝ] F) :
      (a : F) → F)
    (⇑(↑(HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist ((fun (x : F) ↦ c + x) x) c) 2)
              (↑(↑(Submodule.reflection (ℝ ∙ ((fun (x : F) ↦ c + x) x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F)) :
          F →ₗ[ℝ] F) :
      (a : F) → F)
    {x}
⊢ HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist ((fun (x : F) ↦ c + x) x) c) 2)
      (↑(↑(Submodule.reflection (ℝ ∙ ((fun (x : F) ↦ c + x) x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F))
    ((fun (x : F) ↦ c + x) x)
have refine_2₁ : ∀ (y : F) (hy : y ∈ (↑(ℝ ∙ x)ᗮ : Set F)),
  Eq (α := F)
    ((HSMul.hSMul (β := F →L[ℝ] F)
              (HPow.hPow (β := ℕ) R 2 *
                ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
              (ContinuousLinearMap.id ℝ F) +
            (HPow.hPow (β := ℕ) R 2 •
                  -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
                    HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                        ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c))
                        (ContinuousLinearMap.id ℝ F))).smulRight
              (_root_.id (c + x) - c) :
          (a : F) → F)
        y :
      F)
    ((HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist ((fun (x : F) ↦ c + x) x) c) 2)
            (↑(↑(Submodule.reflection (ℝ ∙ ((fun (x : F) ↦ c + x) x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F) :
          (a : F) → F)
        y :
      F)
Tactic: refine this.congr_fderiv (LinearMap.ext_on_codisjoint
    (Submodule.isCompl_orthogonal_of_hasOrthogonalProjection (K := ℝ ∙ x)).codisjoint
    (LinearMap.eqOn_span' ?_) fun y hy ↦ ?_)