awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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)
⊢ (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)
have split : (↑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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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)
⊢ (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)
have hvy : ⟪v, (↑y : E)⟫_ℝ = 0
Tactic: have hvy : ⟪v, y⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp y.2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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
have hvy' : ⟪a • v, (↑y : E)⟫_ℝ = 0
Tactic: have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp only [inner_smul_left, hvy, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
have h : 1 = ‖a • v + (↑y : E)‖ * ‖a • v + (↑y : E)‖
Tactic: convert! norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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)‖
⊢ 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
have h₁ : HPow.hPow (β := ℕ) a 2 = ‖a • v‖ * ‖a • v‖
Tactic: convert! norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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‖
⊢ 1 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) ‖y‖ 2
have h₂ : HPow.hPow (β := ℕ) ‖y‖ 2 = ‖(↑y : E)‖ * ‖(↑y : E)‖
Tactic: convert! norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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
⊢ (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)
have pythag : 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 _
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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
have this : a < 1
Tactic: have : a < 1 := (inner_lt_one_iff_real_of_norm_eq_one hv (by simp)).mpr hx.symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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
⊢ 0 < 1 - a
have linarith : 1 - a ≤ 0 → a - 1 + (1 - a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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
⊢ (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)
have ha : 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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 / (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)
have 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)
Tactic: rw [split, Submodule.coe_smul_of_tower]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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 / (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)
have 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)
Tactic: simp only [norm_smul, norm_div, Real.norm_eq_abs, abs_of_nonneg ha.le]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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| / (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)
have match_scalars : (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ * (4 * (2 / (1 - a) * 1)) = 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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
⊢ (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)
have match_scalars₁ : (HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 + 4)⁻¹ * ((HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 - 4) * 1) = a * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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| / (1 - a) * ‖y‖) 2 + 4)⁻¹ * (4 * (2 / (1 - a) * 1)) = 1
have field_simp : (1 - a) * 4 * 2 = HPow.hPow (α := ℝ) (β := ℕ) |2| 2 * HPow.hPow (β := ℕ) ‖y‖ 2 + HPow.hPow (β := ℕ) (1 - a) 2 * 4
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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| / (1 - a) * ‖y‖) 2 + 4)⁻¹ * ((HPow.hPow (β := ℕ) (|2| / (1 - a) * ‖y‖) 2 - 4) * 1) = a * 1
have 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)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ stereoToFun v (↑(stereoInvFun hv w) : E) = w
have 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
Tactic: simp only [stereoToFun, stereoInvFun, stereoInvFunAux, smul_add, map_add, map_smul,
    innerSL_apply_apply, Submodule.orthogonalProjection_mem_subspace_eq_self]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ (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
have h₁ : 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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)ᗮ)
⊢ (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
have h₂ : ⟪v, (↑w : E)⟫ = 0
Tactic: have h₂ : ⟪v, w⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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
⊢ (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
have h₃ : ⟪v, v⟫ = 1
Tactic: have h₃ : ⟪v, v⟫ = 1 := by simp [hv]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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 /
          (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
have 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
Tactic: rw [h₁, h₂, h₃]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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 /
          (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
have 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
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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 /
        (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
have simp : 2 = HAdd.hAdd (α := ℝ) 1 1
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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 :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h : (↑x : E) = v
⊢ Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯} x
have hv₁ : ‖(↑x : E)‖ = 1
Tactic: rw [← h] at hv
Cleared hypotheses: hx, h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv_1 : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hv : ‖(↑x : E)‖ = 1
hx :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h : (↑x : E) = v
⊢ Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯} x
have a : (↑x : E) = (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v sorry) : E)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : (↑(sphere 0 1) : Type u_1)
h :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ w
⊢ Membership.mem (γ := Set E)
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} (↑w : E)
have dsimp : ¬⟪v, (↑w : E)⟫ = 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : (↑(sphere 0 1) : Type u_1)
⊢ Eq (α := ↥(ℝ ∙ (↑(-v) : E))ᗮ) ((↑(stereographic ⋯) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) v) 0
have h : v = - -v
Tactic: convert! stereographic_apply_neg (-v)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : (↑(sphere 0 1) : Type u_1)
⊢ v = - -v
have h : (↑v : E) = (↑(- -v) : E)
Tactic: ext1