-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereoInvFun_ne_north_pole (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) :
    stereoInvFun hv w ≠ (⟨v, by simp [hv]⟩ : sphere (0 : E) 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ stereoInvFun hv w ≠ ⟨v, ⋯⟩

Tactic:
refine Subtype.coe_ne_coe.1 ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ ↑(stereoInvFun hv w) ≠ ↑⟨v, ⋯⟩

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
hw : ⟪v, ↑w⟫_ℝ = 0
⊢ (‖↑w‖ ^ 2 + 4)⁻¹ * (‖↑w‖ ^ 2 - 4) < 1

Tactic:
rw [inv_mul_lt_iff₀']

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
hw : ⟪v, ↑w⟫_ℝ = 0
⊢ ‖↑w‖ ^ 2 - 4 < 1 * (‖↑w‖ ^ 2 + 4)

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
hw : ⟪v, ↑w⟫_ℝ = 0
⊢ 0 < ‖↑w‖ ^ 2 + 4

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
hw : ⟪v, ↑w⟫_ℝ = 0
⊢ 0 < ‖↑w‖ ^ 2 + 4

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
hw : ⟪v, ↑w⟫_ℝ = 0
⊢ ‖↑w‖ ^ 2 - 4 < 1 * (‖↑w‖ ^ 2 + 4)

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ ↑(stereoInvFun hv w) ≠ ↑⟨v, ⋯⟩

Tactic:
rw [← inner_lt_one_iff_real_of_norm_one _ hv]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ ⟪↑(stereoInvFun hv w), v⟫_ℝ < 1

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ ‖↑(stereoInvFun hv w)‖ = 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ ‖↑(stereoInvFun hv w)‖ = 1

Tactic:
simpa using stereoInvFunAux_mem hv w.2

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ ⟪↑(stereoInvFun hv w), v⟫_ℝ < 1

Tactic:
have hw : ⟪v, w⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
hw : ⟪v, ↑w⟫_ℝ = 0
⊢ ⟪↑(stereoInvFun hv w), v⟫_ℝ < 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
hw : ⟪v, ↑w⟫_ℝ = 0
hw' : (‖↑w‖ ^ 2 + 4)⁻¹ * (‖↑w‖ ^ 2 - 4) < 1
⊢ ⟪↑(stereoInvFun hv w), v⟫_ℝ < 1

Tactic:
simpa [real_inner_comm, inner_add_right, inner_smul_right, real_inner_self_eq_norm_mul_norm, hw,
  hv] using hw'

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ v ∈ sphere 0 1

Tactic:
simp [hv]

Result:
no goals