-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereo_right_inv (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) : stereoToFun v (stereoInvFun hv w) = w

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

Tactic:
simp only [stereoToFun, stereoInvFun, stereoInvFunAux, smul_add, map_add, map_smul, innerSL_apply,
  orthogonalProjection_mem_subspace_eq_self]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v =
    w

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
h₃ : inner v v = 1
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v =
    w

Tactic:
rw [h₁, h₂, h₃]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
h₃ : inner v v = 1
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 0 =
    w

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v =
    w

Tactic:
have h₂ : inner 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})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v =
    w

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
h₃ : inner v v = 1
⊢ 2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1)) * ((‖↑w‖ ^ 2 + 4)⁻¹ * (4 * 1)) = 1

Tactic:
simp (disch := field_simp_discharge) only [add_div', add_sub_sub_cancel, div_div,
  div_div_eq_mul_div, div_eq_iff, div_mul_eq_mul_div, inv_eq_one_div,
  mul_div_assoc', mul_one, mul_zero, one_mul, smul_eq_mul, sub_div', zero_add, zero_div, zero_mul]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
h₃ : inner v v = 1
⊢ 2 * (‖↑w‖ ^ 2 + 4) * 4 = (4 + 4) * (‖↑w‖ ^ 2 + 4)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
h₃ : inner v v = 1
⊢ 2 * (‖↑w‖ ^ 2 + 4) * 4 = (4 + 4) * (‖↑w‖ ^ 2 + 4)

Tactic:
ring

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v =
    w

Tactic:
have h₁ : orthogonalProjection (ℝ ∙ v)ᗮ v = 0 :=
  orthogonalProjection_orthogonalComplement_singleton_eq_zero v

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v =
    w

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
h₃ : inner v v = 1
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 0 =
    w

Tactic:
match_scalars

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
h₃ : inner v v = 1
⊢ 2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1)) * ((‖↑w‖ ^ 2 + 4)⁻¹ * (4 * 1)) = 1

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

Tactic:
simp [real_inner_self_eq_norm_mul_norm, hv]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v =
    w

Tactic:
have h₃ : inner v v = (1 : ℝ) := by simp [real_inner_self_eq_norm_mul_norm, hv]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(Submodule.span ℝ {v})ᗮ
h₁ : (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v = 0
h₂ : inner v ↑w = 0
h₃ : inner v v = 1
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • inner v ↑w + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • inner v v))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) v =
    w