awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ∞ω
refine_1 :
  ContDiffOn ℝ (F := ℝ) n
    (fun (i : E) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) i : ℝ))
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
⊢ ContDiffOn ℝ (F := ℝ) n
    (fun (i : E) ↦
      2 / HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) i : ℝ))
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
have refine_2 : ∀ (x : E),
  Membership.mem (γ := Set E)
      {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} x →
    HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) ≠ 0
Tactic: refine contDiff_const.contDiffOn.div ?_ ?_
-- 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 : E
hw : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ w
⊢ Membership.mem (γ := Set E) (sphere 0 1) (stereoInvFunAux v w)
have h₁ : 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4
Tactic: have h₁ : (0 : ℝ) < ‖w‖ ^ 2 + 4 := by positivity
-- 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 : E
hw : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ w
h₁ : 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4
⊢ Membership.mem (γ := Set E) (sphere 0 1) (stereoInvFunAux v w)
have suffices : ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ = HPow.hPow (β := ℕ) ‖w‖ 2 + 4
Tactic: suffices ‖(4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v‖ = ‖w‖ ^ 2 + 4 by
    simp only [mem_sphere_zero_iff_norm, norm_smul, Real.norm_eq_abs, abs_inv, this,
      abs_of_pos h₁, stereoInvFunAux_apply, inv_mul_cancel₀ h₁.ne']
-- 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 : E
hw : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ w
h₁ : 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4
⊢ ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ = HPow.hPow (β := ℕ) ‖w‖ 2 + 4
have suffices : HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ 2 =
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖w‖ 2 + 4) 2
Tactic: suffices ‖(4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v‖ ^ 2 = (‖w‖ ^ 2 + 4) ^ 2 by
    simpa only [sq_eq_sq_iff_abs_eq_abs, abs_norm, abs_of_pos h₁] using this
-- 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 : E
hw : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ w
h₁ : 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4
⊢ HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖w‖ 2 + 4) 2
have hw₁ : ⟪w, v⟫ = 0
Tactic: rw [Submodule.mem_orthogonal_singleton_iff_inner_left] at hw
Cleared hypotheses: hw, 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 : E
hw : ⟪w, v⟫ = 0
h₁ : 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4
⊢ HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖w‖ 2 + 4) 2
have simp : HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ‖w‖ 2 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) 2 =
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖w‖ 2 + 4) 2
Tactic: simp [norm_add_sq_real, norm_smul, inner_smul_left, inner_smul_right, hw, mul_pow,
    Real.norm_eq_abs, 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
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
have h : 0 = HSMul.hSMul (α := ℕ) (β := E →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) 0 : E →L[ℝ] ℝ)
Tactic: convert! (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt
-- 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
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
have h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
Tactic: have h₀ : HasFDerivAt (fun w : E => ‖w‖ ^ 2) (0 : StrongDual ℝ E) 0 := by
    convert! (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt
    simp only [map_zero, smul_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
h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0
have h : Real.instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
    Eq (α := E →L[ℝ] ℝ) 0
      (ContinuousLinearMap.toSpanSingleton ℝ
          (-(HPow.hPow (β := ℕ)
                (HAdd.hAdd (α := E → ℝ) (β := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (fun (x : E) ↦ 4) 0)
                2)⁻¹) ∘SL
        HAdd.hAdd (α := E →L[ℝ] ℝ) 0 0)
Tactic: convert! (hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0))
-- 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
h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
h :
  Real.instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      Eq (α := E →L[ℝ] ℝ) 0
        (ContinuousLinearMap.toSpanSingleton ℝ
            (-(HPow.hPow (β := ℕ)
                  (HAdd.hAdd (α := E → ℝ) (β := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (fun (x : E) ↦ 4) 0)
                  2)⁻¹) ∘SL
          HAdd.hAdd (α := E →L[ℝ] ℝ) 0 0)
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0
have convert! : HAdd.hAdd (α := E → ℝ) (β := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (fun (x : E) ↦ 4) 0 ≠ 0
Tactic: convert! (hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0))
-- 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
h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
have h₁ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0
Tactic: have h₁ : HasFDerivAt (fun w : E => (‖w‖ ^ 2 + 4)⁻¹) (0 : StrongDual ℝ E) 0 := by
    convert! (hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0)) <;> 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
h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
h₁ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0
⊢ HasFDerivAt (fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v)
    (HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E)) 0
have h : HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) =
  HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) +
      ContinuousLinearMap.smulRight (S := ℝ) 0 (id 0) +
    (HSMul.hSMul (β := E →L[ℝ] E)
        (HSub.hSub (α := E → ℝ) (β := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (fun (x : E) ↦ 4) 0) 0 +
      (HSub.hSub (α := E →L[ℝ] ℝ) 0 0).smulRight v)
Tactic: convert!
      ((hasFDerivAt_const (4 : ℝ) 0).smul (hasFDerivAt_id 0)).add
        ((h₀.sub (hasFDerivAt_const (4 : ℝ) 0)).smul (hasFDerivAt_const v 0)) using 1
-- 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
h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
h₁ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0
⊢ HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) =
    HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) +
        ContinuousLinearMap.smulRight (S := ℝ) 0 (id 0) +
      (HSMul.hSMul (β := E →L[ℝ] E)
          (HSub.hSub (α := E → ℝ) (β := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (fun (x : E) ↦ 4) 0) 0 +
        (HSub.hSub (α := E →L[ℝ] ℝ) 0 0).smulRight v)
have h : ∀ (w : E),
  Eq (α := E) ((HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) : (a : E) → E) w : E)
    ((HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) +
              ContinuousLinearMap.smulRight (S := ℝ) 0 (id 0) +
            (HSMul.hSMul (β := E →L[ℝ] E)
                (HSub.hSub (α := E → ℝ) (β := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (fun (x : E) ↦ 4) 0) 0 +
              (HSub.hSub (α := E →L[ℝ] ℝ) 0 0).smulRight v) :
          (a : E) → E)
        w :
      E)
Tactic: ext w
-- 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
h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
h₁ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
have h₂ : HasFDerivAt (fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v)
  (HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E)) 0
Tactic: have h₂ : HasFDerivAt (fun w => (4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v)
      ((4 : ℝ) • ContinuousLinearMap.id ℝ E) 0 := by
    convert!
      ((hasFDerivAt_const (4 : ℝ) 0).smul (hasFDerivAt_id 0)).add
        ((h₀.sub (hasFDerivAt_const (4 : ℝ) 0)).smul (hasFDerivAt_const v 0)) using 1
    ext w
    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
h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
h₁ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0
h₂ :
  HasFDerivAt (fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v)
    (HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E)) 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
have h : ContinuousLinearMap.id ℝ E =
  (HPow.hPow (β := ℕ) (norm.{u_1} (E := E) 0) 2 + 4)⁻¹ •
      HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) +
    ContinuousLinearMap.smulRight (S := ℝ) 0
      (HSMul.hSMul (α := ℝ) (β := E) 4 0 + (HPow.hPow (β := ℕ) (norm.{u_1} (E := E) 0) 2 - 4) • v)
Tactic: convert! h₁.smul h₂ using 1
-- 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
h₀ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0
h₁ : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0
h₂ :
  HasFDerivAt (fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v)
    (HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E)) 0
⊢ ContinuousLinearMap.id ℝ E =
    (HPow.hPow (β := ℕ) (norm.{u_1} (E := E) 0) 2 + 4)⁻¹ •
        HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) +
      ContinuousLinearMap.smulRight (S := ℝ) 0
        (HSMul.hSMul (α := ℝ) (β := E) 4 0 + (HPow.hPow (β := ℕ) (norm.{u_1} (E := E) 0) 2 - 4) • v)
have h : ∀ (w : E),
  Eq (α := E) ((ContinuousLinearMap.id ℝ E : (a : E) → E) w : E)
    (((HPow.hPow (β := ℕ) (norm.{u_1} (E := E) 0) 2 + 4)⁻¹ •
              HSMul.hSMul (α := ℝ) (β := E →L[ℝ] E) 4 (ContinuousLinearMap.id ℝ E) +
            ContinuousLinearMap.smulRight (S := ℝ) 0
              (HSMul.hSMul (α := ℝ) (β := E) 4 0 + (HPow.hPow (β := ℕ) (norm.{u_1} (E := E) 0) 2 - 4) • v) :
          (a : E) → E)
        w :
      E)
Tactic: ext w
-- 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
⊢ HasFDerivAt (E := ↥(ℝ ∙ v)ᗮ)
    (stereoInvFunAux v ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ x))
    (Submodule.subtypeL (ℝ ∙ v)ᗮ) 0
have this : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((Submodule.subtypeL (ℝ ∙ v)ᗮ : (a : ↥(ℝ ∙ v)ᗮ) → E) 0)
Tactic: have : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((ℝ ∙ v)ᗮ.subtypeL 0) :=
    hasFDerivAt_stereoInvFunAux 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
m : ℕ∞ω
⊢ ContDiff ℝ m (stereoInvFunAux v)
have h₀ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2
Tactic: have h₀ : ContDiff ℝ ω fun w : E => ‖w‖ ^ 2 := contDiff_norm_sq ℝ
-- 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
m : ℕ∞ω
h₀ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2
⊢ ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹
have refine : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 + 4 ≠ 0
Tactic: refine (h₀.add contDiff_const).inv ?_
-- 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
m : ℕ∞ω
h₀ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 4 ≠ 0
have nlinarith : HPow.hPow (β := ℕ) ‖x‖ 2 + 4 = 0 →
  HMul.hMul (α := ℝ) 4 (-1) + (0 - HPow.hPow (β := ℕ) ‖x‖ 2) + (HPow.hPow (β := ℕ) ‖x‖ 2 + 4 - 0) = 0
Tactic: nlinarith
-- 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
m : ℕ∞ω
h₀ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2
x : E
nlinarith :
  HPow.hPow (β := ℕ) ‖x‖ 2 + 4 = 0 →
    HMul.hMul (α := ℝ) 4 (-1) + (0 - HPow.hPow (β := ℕ) ‖x‖ 2) + (HPow.hPow (β := ℕ) ‖x‖ 2 + 4 - 0) = 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 4 ≠ 0
have nlinarith₁ : HPow.hPow (β := ℕ) ‖x‖ 2 + 4 = 0 → GT.gt (α := ℝ) 4 0
Tactic: nlinarith
-- 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
m : ℕ∞ω
h₀ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2
⊢ ContDiff ℝ m (stereoInvFunAux v)
have h₁ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹
Tactic: have h₁ : ContDiff ℝ ω fun w : E => (‖w‖ ^ 2 + 4)⁻¹ := by
    refine (h₀.add contDiff_const).inv ?_
    intro x
    nlinarith
-- 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
m : ℕ∞ω
h₀ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2
h₁ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹
⊢ ContDiff ℝ (F := E) ω fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v
have refine : ContDiff ℝ (F := E) ω fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v
Tactic: refine (contDiff_const.smul contDiff_id).add ?_
-- 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
m : ℕ∞ω
h₀ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2
h₁ : ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹
⊢ ContDiff ℝ m (stereoInvFunAux v)
have h₂ : ContDiff ℝ (F := E) ω fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v
Tactic: have h₂ : ContDiff ℝ ω fun w => (4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v := by
    refine (contDiff_const.smul contDiff_id).add ?_
    exact (h₀.sub contDiff_const).smul contDiff_const
-- 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)ᗮ
⊢ stereoInvFun hv w ≠ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯
have refine : (↑(stereoInvFun hv w) : E) ≠ (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v sorry) : E)
Tactic: refine Subtype.coe_ne_coe.1 ?_
-- 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)ᗮ
⊢ (↑(stereoInvFun hv w) : E) ≠ (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯) : E)
have rw : ⟪(↑(stereoInvFun hv w) : E), v⟫_ℝ < 1
Tactic: rw [← inner_lt_one_iff_real_of_norm_eq_one _ 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)ᗮ
rw : ⟪(↑(stereoInvFun hv w) : E), v⟫_ℝ < 1
⊢ (↑(stereoInvFun hv w) : E) ≠ (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯) : E)
have rw₁ : ‖(↑(stereoInvFun hv w) : E)‖ = 1
Tactic: rw [← inner_lt_one_iff_real_of_norm_eq_one _ hv]
-- 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)ᗮ
⊢ ⟪(↑(stereoInvFun hv w) : E), v⟫_ℝ < 1
have hw : ⟪v, (↑w : E)⟫_ℝ = 0
Tactic: have hw : ⟪v, w⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.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
w : ↥(ℝ ∙ v)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
⊢ (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) < 1
have rw : HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 < 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)
Tactic: rw [inv_mul_lt_iff₀']
-- 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)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
rw : HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 < 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)
⊢ (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) < 1
have rw₁ : 0 < HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4
Tactic: rw [inv_mul_lt_iff₀']
-- 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)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
⊢ HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 < 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)
have linarith : 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4) ≤ HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 →
  HMul.hMul (α := ℝ) 8 (-1) + (1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4) - (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4)) = 0
Tactic: 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
w : ↥(ℝ ∙ v)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
linarith :
  1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4) ≤ HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 →
    HMul.hMul (α := ℝ) 8 (-1) + (1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4) - (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4)) = 0
⊢ HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 < 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)
have linarith₁ : 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4) ≤ HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 → GT.gt (α := ℝ) 8 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
w : ↥(ℝ ∙ v)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
⊢ ⟪(↑(stereoInvFun hv w) : E), v⟫_ℝ < 1
have hw' : (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) < 1
Tactic: have hw' : (‖(w : E)‖ ^ 2 + 4)⁻¹ * (‖(w : E)‖ ^ 2 - 4) < 1 := by
      rw [inv_mul_lt_iff₀']
      · linarith
      positivity
-- 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
⊢ stereoInvFun hv (stereoToFun v (↑x : E)) = x
have a : (↑(stereoInvFun hv (stereoToFun v (↑x : E))) : E) = (↑x : E)
Tactic: 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
x : (↑(sphere 0 1) : Type u_1)
hx : (↑x : E) ≠ v
⊢ (↑(stereoInvFun hv (stereoToFun v (↑x : E))) : E) = (↑x : E)
have a : (HPow.hPow (β := ℕ)
            ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ)
                (2 /
                  HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ)
                    ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E) : ℝ))
                ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
            2 +
          4)⁻¹ •
      HSMul.hSMul (α := ℝ) 4
        (↑(HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ)
              (2 /
                HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ)
                  ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E) : ℝ))
              ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)) :
          E) +
    (HPow.hPow (β := ℕ)
            ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ)
                (2 /
                  HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ)
                    ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E) : ℝ))
                ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
            2 +
          4)⁻¹ •
      (HPow.hPow (β := ℕ)
            ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ)
                (2 /
                  HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ)
                    ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E) : ℝ))
                ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
            2 -
          4) •
        v =
  (↑x : E)
Tactic: simp only [stereoToFun_apply, stereoInvFun_apply, smul_add]
-- 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)
⊢ (↑x : E) = a • v + (↑y : E)
have rw : HAdd.hAdd (β := E) (⟪v, (↑x : E)⟫_ℝ • v) ((Submodule.starProjection (ℝ ∙ v)ᗮ : (a : E) → E) (↑x : E) : E) =
  a • v + (↑y : E)
Tactic: rw [← ((ℝ ∙ v).starProjection_add_starProjection_orthogonal x),
      Submodule.starProjection_unit_singleton ℝ hv x]