awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccRightChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccRightChart x y).symm ≫ₕ IccRightChart x y).source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))

Tactic:
(mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1

Premises used: Iff.mpr, ContDiffOn, symm_trans_mem_contDiffGroupoid, And.left, mem_groupoid_of_pregroupoid
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x_1 y_1 : ℝ
hxy : Fact (x_1 < y_1)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M_1 : Type u_3
inst_3 : TopologicalSpace M_1
inst_4 : ChartedSpace H M_1
x y : ℝ
inst_5 : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin 1)) (F := EuclideanSpace ℝ (Fin 1)) n
    (have this : EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) := fun (z : EuclideanSpace ℝ (Fin 1)) ↦
      toLp 2 fun (i : Fin 1) ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n
    ((↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)) ∘
      (↑((IccRightChart x y).symm ≫ₕ IccRightChart x y) : EuclideanHalfSpace 1 → EuclideanHalfSpace 1) ∘
        (↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1))
    ((↑(ModelWithCorners.symm (𝓡∂ 1)) : EuclideanSpace ℝ (Fin 1) → EuclideanHalfSpace 1) ⁻¹'
        ((IccRightChart x y).symm ≫ₕ IccRightChart x y).source ∩
      range (ι := EuclideanHalfSpace 1) (↑(𝓡∂ 1) : EuclideanHalfSpace 1 → EuclideanSpace ℝ (Fin 1)))

Tactic:
exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1

Premises used: Iff.mpr, symm_trans_mem_contDiffGroupoid, And.left, mem_groupoid_of_pregroupoid
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
⊢ ChartedSpace (EuclideanHalfSpace 1) (↑(Icc 0 1) : Type)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Instances.Real
Goal:
x y : ℝ
hxy : Fact (x < y)
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
n : ℕ∞ω
⊢ IsManifold (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) n (↑(Icc 0 1) : Type)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v x : E
⊢ stereoToFun v x =
    HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ)
      (2 /
        HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ))
      ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) x : ↥(ℝ ∙ v)ᗮ)

Tactic:
rfl

Premises used: stereoToFun, rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ ContDiffOn ℝ (F := ↥(ℝ ∙ v)ᗮ) n (stereoToFun v)
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}

Tactic:
ContDiffOn.fun_smul ?_ (ℝ ∙ v)ᗮ.orthogonalProjection.contDiff.contDiffOn

Premises used: Real, ContDiff.contDiffOn, Submodule.orthogonalProjection, Submodule.orthogonal, Submodule.span, stereoToFun, ContinuousLinearMap.contDiff, Singleton.singleton, ContDiffOn.fun_smul
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
refine :
  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 : ℝ)}
⊢ ContDiffOn ℝ (F := ↥(ℝ ∙ v)ᗮ) n (stereoToFun v)
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}

Tactic:
refine ContDiffOn.fun_smul ?_ (ℝ ∙ v)ᗮ.orthogonalProjection.contDiff.contDiffOn

Premises used: Real, ContDiff.contDiffOn, Submodule.orthogonalProjection, Submodule.orthogonal, Submodule.span, ContinuousLinearMap.contDiff, Singleton.singleton, ContDiffOn.fun_smul
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ 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 : ℝ)}

Tactic:
contDiff_const.contDiffOn.div ?_ ?_

Premises used: ContDiff.contDiffOn, contDiff_const, ContDiffOn.div
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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 : ℝ)}
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
⊢ 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 : ℝ)}

Tactic:
refine contDiff_const.contDiffOn.div ?_ ?_

Premises used: ContDiff.contDiffOn, contDiff_const, ContDiffOn.div
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ 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 : ℝ)}

Tactic:
(contDiff_const.sub (innerSL ℝ v).contDiff).contDiffOn

Premises used: ContDiff.sub, Real, ContDiff.contDiffOn, innerSL, contDiff_const, ContinuousLinearMap.contDiff, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ 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 : ℝ)}

Tactic:
exact (contDiff_const.sub (innerSL ℝ v).contDiff).contDiffOn

Premises used: ContDiff.sub, Real, ContDiff.contDiffOn, innerSL, contDiff_const, ContinuousLinearMap.contDiff, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
x : E
h :
  Membership.mem (γ := Set E)
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} x
h' : HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) = 0
⊢ False

Tactic:
h (sub_eq_zero.mp h').symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
x : E
h :
  Membership.mem (γ := Set E)
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} x
h' : HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) = 0
⊢ False

Tactic:
exact h (sub_eq_zero.mp h').symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
⊢ ContinuousOn (Y := ↥(ℝ ∙ v)ᗮ) (stereoToFun v)
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}

Tactic:
(contDiffOn_stereoToFun (n := 0)).continuousOn

Premises used: Set.Mem, setOf, contDiffOn_stereoToFun, ContDiffOn.continuousOn
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v w : E
⊢ stereoInvFunAux v w =
    (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹ • (HSMul.hSMul (α := ℝ) 4 w + (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 : E
hw : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ w
⊢ 0 < HPow.hPow (β := ℕ) ‖w‖ 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 : E
hw : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ w
⊢ 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4

Tactic:
have h₁ : (0 : ℝ) < ‖w‖ ^ 2 + 4 := by 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 : E
hw : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ w
h₁ : 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4
this : ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ = HPow.hPow (β := ℕ) ‖w‖ 2 + 4
⊢ Membership.mem (γ := Set E) (sphere 0 1) (stereoInvFunAux v w)

Tactic:
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']

Premises used: norm_smul, stereoInvFunAux_apply, abs_inv, mem_sphere_zero_iff_norm, LT.lt.ne', abs_of_pos, inv_mul_cancel₀, 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
w : E
hw : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ v)ᗮ w
h₁ : 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4
suffices : ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ = HPow.hPow (β := ℕ) ‖w‖ 2 + 4
⊢ Membership.mem (γ := Set E) (sphere 0 1) (stereoInvFunAux v w)

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']
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
this :
  HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖w‖ 2 + 4) 2
⊢ ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ = HPow.hPow (β := ℕ) ‖w‖ 2 + 4

Tactic:
simpa only [sq_eq_sq_iff_abs_eq_abs, abs_norm, abs_of_pos h₁] using this

Premises used: sq_eq_sq_iff_abs_eq_abs, abs_of_pos, abs_norm
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
suffices :
  HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖w‖ 2 + 4) 2
⊢ ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ = HPow.hPow (β := ℕ) ‖w‖ 2 + 4

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
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
⊢ ⟪w, v⟫ = 0

Tactic:
rw [Submodule.mem_orthogonal_singleton_iff_inner_left] at hw

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_left
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
hw₁ : ⟪w, v⟫ = 0
⊢ 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4

Tactic:
rw [Submodule.mem_orthogonal_singleton_iff_inner_left] at hw

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_left
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
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
⊢ HPow.hPow (β := ℕ) ‖HSMul.hSMul (α := ℝ) 4 w + (HPow.hPow (β := ℕ) ‖w‖ 2 - 4) • v‖ 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]

Premises used: norm_smul, inner_smul_right, norm_add_sq_real, mul_pow, Real.norm_eq_abs, 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
w : E
hw : ⟪w, v⟫ = 0
h₁ : 0 < HPow.hPow (β := ℕ) ‖w‖ 2 + 4
⊢ 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:
ring
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
⊢ HasFDerivAt (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)
    (HSMul.hSMul (α := ℕ) (β := E →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) 0 : E →L[ℝ] ℝ)) 0

Tactic:
(hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt

Premises used: hasStrictFDerivAt_norm_sq, HasStrictFDerivAt.hasFDerivAt, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
h : 0 = HSMul.hSMul (α := ℕ) (β := E →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) 0 : E →L[ℝ] ℝ)
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) 0 0

Tactic:
convert! (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt

Premises used: hasStrictFDerivAt_norm_sq, HasStrictFDerivAt.hasFDerivAt, OfNat.ofNat
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
⊢ 0 = HSMul.hSMul (α := ℕ) (β := E →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) 0 : E →L[ℝ] ℝ)

Tactic:
simp only [map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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

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]
-- 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
⊢ HasFDerivAt ((fun (x : ℝ) ↦ x⁻¹) ∘ HAdd.hAdd (α := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) fun (x : E) ↦ 4)
    (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)
    0

Tactic:
(hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0))

Premises used: HasFDerivAt.add, hasFDerivAt_const, OfNat.ofNat, HasFDerivAt.comp
-- 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 :
  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)
convert! : HAdd.hAdd (α := E → ℝ) (β := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (fun (x : E) ↦ 4) 0 ≠ 0
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w : E) ↦ (HPow.hPow (β := ℕ) ‖w‖ 2 + 4)⁻¹) 0 0

Tactic:
convert! (hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0))

Premises used: HasFDerivAt.add, hasFDerivAt_const, OfNat.ofNat, HasFDerivAt.comp
-- 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
e_8 : Real.instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : 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:
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
⊢ HAdd.hAdd (α := E → ℝ) (β := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (fun (x : E) ↦ 4) 0 ≠ 0

Tactic:
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
⊢ 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
-- 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
    (HSMul.hSMul (α := E → ℝ) (β := E → E) (fun (x : E) ↦ 4) id +
      HSMul.hSMul (β := E → E) (HSub.hSub (α := E → ℝ) (fun (w : E) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) fun (x : E) ↦ 4)
        fun (x : E) ↦ v)
    (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))
    0

Tactic:
((hasFDerivAt_const (4 : ℝ) 0).smul (hasFDerivAt_id 0)).add
        ((h₀.sub (hasFDerivAt_const (4 : ℝ) 0)).smul (hasFDerivAt_const v 0))

Premises used: HasFDerivAt.sub, HasFDerivAt.add, hasFDerivAt_id, hasFDerivAt_const, OfNat.ofNat, 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 :
  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)
⊢ 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:
convert!
      ((hasFDerivAt_const (4 : ℝ) 0).smul (hasFDerivAt_id 0)).add
        ((h₀.sub (hasFDerivAt_const (4 : ℝ) 0)).smul (hasFDerivAt_const v 0)) using 1

Premises used: HasFDerivAt.sub, HasFDerivAt.add, hasFDerivAt_id, hasFDerivAt_const, OfNat.ofNat, 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 :
  ∀ (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)
⊢ 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:
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
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:
simp