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
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

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
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
    (HSMul.hSMul (α := E → ℝ) (β := E → E) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) fun (w : E) ↦
      HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v)
    ((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))
    0

Tactic:
h₁.smul h₂

Premises used: HasFDerivAt.smul
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
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)
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Tactic:
convert! h₁.smul h₂ using 1

Premises used: HasFDerivAt.smul
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
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)
⊢ 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:
ext w
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
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:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
⊢ 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
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
this :
  HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((Submodule.subtypeL (ℝ ∙ v)ᗮ : (a : ↥(ℝ ∙ v)ᗮ) → E) 0)
⊢ HasFDerivAt (E := ↥(ℝ ∙ v)ᗮ) (⇑(Submodule.subtypeL (ℝ ∙ v)ᗮ) : (a : ↥(ℝ ∙ v)ᗮ) → E) (Submodule.subtypeL (ℝ ∙ v)ᗮ) 0

Tactic:
apply ContinuousLinearMap.hasFDerivAt

Premises used: ContinuousLinearMap.hasFDerivAt
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
this :
  HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((Submodule.subtypeL (ℝ ∙ v)ᗮ : (a : ↥(ℝ ∙ v)ᗮ) → E) 0)
⊢ HasFDerivAt (E := ↥(ℝ ∙ v)ᗮ)
    (stereoInvFunAux v ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ x))
    (Submodule.subtypeL (ℝ ∙ v)ᗮ) 0

Tactic:
refine this.comp (0 : (ℝ ∙ v)ᗮ) (by apply ContinuousLinearMap.hasFDerivAt)

Premises used: OfNat.ofNat, HasFDerivAt.comp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
m : ℕ∞ω
⊢ ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2

Tactic:
have h₀ : ContDiff ℝ ω fun w : E => ‖w‖ ^ 2 := contDiff_norm_sq ℝ
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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)⁻¹

Tactic:
(h₀.add contDiff_const).inv ?_

Premises used: contDiff_const, ContDiff.add, ContDiff.inv
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
refine : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 + 4 ≠ 0
⊢ ContDiff ℝ (F := ℝ) ω fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹

Tactic:
refine (h₀.add contDiff_const).inv ?_

Premises used: contDiff_const, ContDiff.add, ContDiff.inv
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
nlinarith₁ : HPow.hPow (β := ℕ) ‖x‖ 2 + 4 = 0 → GT.gt (α := ℝ) 4 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + 4 ≠ 0

Tactic:
nlinarith
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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)⁻¹

Tactic:
have h₁ : ContDiff ℝ ω fun w : E => (‖w‖ ^ 2 + 4)⁻¹ := by
    refine (h₀.add contDiff_const).inv ?_
    intro x
    nlinarith
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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

Tactic:
(contDiff_const.smul contDiff_id).add ?_

Premises used: contDiff_id, contDiff_const, ContDiff.smul, ContDiff.add
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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)⁻¹
refine : ContDiff ℝ (F := E) ω fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v
⊢ ContDiff ℝ (F := E) ω fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v

Tactic:
refine (contDiff_const.smul contDiff_id).add ?_

Premises used: contDiff_id, contDiff_const, ContDiff.smul, ContDiff.add
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v

Tactic:
(h₀.sub contDiff_const).smul contDiff_const

Premises used: ContDiff.sub, contDiff_const, ContDiff.smul
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v

Tactic:
exact (h₀.sub contDiff_const).smul contDiff_const

Premises used: ContDiff.sub, contDiff_const, ContDiff.smul
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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

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
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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)⁻¹
h₂ : ContDiff ℝ (F := E) ω fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v
⊢ ContDiff ℝ m (stereoInvFunAux v)

Tactic:
(h₁.smul h₂).of_le le_top

Premises used: ContDiff.of_le, ContDiff.smul, le_top, stereoInvFunAux
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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)⁻¹
h₂ : ContDiff ℝ (F := E) ω fun (w : E) ↦ HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v
⊢ ContDiff ℝ m (stereoInvFunAux v)

Tactic:
exact (h₁.smul h₂).of_le le_top

Premises used: ContDiff.of_le, ContDiff.smul, le_top
-- 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)ᗮ
⊢ (↑(stereoInvFun hv w) : E) =
    (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹ • (HSMul.hSMul (α := ℝ) 4 (↑w : E) + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v)

Tactic:
rfl

Premises used: stereoInvFunAux, rfl
-- 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)ᗮ
⊢ Membership.mem (γ := Set E) (sphere 0 1) v

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)ᗮ
⊢ stereoInvFun hv w ≠ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯

Tactic:
Subtype.coe_ne_coe.1 ?_

Premises used: Iff.mp, Subtype.coe_ne_coe
-- 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)ᗮ
refine :
  (↑(stereoInvFun hv w) : E) ≠ (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯) : E)
⊢ stereoInvFun hv w ≠ Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯

Tactic:
refine Subtype.coe_ne_coe.1 ?_

Premises used: Iff.mp, Subtype.coe_ne_coe
-- 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)ᗮ
rw : ⟪(↑(stereoInvFun hv w) : E), v⟫_ℝ < 1
rw₁ : ‖(↑(stereoInvFun hv w) : E)‖ = 1
⊢ (↑(stereoInvFun hv w) : E) ≠ (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯) : E)

Tactic:
rw [← inner_lt_one_iff_real_of_norm_eq_one _ hv]

Premises used: inner_lt_one_iff_real_of_norm_eq_one
-- 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)ᗮ
⊢ ⟪v, (↑w : E)⟫_ℝ = 0

Tactic:
have hw : ⟪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)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
rw : HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 < 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)
rw₁ : 0 < HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4
⊢ (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) < 1

Tactic:
rw [inv_mul_lt_iff₀']

Premises used: inv_mul_lt_iff₀'
-- 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)ᗮ
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
linarith₁ : 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4) ≤ HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 → GT.gt (α := ℝ) 8 0
⊢ HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4 < 1 * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)

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
w : ↥(ℝ ∙ v)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
⊢ 0 < HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4

Tactic:
positivity
-- 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)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
⊢ (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
-- 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)ᗮ
hw : ⟪v, (↑w : E)⟫_ℝ = 0
hw' : (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 + 4)⁻¹ * (HPow.hPow (β := ℕ) ‖(↑w : E)‖ 2 - 4) < 1
⊢ ⟪(↑(stereoInvFun hv w) : E), v⟫_ℝ < 1

Tactic:
simpa [real_inner_comm, inner_add_right, inner_smul_right, real_inner_self_eq_norm_mul_norm, hw,
      hv] using hw'

Premises used: inner_add_right, inner_smul_right, real_inner_self_eq_norm_mul_norm, real_inner_comm
-- 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)ᗮ
⊢ ‖(↑(stereoInvFun hv w) : E)‖ = 1

Tactic:
simpa using stereoInvFunAux_mem hv w.2

Premises used: stereoInvFunAux_mem, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
⊢ Continuous (X := ↥(ℝ ∙ v)ᗮ) (stereoInvFun hv)

Tactic:
continuous_induced_rng.2
    ((contDiff_stereoInvFunAux (m := 0)).continuous.comp continuous_subtype_val)

Premises used: Iff.mpr, continuous_subtype_val, Continuous.comp, ContDiff.continuous, contDiff_stereoInvFunAux, continuous_induced_rng
-- 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 : (↑(stereoInvFun hv (stereoToFun v (↑x : E))) : E) = (↑x : E)
⊢ stereoInvFun hv (stereoToFun v (↑x : E)) = x

Tactic:
ext
-- 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 :
  (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)
⊢ (↑(stereoInvFun hv (stereoToFun v (↑x : E))) : E) = (↑x : E)

Tactic:
simp only [stereoToFun_apply, stereoInvFun_apply, smul_add]

Premises used: stereoInvFun_apply, stereoToFun_apply, smul_add
-- 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 :
  let a : ℝ := (((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) (↑x : E);
  (HPow.hPow (β := ℕ)
              ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - a))
                  ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
              2 +
            4)⁻¹ •
        HSMul.hSMul (α := ℝ) 4
          (↑(HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - a))
                ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)) :
            E) +
      (HPow.hPow (β := ℕ)
              ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - a))
                  ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
              2 +
            4)⁻¹ •
        (HPow.hPow (β := ℕ)
              ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - a))
                  ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
              2 -
            4) •
          v =
    (↑x : 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)⁻¹ •
        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:
set a : ℝ := innerSL _ v x

Premises used: innerSL, Subtype.val, DFunLike.coe
-- 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)
a₁ :
  let 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)
⊢ (HPow.hPow (β := ℕ)
              ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - a))
                  ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
              2 +
            4)⁻¹ •
        HSMul.hSMul (α := ℝ) 4
          (↑(HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - a))
                ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)) :
            E) +
      (HPow.hPow (β := ℕ)
              ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - a))
                  ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
              2 +
            4)⁻¹ •
        (HPow.hPow (β := ℕ)
              ‖HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - a))
                  ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)‖
              2 -
            4) •
          v =
    (↑x : E)

Tactic:
set y := (ℝ ∙ v)ᗮ.orthogonalProjection x

Premises used: Real, Submodule.orthogonalProjection, Submodule.orthogonal, Submodule.span, Singleton.singleton, Subtype.val, DFunLike.coe