-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem contDiff_stereoInvFunAux {m : WithTop ℕ∞} : ContDiff ℝ m (stereoInvFunAux v)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
x : E
⊢ ‖x‖ ^ 2 + 4 ≠ 0

Tactic:
nlinarith

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w => (‖w‖ ^ 2 + 4)⁻¹
⊢ ContDiff ℝ ω fun w => 4 • w + (‖w‖ ^ 2 - 4) • v

Tactic:
refine (contDiff_const.smul contDiff_id).add ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w => (‖w‖ ^ 2 + 4)⁻¹
⊢ ContDiff ℝ ω fun w => (‖w‖ ^ 2 - 4) • v

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w => (‖w‖ ^ 2 + 4)⁻¹
⊢ ContDiff ℝ ω fun w => (‖w‖ ^ 2 - 4) • v

Tactic:
exact (h₀.sub contDiff_const).smul contDiff_const

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w => (‖w‖ ^ 2 + 4)⁻¹
h₂ : ContDiff ℝ ω fun w => 4 • w + (‖w‖ ^ 2 - 4) • v
⊢ ContDiff ℝ m (stereoInvFunAux v)

Tactic:
exact (h₁.smul h₂).of_le le_top

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w => (‖w‖ ^ 2 + 4)⁻¹
⊢ ContDiff ℝ m (stereoInvFunAux v)

Tactic:
have h₂ : ContDiff ℝ ω fun w => (4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v := by
  refine (contDiff_const.smul contDiff_id).add ?_
  exact (h₀.sub contDiff_const).smul contDiff_const

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w => (‖w‖ ^ 2 + 4)⁻¹
h₂ : ContDiff ℝ ω fun w => 4 • w + (‖w‖ ^ 2 - 4) • v
⊢ ContDiff ℝ m (stereoInvFunAux v)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
⊢ ContDiff ℝ ω fun w => (‖w‖ ^ 2 + 4)⁻¹

Tactic:
refine (h₀.add contDiff_const).inv ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
⊢ ∀ (x : E), ‖x‖ ^ 2 + 4 ≠ 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
⊢ ContDiff ℝ m (stereoInvFunAux v)

Tactic:
have h₀ : ContDiff ℝ ω fun w : E => ‖w‖ ^ 2 := contDiff_norm_sq ℝ

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
⊢ ContDiff ℝ m (stereoInvFunAux v)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
⊢ ∀ (x : E), ‖x‖ ^ 2 + 4 ≠ 0

Tactic:
intro x

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
x : E
⊢ ‖x‖ ^ 2 + 4 ≠ 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
⊢ ContDiff ℝ m (stereoInvFunAux v)

Tactic:
have h₁ : ContDiff ℝ ω fun w : E => (‖w‖ ^ 2 + 4)⁻¹ := by
  refine (h₀.add contDiff_const).inv ?_
  intro x
  nlinarith

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : WithTop ℕ∞
h₀ : ContDiff ℝ ω fun w => ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w => (‖w‖ ^ 2 + 4)⁻¹
⊢ ContDiff ℝ m (stereoInvFunAux v)