-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereo_left_inv (hv : ‖v‖ = 1) {x : sphere (0 : E) 1} (hx : (x : E) ≠ v) :
    stereoInvFun hv (stereoToFun v x) = x

Proof state:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    ↑x

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

Result:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    ↑x

Proof state:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • (2 / (1 - a)) • ↑y +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    a • v + ↑y

Tactic:
simp only [norm_smul, norm_div, RCLike.norm_ofNat, Real.norm_eq_abs, abs_of_nonneg ha.le]

Result:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ ((2 / (1 - a) * ‖y‖) ^ 2 + 4)⁻¹ • 4 • (2 / (1 - a)) • ↑y +
      ((2 / (1 - a) * ‖y‖) ^ 2 + 4)⁻¹ • ((2 / (1 - a) * ‖y‖) ^ 2 - 4) • v =
    a • v + ↑y

Proof state:
case h.e'_3.h.e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
hvy' : ⟪a • v, ↑y⟫_ℝ = 0
⊢ a ^ 2 = ‖a • v‖ * ‖a • v‖

Tactic:
simp [norm_smul, hv, ← sq, sq_abs]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
this : a < 1
⊢ 0 < 1 - a

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
⊢ ⟪a • v, ↑y⟫_ℝ = 0

Tactic:
simp only [inner_smul_left, hvy, mul_zero]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ (1 - a) ^ 2 * (4 * 2) = ((2 * ‖y‖) ^ 2 + 4 * (1 - a) ^ 2) * (1 - a)

Tactic:
linear_combination 4 * (1 - a) * pythag

Result:
no goals

Proof state:
case h.e'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
hvy' : ⟪a • v, ↑y⟫_ℝ = 0
⊢ 1 = ‖a • v + ↑y‖ * ‖a • v + ↑y‖

Tactic:
simp [← split]

Result:
no goals

Proof state:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • ↑((2 / (1 - a)) • y) +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    ↑x

Tactic:
rw [split, Submodule.coe_smul_of_tower]

Result:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • (2 / (1 - a)) • ↑y +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    a • v + ↑y

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
⊢ ‖↑x‖ = 1

Tactic:
simp

Result:
no goals

Proof state:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
⊢ ↑(stereoInvFun hv (stereoToFun v ↑x)) = ↑x

Tactic:
simp only [stereoToFun_apply, stereoInvFun_apply, smul_add]

Result:
case a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
⊢ (‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x‖ ^ 2 + 4)⁻¹ •
        4 • ↑((2 / (1 - ((innerSL ℝ) v) ↑x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x) +
      (‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x‖ ^ 2 + 4)⁻¹ •
        (‖(2 / (1 - ((innerSL ℝ) v) ↑x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x‖ ^ 2 - 4) • v =
    ↑x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
hvy' : ⟪a • v, ↑y⟫_ℝ = 0
⊢ 1 = a ^ 2 + ‖y‖ ^ 2

Tactic:
convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2

Result:
case h.e'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
hvy' : ⟪a • v, ↑y⟫_ℝ = 0
⊢ 1 = ‖a • v + ↑y‖ * ‖a • v + ↑y‖

case h.e'_3.h.e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
hvy' : ⟪a • v, ↑y⟫_ℝ = 0
⊢ a ^ 2 = ‖a • v‖ * ‖a • v‖

case h.e'_3.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(Submodule.span ℝ {v})ᗮ := (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
hvy' : ⟪a • v, ↑y⟫_ℝ = 0
⊢ ‖y‖ ^ 2 = ‖↑y‖ * ‖↑y‖