-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem hasFDerivAt_stereoInvFunAux (v : E) :
    HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
h₂ : HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0
⊢ ContinuousLinearMap.id ℝ E =
    (‖0‖ ^ 2 + 4)⁻¹ • 4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (4 • 0 + (‖0‖ ^ 2 - 4) • v)

Tactic:
ext w

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
h₂ : HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0
w : E
⊢ (ContinuousLinearMap.id ℝ E) w =
    ((‖0‖ ^ 2 + 4)⁻¹ • 4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (4 • 0 + (‖0‖ ^ 2 - 4) • v)) w

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
h₂ : HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Tactic:
convert h₁.smul h₂ using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
h₂ : HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0
⊢ ContinuousLinearMap.id ℝ E =
    (‖0‖ ^ 2 + 4)⁻¹ • 4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (4 • 0 + (‖0‖ ^ 2 - 4) • v)

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ 0 = 2 • (innerSL ℝ) 0

Tactic:
simp only [map_zero, smul_zero]

Result:
no goals

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
w : E
⊢ (4 • ContinuousLinearMap.id ℝ E) w =
    (4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (id 0) +
        ((‖0‖ ^ 2 - 4) • 0 + (0 - 0).smulRight v))
      w

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
⊢ HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0

Tactic:
convert (hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0)) <;> simp

Result:
no goals

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
⊢ 4 • ContinuousLinearMap.id ℝ E =
    4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (id 0) + ((‖0‖ ^ 2 - 4) • 0 + (0 - 0).smulRight v)

Tactic:
ext w

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
w : E
⊢ (4 • ContinuousLinearMap.id ℝ E) w =
    (4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (id 0) +
        ((‖0‖ ^ 2 - 4) • 0 + (0 - 0).smulRight v))
      w

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
⊢ HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0

Tactic:
convert ((hasFDerivAt_const (4 : ℝ) 0).smul (hasFDerivAt_id 0)).add
  ((h₀.sub (hasFDerivAt_const (4 : ℝ) 0)).smul (hasFDerivAt_const v 0)) using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
⊢ 4 • ContinuousLinearMap.id ℝ E =
    4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (id 0) + ((‖0‖ ^ 2 - 4) • 0 + (0 - 0).smulRight v)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Tactic:
have h₀ : HasFDerivAt (fun w : E => ‖w‖ ^ 2) (0 : E →L[ℝ] ℝ) 0 := by
  convert (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt
  simp only [map_zero, smul_zero]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Tactic:
have h₂ : HasFDerivAt (fun w => (4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v)
    ((4 : ℝ) • ContinuousLinearMap.id ℝ E) 0 := by
  convert ((hasFDerivAt_const (4 : ℝ) 0).smul (hasFDerivAt_id 0)).add
    ((h₀.sub (hasFDerivAt_const (4 : ℝ) 0)).smul (hasFDerivAt_const v 0)) using 1
  ext w
  simp

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
h₂ : HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
h₂ : HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0
w : E
⊢ (ContinuousLinearMap.id ℝ E) w =
    ((‖0‖ ^ 2 + 4)⁻¹ • 4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (4 • 0 + (‖0‖ ^ 2 - 4) • v)) w

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Tactic:
have h₁ : HasFDerivAt (fun w : E => (‖w‖ ^ 2 + 4)⁻¹) (0 : E →L[ℝ] ℝ) 0 := by
  convert (hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0)) <;> simp

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0

Tactic:
convert (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ 0 = 2 • (innerSL ℝ) 0