awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
rw :
  HAdd.hAdd (β := E) (⟪v, (↑x : E)⟫_ℝ • v) ((Submodule.starProjection (ℝ ∙ v)ᗮ : (a : E) → E) (↑x : E) : E) =
    a • v + (↑y : E)
⊢ (↑x : E) = a • v + (↑y : E)

Tactic:
rw [← ((ℝ ∙ v).starProjection_add_starProjection_orthogonal x),
      Submodule.starProjection_unit_singleton ℝ hv x]

Premises used: Real, Submodule.starProjection_add_starProjection_orthogonal, Submodule.starProjection_unit_singleton, Subtype.val
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
⊢ HAdd.hAdd (β := E) (⟪v, (↑x : E)⟫_ℝ • v) ((Submodule.starProjection (ℝ ∙ v)ᗮ : (a : E) → E) (↑x : E) : E) =
    a • v + (↑y : E)

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
⊢ (↑x : E) = a • v + (↑y : E)

Tactic:
have split : ↑x = a • v + ↑y := by
    rw [← ((ℝ ∙ v).starProjection_add_starProjection_orthogonal x),
      Submodule.starProjection_unit_singleton ℝ hv x]
    rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
⊢ ⟪v, (↑y : E)⟫_ℝ = 0

Tactic:
have hvy : ⟪v, y⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp y.2
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
⊢ ⟪a • v, (↑y : E)⟫_ℝ = 0

Tactic:
simp only [inner_smul_left, hvy, mul_zero]

Premises used: MulZeroClass.mul_zero, inner_smul_left
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
⊢ ⟪a • v, (↑y : E)⟫_ℝ = 0

Tactic:
have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp only [inner_smul_left, hvy, mul_zero]
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
hvy' : ⟪a • v, (↑y : E)⟫_ℝ = 0
⊢ ‖a • v + (↑y : E)‖ * ‖a • v + (↑y : E)‖ = ‖a • v‖ * ‖a • v‖ + ‖(↑y : E)‖ * ‖(↑y : E)‖

Tactic:
norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy'

Premises used: norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
hvy' : ⟪a • v, (↑y : E)⟫_ℝ = 0
h : 1 = ‖a • v + (↑y : E)‖ * ‖a • v + (↑y : E)‖
h₁ : HPow.hPow (β := ℕ) a 2 = ‖a • v‖ * ‖a • v‖
h₂ : HPow.hPow (β := ℕ) ‖y‖ 2 = ‖(↑y : E)‖ * ‖(↑y : E)‖
⊢ 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
convert! norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2

Premises used: norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
hvy' : ⟪a • v, (↑y : E)⟫_ℝ = 0
⊢ 1 = ‖a • v + (↑y : E)‖ * ‖a • v + (↑y : E)‖

Tactic:
simp [← split]
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
hvy' : ⟪a • v, (↑y : E)⟫_ℝ = 0
⊢ HPow.hPow (β := ℕ) a 2 = ‖a • v‖ * ‖a • v‖

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

Premises used: norm_smul, sq, sq_abs
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
hvy' : ⟪a • v, (↑y : E)⟫_ℝ = 0
⊢ HPow.hPow (β := ℕ) ‖y‖ 2 = ‖(↑y : E)‖ * ‖(↑y : E)‖

Tactic:
sq _

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, setOf, sq, Classical.choose
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
hvy' : ⟪a • v, (↑y : E)⟫_ℝ = 0
⊢ HPow.hPow (β := ℕ) ‖y‖ 2 = ‖(↑y : E)‖ * ‖(↑y : E)‖

Tactic:
exact sq _

Premises used: sq
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
⊢ 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
have pythag : 1 = a ^ 2 + ‖y‖ ^ 2 := by
    have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp only [inner_smul_left, hvy, mul_zero]
    convert! norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2
    · simp [← split]
    · simp [norm_smul, hv, ← sq, sq_abs]
    · exact sq _
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
⊢ ‖(↑x : E)‖ = 1

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
⊢ a < 1

Tactic:
have : a < 1 := (inner_lt_one_iff_real_of_norm_eq_one hv (by simp)).mpr hx.symm
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
this : a < 1
linarith : 1 - a ≤ 0 → a - 1 + (1 - a - 0) = 0
⊢ 0 < 1 - a

Tactic:
linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
⊢ 0 < 1 - a

Tactic:
have ha : 0 < 1 - a := by
    have : a < 1 := (inner_lt_one_iff_real_of_norm_eq_one hv (by simp)).mpr hx.symm
    linarith
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 < 1 - a
a₁ :
  (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 ((2 / (1 - a)) • (↑y : E)) +
      (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 - 4) • v =
    a • v + (↑y : E)
⊢ (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 (↑((2 / (1 - a)) • y) : E) +
      (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 - 4) • v =
    (↑x : E)

Tactic:
rw [split, Submodule.coe_smul_of_tower]

Premises used: Submodule.coe_smul_of_tower
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 < 1 - a
a₁ :
  (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 ((2 / (1 - a)) • (↑y : E)) +
      (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 - 4) • v =
    a • v + (↑y : E)
⊢ (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 ((2 / (1 - a)) • (↑y : E)) +
      (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) ‖(2 / (1 - a)) • y‖ 2 - 4) • v =
    a • v + (↑y : E)

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

Premises used: norm_smul, LT.lt.le, norm_div, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 < 1 - a
match_scalars : (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ * (4 * (2 / (1 - a) * 1)) = 1
match_scalars₁ :
  (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ * ((HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 - 4) * 1) = a * 1
⊢ (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 ((2 / (1 - a)) • (↑y : E)) +
      (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 - 4) • v =
    a • v + (↑y : E)

Tactic:
match_scalars
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 < 1 - a
field_simp :
  (1 - a) * 4 * 2 = HPow.hPow (α := ℝ) (β := ℕ) |2| 2 * HPow.hPow (β := ℕ) ‖y‖ 2 + HPow.hPow (β := ℕ) (1 - a) 2 * 4
⊢ (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ * (4 * (2 / (1 - a) * 1)) = 1

Tactic:
field_simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 < 1 - a
⊢ (1 - a) * 4 * 2 = HPow.hPow (α := ℝ) (β := ℕ) |2| 2 * HPow.hPow (β := ℕ) ‖y‖ 2 + HPow.hPow (β := ℕ) (1 - a) 2 * 4

Tactic:
linear_combination 4 * pythag
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 < 1 - a
field_simp :
  HPow.hPow (α := ℝ) (β := ℕ) |2| 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (1 - a) 2 * 4 =
    a * (HPow.hPow (α := ℝ) (β := ℕ) |2| 2 * HPow.hPow (β := ℕ) ‖y‖ 2 + HPow.hPow (β := ℕ) (1 - a) 2 * 4)
⊢ (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ * ((HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 - 4) * 1) = a * 1

Tactic:
field_simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E)
y : ↥(ℝ ∙ v)ᗮ := (Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E)
split : (↑x : E) = a • v + (↑y : E)
hvy : ⟪v, (↑y : E)⟫_ℝ = 0
pythag : 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 < 1 - a
⊢ HPow.hPow (α := ℝ) (β := ℕ) |2| 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) (1 - a) 2 * 4 =
    a * (HPow.hPow (α := ℝ) (β := ℕ) |2| 2 * HPow.hPow (β := ℕ) ‖y‖ 2 + HPow.hPow (β := ℕ) (1 - a) 2 * 4)

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

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
simp :
  (2 /
          (1 -
            ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 ⟪v, (↑w : E)⟫ +
              (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) • ⟪v, v⟫))) •
        (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 w +
      (2 /
          (1 -
            ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 ⟪v, (↑w : E)⟫ +
              (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) • ⟪v, v⟫))) •
        (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ •
          HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4)
            ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) =
    w
⊢ stereoToFun v (↑(stereoInvFun hv w) : E) = w

Tactic:
simp only [stereoToFun, stereoInvFun, stereoInvFunAux, smul_add, map_add, map_smul,
    innerSL_apply_apply, Submodule.orthogonalProjection_mem_subspace_eq_self]

Premises used: innerSL_apply_apply, Submodule.orthogonalProjection_mem_subspace_eq_self, stereoInvFun, map_add, stereoInvFunAux, stereoToFun, smul_add, map_smul
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ Eq (α := ↥(ℝ ∙ v)ᗮ) ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) (0 : ↥(ℝ ∙ v)ᗮ)

Tactic:
have h₁ : (ℝ ∙ v)ᗮ.orthogonalProjection v = 0 :=
    Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero v
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : Eq (α := ↥(ℝ ∙ v)ᗮ) ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) (0 : ↥(ℝ ∙ v)ᗮ)
⊢ ⟪v, (↑w : E)⟫ = 0

Tactic:
have h₂ : ⟪v, w⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : Eq (α := ↥(ℝ ∙ v)ᗮ) ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) (0 : ↥(ℝ ∙ v)ᗮ)
h₂ : ⟪v, (↑w : E)⟫ = 0
⊢ ⟪v, v⟫ = 1

Tactic:
simp [hv]
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : Eq (α := ↥(ℝ ∙ v)ᗮ) ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) (0 : ↥(ℝ ∙ v)ᗮ)
h₂ : ⟪v, (↑w : E)⟫ = 0
⊢ ⟪v, v⟫ = 1

Tactic:
have h₃ : ⟪v, v⟫ = 1 := by simp [hv]
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : Eq (α := ↥(ℝ ∙ v)ᗮ) ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) (0 : ↥(ℝ ∙ v)ᗮ)
h₂ : ⟪v, (↑w : E)⟫ = 0
h₃ : ⟪v, v⟫ = 1
rw :
  (2 /
          (1 -
            ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) (β := ℝ) 4 0 +
              (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ •
                HSMul.hSMul (β := ℝ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) 1))) •
        (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 w +
      (2 /
          (1 -
            ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) (β := ℝ) 4 0 +
              (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ •
                HSMul.hSMul (β := ℝ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) 1))) •
        (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) 0 =
    w
⊢ (2 /
          (1 -
            ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 ⟪v, (↑w : E)⟫ +
              (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) • ⟪v, v⟫))) •
        (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 w +
      (2 /
          (1 -
            ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 ⟪v, (↑w : E)⟫ +
              (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) • ⟪v, v⟫))) •
        (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ •
          HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4)
            ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) =
    w

Tactic:
rw [h₁, h₂, h₃]
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : Eq (α := ↥(ℝ ∙ v)ᗮ) ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) (0 : ↥(ℝ ∙ v)ᗮ)
h₂ : ⟪v, (↑w : E)⟫ = 0
h₃ : ⟪v, v⟫ = 1
match_scalars :
  2 /
        (1 -
          ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) (β := ℝ) 4 0 +
            (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (β := ℝ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) 1)) *
      ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ * HMul.hMul (α := ℝ) 4 1) =
    1
⊢ (2 /
          (1 -
            ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) (β := ℝ) 4 0 +
              (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ •
                HSMul.hSMul (β := ℝ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) 1))) •
        (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) 4 w +
      (2 /
          (1 -
            ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) (β := ℝ) 4 0 +
              (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ •
                HSMul.hSMul (β := ℝ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) 1))) •
        (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) 0 =
    w

Tactic:
match_scalars
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : Eq (α := ↥(ℝ ∙ v)ᗮ) ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) (0 : ↥(ℝ ∙ v)ᗮ)
h₂ : ⟪v, (↑w : E)⟫ = 0
h₃ : ⟪v, v⟫ = 1
simp : 2 = HAdd.hAdd (α := ℝ) 1 1
⊢ 2 /
        (1 -
          ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (α := ℝ) (β := ℝ) 4 0 +
            (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ • HSMul.hSMul (β := ℝ) (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) 1)) *
      ((HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ * HMul.hMul (α := ℝ) 4 1) =
    1

Tactic:
simp [field]
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : Eq (α := ↥(ℝ ∙ v)ᗮ) ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) v : ↥(ℝ ∙ v)ᗮ) (0 : ↥(ℝ ∙ v)ᗮ)
h₂ : ⟪v, (↑w : E)⟫ = 0
h₃ : ⟪v, v⟫ = 1
⊢ 2 = HAdd.hAdd (α := ℝ) 1 1

Tactic:
ring
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
⊢ Membership.mem (γ := Set E) (sphere 0 1) v

Tactic:
simp [hv]