[GOAL]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
s : Set E
a : E
n : ℕ∞
hc : DifferentiableAt ℝ c a
hR : DifferentiableAt ℝ R a
hx : DifferentiableAt ℝ x a
hne : x a ≠ c a
⊢ DifferentiableAt ℝ (fun a => inversion (c a) (R a) (x a)) a
[PROOFSTEP]
rw [← differentiableWithinAt_univ] at *
[GOAL]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
s : Set E
a : E
n : ℕ∞
hc : DifferentiableWithinAt ℝ c univ a
hR : DifferentiableWithinAt ℝ R univ a
hx : DifferentiableWithinAt ℝ x univ a
hne : x a ≠ c a
⊢ DifferentiableWithinAt ℝ (fun a => inversion (c a) (R a) (x a)) univ a
[PROOFSTEP]
exact hc.inversion hR hx hne
[GOAL]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d x y z : F
r R : ℝ
hx : x ≠ c
⊢ HasFDerivAt (inversion c R)
    ((R / dist x c) ^ 2 • ↑(ContinuousLinearEquiv.mk (reflection (Submodule.span ℝ {x - c})ᗮ).toLinearEquiv)) x
[PROOFSTEP]
rcases add_left_surjective c x with ⟨x, rfl⟩
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
⊢ HasFDerivAt (inversion c R)
    ((R / dist ((fun x x_1 => x + x_1) c x) c) ^ 2 •
      ↑(ContinuousLinearEquiv.mk (reflection (Submodule.span ℝ {(fun x x_1 => x + x_1) c x - c})ᗮ).toLinearEquiv))
    ((fun x x_1 => x + x_1) c x)
[PROOFSTEP]
have : HasFDerivAt (inversion c R) (_ : F →L[ℝ] F) (c + x)
[GOAL]
case this
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
⊢ HasFDerivAt (inversion c R) ?m.24683 (c + x)
[PROOFSTEP]
simp_rw [inversion, dist_eq_norm, div_pow, div_eq_mul_inv]
[GOAL]
case this
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
⊢ HasFDerivAt (fun x => (R ^ 2 * (‖x - c‖ ^ 2)⁻¹) • (x -ᵥ c) +ᵥ c) ?m.24683 (c + x)
[PROOFSTEP]
have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c
[GOAL]
case this
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c 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) ?m.24683 (c + x)
[PROOFSTEP]
have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul (R ^ 2)
[GOAL]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
A : HasFDerivAt (fun x => _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ ‖_root_.id (c + x) - c‖ ^ 2 ≠ 0
[PROOFSTEP]
simpa using hx
[GOAL]
case this
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c 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 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
    (c + x)
⊢ HasFDerivAt (fun x => (R ^ 2 * (‖x - c‖ ^ 2)⁻¹) • (x -ᵥ c) +ᵥ c) ?m.24683 (c + x)
[PROOFSTEP]
exact (B.smul A).add_const c
[GOAL]
case intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      ContinuousLinearMap.smulRight
        (R ^ 2 •
          -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
            2 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
        (_root_.id (c + x) - c))
    (c + x)
⊢ HasFDerivAt (inversion c R)
    ((R / dist ((fun x x_1 => x + x_1) c x) c) ^ 2 •
      ↑(ContinuousLinearEquiv.mk (reflection (Submodule.span ℝ {(fun x x_1 => x + x_1) c x - c})ᗮ).toLinearEquiv))
    ((fun x x_1 => x + x_1) c x)
[PROOFSTEP]
refine
  this.congr_fderiv
    (LinearMap.ext_on_codisjoint (Submodule.isCompl_orthogonal_of_completeSpace (K := ℝ ∙ x)).codisjoint
      (LinearMap.eqOn_span' ?_) fun y hy ↦ ?_)
[GOAL]
case intro.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      ContinuousLinearMap.smulRight
        (R ^ 2 •
          -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
            2 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
        (_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 +
        ContinuousLinearMap.smulRight
          (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
          (_root_.id (c + x) - c))
    ↑((R / dist ((fun x x_1 => x + x_1) c x) c) ^ 2 •
        ↑(ContinuousLinearEquiv.mk (reflection (Submodule.span ℝ {(fun x x_1 => x + x_1) c x - c})ᗮ).toLinearEquiv))
    {x}
[PROOFSTEP]
have : ((‖x‖ ^ 2) ^ 2)⁻¹ * (‖x‖ ^ 2) = (‖x‖ ^ 2)⁻¹
[GOAL]
case this
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      ContinuousLinearMap.smulRight
        (R ^ 2 •
          -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
            2 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
        (_root_.id (c + x) - c))
    (c + x)
⊢ ((‖x‖ ^ 2) ^ 2)⁻¹ * ‖x‖ ^ 2 = (‖x‖ ^ 2)⁻¹
[PROOFSTEP]
rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']
[GOAL]
case intro.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
this✝ :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      ContinuousLinearMap.smulRight
        (R ^ 2 •
          -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
            2 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
        (_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 +
        ContinuousLinearMap.smulRight
          (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
          (_root_.id (c + x) - c))
    ↑((R / dist ((fun x x_1 => x + x_1) c x) c) ^ 2 •
        ↑(ContinuousLinearEquiv.mk (reflection (Submodule.span ℝ {(fun x x_1 => x + x_1) c x - c})ᗮ).toLinearEquiv))
    {x}
[PROOFSTEP]
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]
[GOAL]
case intro.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
a b c d y✝ z : F
r R : ℝ
x : F
hx : (fun x x_1 => x + x_1) c x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      ContinuousLinearMap.smulRight
        (R ^ 2 •
          -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
            2 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
        (_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 +
          ContinuousLinearMap.smulRight
            (R ^ 2 •
              -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
                2 • ContinuousLinearMap.comp (↑(innerSL ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))
            (_root_.id (c + x) - c))
      y =
    ↑((R / dist ((fun x x_1 => x + x_1) c x) c) ^ 2 •
          ↑(ContinuousLinearEquiv.mk (reflection (Submodule.span ℝ {(fun x x_1 => x + x_1) c x - c})ᗮ).toLinearEquiv))
      y
[PROOFSTEP]
simp [Submodule.mem_orthogonal_singleton_iff_inner_right.1 hy, reflection_mem_subspace_eq_self hy, div_eq_mul_inv,
  mul_pow]
