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
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  Eq (α := Submodule ℝ E)
    (LinearMap.range (M := EuclideanSpace ℝ (Fin n))
      (↑(fderiv ℝ
            (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
              (stereoInvFunAux (-(↑v : E)) ∘
                Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
            0) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E))
    (ℝ ∙ (↑v : E))ᗮ
h :
  Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)) = Submodule ℝ E →
    TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v = EuclideanSpace ℝ (Fin n) →
      TangentSpace 𝓘(ℝ, E) (↑v : E) = E →
        HEq (α := AddCommMonoid (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)) AddCommGroup.toAddCommMonoid
            (β := AddCommMonoid (EuclideanSpace ℝ (Fin n))) AddCommGroup.toAddCommMonoid →
          HEq.{u_1 + 1} (α := AddCommMonoid (TangentSpace 𝓘(ℝ, E) (↑v : E))) AddCommGroup.toAddCommMonoid (β :=
              AddCommMonoid E) AddCommGroup.toAddCommMonoid →
            HEq (α := Module ℝ (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)) (instModuleTangentSpace (𝓡 n) v)
                (β := Module ℝ (EuclideanSpace ℝ (Fin n)))
                (WithLp.instModule 2 ℝ ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)) →
              HEq (α := Module ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E))) (instModuleTangentSpace 𝓘(ℝ, E) (↑v : E)) (β :=
                  Module ℝ E) (NormedSpace.toModule : Module ℝ E) →
                HEq (α := TopologicalSpace (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v))
                    (instTopologicalSpaceTangentSpace (𝓡 n) v) (β := TopologicalSpace (EuclideanSpace ℝ (Fin n)))
                    (PiLp.topologicalSpace 2 fun (x : Fin n) ↦ ℝ) →
                  HEq (α := TopologicalSpace (TangentSpace 𝓘(ℝ, E) (↑v : E)))
                      (instTopologicalSpaceTangentSpace 𝓘(ℝ, E) (↑v : E)) (β := TopologicalSpace E)
                      UniformSpace.toTopologicalSpace →
                    Eq (α := EuclideanSpace ℝ (Fin n))
                      ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v) 0
⊢ Eq (α := Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (LinearMap.range (M := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)
      (↑(fderiv ℝ
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
              (↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt v)) :
                EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
            ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v)) :
        TangentSpace (𝓡 n) v →ₗ[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (ℝ ∙ (↑v : E))ᗮ

Tactic:
convert! this using 4
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  Eq (α := Submodule ℝ E)
    (LinearMap.range (M := EuclideanSpace ℝ (Fin n))
      (↑(fderiv ℝ
            (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
              (stereoInvFunAux (-(↑v : E)) ∘
                Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
            0) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E))
    (ℝ ∙ (↑v : E))ᗮ
e_1 : Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)) = Submodule ℝ E
e_3 : TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v = EuclideanSpace ℝ (Fin n)
e_4 : TangentSpace 𝓘(ℝ, E) (↑v : E) = E
e_7 :
  HEq (α := AddCommMonoid (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)) AddCommGroup.toAddCommMonoid (β :=
    AddCommMonoid (EuclideanSpace ℝ (Fin n))) AddCommGroup.toAddCommMonoid
e_8 :
  HEq.{u_1 + 1} (α := AddCommMonoid (TangentSpace 𝓘(ℝ, E) (↑v : E))) AddCommGroup.toAddCommMonoid (β := AddCommMonoid E)
    AddCommGroup.toAddCommMonoid
e_9 :
  HEq (α := Module ℝ (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)) (instModuleTangentSpace (𝓡 n) v) (β :=
    Module ℝ (EuclideanSpace ℝ (Fin n))) (WithLp.instModule 2 ℝ ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i))
e_10 :
  HEq (α := Module ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E))) (instModuleTangentSpace 𝓘(ℝ, E) (↑v : E)) (β := Module ℝ E)
    (NormedSpace.toModule : Module ℝ E)
e_7_1 :
  HEq (α := TopologicalSpace (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v))
    (instTopologicalSpaceTangentSpace (𝓡 n) v) (β := TopologicalSpace (EuclideanSpace ℝ (Fin n)))
    (PiLp.topologicalSpace 2 fun (x : Fin n) ↦ ℝ)
e_10_1 :
  HEq (α := TopologicalSpace (TangentSpace 𝓘(ℝ, E) (↑v : E))) (instTopologicalSpaceTangentSpace 𝓘(ℝ, E) (↑v : E)) (β :=
    TopologicalSpace E) UniformSpace.toTopologicalSpace
⊢ Eq (α := EuclideanSpace ℝ (Fin n))
    ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v) 0

Tactic:
apply stereographic'_neg

Premises used: _private.0.stereographic'_neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
ℝ :
  Eq (α := Submodule ℝ E)
    (LinearMap.range (M := EuclideanSpace ℝ (Fin n))
      (↑(fderiv ℝ
            (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
              (stereoInvFunAux (-(↑v : E)) ∘
                Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
            0) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E))
    (ℝ ∙ (↑v : E))ᗮ
⊢ Eq (α := Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (LinearMap.range (M := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)
      (↑(fderiv ℝ
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
              (↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt v)) :
                EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
            ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v)) :
        TangentSpace (𝓡 n) v →ₗ[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (ℝ ∙ (↑v : E))ᗮ

Tactic:
suffices
      (fderiv ℝ ((stereoInvFunAux (-v : E) ∘ (↑)) ∘ U.symm) 0).range = (ℝ ∙ (v : E))ᗮ by
    convert! this using 4
    apply stereographic'_neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
⊢ HasFDerivAt (E := ↥(ℝ ∙ -(↑v : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ -(↑v : E))ᗮ) 0

Tactic:
hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)

Premises used: Subtype.val, Neg.neg, hasFDerivAt_stereoInvFunAux_comp_coe
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
h :
  ↥(ℝ ∙ (↑(-v) : E))ᗮ = ↥(ℝ ∙ -(↑v : E))ᗮ →
    Eq (α := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
      ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0 : ↥(ℝ ∙ (↑(-v) : E))ᗮ) (0 : ↥(ℝ ∙ -(↑v : E))ᗮ)
⊢ HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)

Tactic:
convert! hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)

Premises used: Subtype.val, Neg.neg, hasFDerivAt_stereoInvFunAux_comp_coe
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
e_3 : ↥(ℝ ∙ (↑(-v) : E))ᗮ = ↥(ℝ ∙ -(↑v : E))ᗮ
⊢ Eq (α := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0 : ↥(ℝ ∙ (↑(-v) : E))ᗮ) (0 : ↥(ℝ ∙ -(↑v : E))ᗮ)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
⊢ HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)

Tactic:
have :
    HasFDerivAt (stereoInvFunAux (-v : E) ∘ (Subtype.val : (ℝ ∙ (↑(-v) : E))ᗮ → E))
      (ℝ ∙ (↑(-v) : E))ᗮ.subtypeL (U.symm 0) := by
    convert! hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)
    simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
⊢ LinearMap.range (M := EuclideanSpace ℝ (Fin n))
      (↑(fderiv ℝ
            (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
              (stereoInvFunAux (-(↑v : E)) ∘
                Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
            0) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E) =
    (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
            (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
              EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range

Tactic:
congr($((this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv).range)

Premises used: LinearIsometryEquiv.symm, congrArg, LinearMap.range, id, ContinuousLinearMap.toLinearMap, HasFDerivAt.fderiv, ContinuousLinearEquiv.hasFDerivAt, LinearIsometryEquiv.toContinuousLinearEquiv, OfNat.ofNat, HasFDerivAt.comp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h :
  (ℝ ∙ (↑v : E))ᗮ =
    (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
            (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
              EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range
⊢ Eq (α := Submodule ℝ E)
    (LinearMap.range (M := EuclideanSpace ℝ (Fin n))
      (↑(fderiv ℝ
            (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
              (stereoInvFunAux (-(↑v : E)) ∘
                Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
            0) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E))
    (ℝ ∙ (↑v : E))ᗮ

Tactic:
convert! congr($((this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv).range)
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h :
  (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
            (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
              EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range =
    (ℝ ∙ (↑v : E))ᗮ
⊢ (ℝ ∙ (↑v : E))ᗮ =
    (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
            (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
              EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range

Tactic:
symm
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
⊢ (Submodule.subtype (ℝ ∙ (↑(-v) : E))ᗮ ∘ₗ
        (↑U.symm.toLinearEquiv : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)).range =
    LinearMap.range (M := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (Submodule.subtype (ℝ ∙ (↑(-v) : E))ᗮ)

Tactic:
(U.symm : EuclideanSpace ℝ (Fin n) ≃ₗᵢ[ℝ] (ℝ ∙ (↑(-v) : E))ᗮ).range_comp
      (ℝ ∙ (↑(-v) : E))ᗮ.subtype

Premises used: Real, LinearIsometryEquiv.symm, LinearEquiv.range_comp, LinearIsometryEquiv.toLinearEquiv, Submodule.orthogonal, Submodule.span, Submodule.subtype, Singleton.singleton, Subtype.val, Neg.neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h :
  Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E))ᗮ
    (LinearMap.range (M := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (Submodule.subtype (ℝ ∙ (↑(-v) : E))ᗮ))
⊢ (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
            (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
              EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range =
    (ℝ ∙ (↑v : E))ᗮ

Tactic:
convert!
    (U.symm : EuclideanSpace ℝ (Fin n) ≃ₗᵢ[ℝ] (ℝ ∙ (↑(-v) : E))ᗮ).range_comp
      (ℝ ∙ (↑(-v) : E))ᗮ.subtype using 1

Premises used: Real, LinearIsometryEquiv.symm, LinearEquiv.range_comp, LinearIsometryEquiv.toLinearEquiv, Submodule.orthogonal, Submodule.span, Submodule.subtype, Singleton.singleton, Subtype.val, Neg.neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h : Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E))ᗮ (ℝ ∙ -(↑v : E))ᗮ
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E))ᗮ
    (LinearMap.range (M := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (Submodule.subtype (ℝ ∙ (↑(-v) : E))ᗮ))

Tactic:
simp only [Submodule.range_subtype, coe_neg_sphere]

Premises used: coe_neg_sphere, Submodule.range_subtype
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h : Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E)) (ℝ ∙ -(↑v : E))
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E))ᗮ (ℝ ∙ -(↑v : E))ᗮ

Tactic:
congr 1
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h : {(↑v : E)} ⊆ (↑(ℝ ∙ -(↑v : E)) : Set E)
h₁ : {-(↑v : E)} ⊆ (↑(ℝ ∙ (↑v : E)) : Set E)
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E)) (ℝ ∙ -(↑v : E))

Tactic:
apply Submodule.span_eq_span

Premises used: Submodule.span_eq_span
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E)) (↑v : E)
⊢ {(↑v : E)} ⊆ (↑(ℝ ∙ -(↑v : E)) : Set E)

Tactic:
simp only [Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, SetLike.mem_coe
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E)) (-(↑v : E))
⊢ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E)) (↑v : E)

Tactic:
rw [← Submodule.neg_mem_iff]

Premises used: Submodule.neg_mem_iff
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
⊢ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E)) (-(↑v : E))

Tactic:
Submodule.mem_span_singleton_self (-v : E)

Premises used: Set.Mem, setOf, Submodule.mem_span_singleton_self, Subtype.val, Neg.neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
⊢ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E)) (-(↑v : E))

Tactic:
exact Submodule.mem_span_singleton_self (-v : E)

Premises used: Submodule.mem_span_singleton_self, Subtype.val, Neg.neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
h : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑v : E)) (-(↑v : E))
⊢ {-(↑v : E)} ⊆ (↑(ℝ ∙ (↑v : E)) : Set E)

Tactic:
simp only [Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, SetLike.mem_coe