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 :
  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, Submodule.mem_span_singleton_self, Subtype.val
-- 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
-- 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)
rw :
  Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(fderivWithin ℝ
          (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x)))
          (Set.range (↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
          ((↑(extChartAt (𝓡 n) v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v)) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))
⊢ Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(mfderiv% (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x)) v) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))

Tactic:
rw [((contMDiff_coe_sphere v).mdifferentiableAt one_ne_zero).mfderiv]

Premises used: ContMDiffAt.mdifferentiableAt, contMDiff_coe_sphere, MDifferentiableAt.mfderiv, one_ne_zero
-- 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)
simp :
  Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(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)) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))
⊢ Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(fderivWithin ℝ
          (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x)))
          (Set.range (↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
          ((↑(extChartAt (𝓡 n) v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v)) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))

Tactic:
simp only [chartAt, fderivWithin_univ, mfld_simps]

Premises used: chartAt, fderivWithin_univ
-- 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 :
  Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)

Tactic:
this
-- 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 :
  Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
h :
  TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v = EuclideanSpace ℝ (Fin n) →
    TangentSpace 𝓘(ℝ, E) (↑v : E) = E →
      (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v →L[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)) =
          (EuclideanSpace ℝ (Fin n) →L[ℝ] E) →
        Eq (α := EuclideanSpace ℝ (Fin n))
          ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v) 0
⊢ Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(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)) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))

Tactic:
convert! this using 3
-- 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 :
  Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
e_1 : TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v = EuclideanSpace ℝ (Fin n)
e_2 : TangentSpace 𝓘(ℝ, E) (↑v : E) = E
e_1_1 :
  (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v →L[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)) =
    (EuclideanSpace ℝ (Fin n) →L[ℝ] E)
⊢ 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 ⋯)
suffices :
  Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
⊢ Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(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)) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))

Tactic:
suffices Injective (fderiv ℝ ((stereoInvFunAux (-v : E) ∘ (↑)) ∘ U.symm) 0) by
    convert! this using 3
    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))ᗮ) ((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)
⊢ Eq (α := (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)

Tactic:
have := congr_arg DFunLike.coe <| (this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv
-- 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_1 :
  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)
this :
  Eq (α := (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)

Tactic:
Eq.subst this.symm ?_

Premises used: Eq.subst, Eq.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_1 :
  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)
this :
  Eq (α := (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
refine :
  Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)

Tactic:
refine Eq.subst this.symm ?_

Premises used: Eq.subst, Eq.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_1 :
  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)
this :
  Eq (α := (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
rw :
  Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → E)
      (⇑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
        (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)

Tactic:
rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_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_1 :
  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)
this :
  Eq (α := (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → E)
      (⇑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
        (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))

Tactic:
simpa [-Subtype.val_injective] using Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
⊢ Fact (finrank ℝ ℂ = HAdd.hAdd (α := ℕ) 1 1)

Tactic:
finrank_real_complex_fact

Premises used: Complex.finrank_real_complex_fact
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ IsManifold (E := EuclideanSpace ℝ (Fin 1)) (𝓡 1) ω Circle

Tactic:
EuclideanSpace.instIsManifoldSphere (E := ℂ)

Premises used: Set.Mem, setOf, EuclideanSpace.instIsManifoldSphere, Circle, Metric.sphere
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
hf :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1)) 𝓘(ℝ, ℂ)
    (M' := ℂ) ω fun (p : Circle × Circle) ↦ (↑p.1 : ℂ) * (↑p.2 : ℂ)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (ModelWithCorners.prod (𝓡 1) (𝓡 1)) (E' :=
    EuclideanSpace ℝ (Fin 1)) (𝓡 1) (M' := Circle) ω fun (p : Circle × Circle) ↦ p.1 * p.2

Tactic:
apply ContMDiff.codRestrict_sphere

Premises used: ContMDiff.codRestrict_sphere
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
rw :
  (Continuous (Y := ℂ) fun (z : ℂ × ℂ) ↦ z.1 * z.2) ∧
    ∀ (x : ℂ × ℂ) (y : ℂ),
      ContDiffOn ℝ ω
        ((↑(extChartAt 𝓘(ℝ, ℂ) y) : ℂ → ℂ) ∘
          (fun (z : ℂ × ℂ) ↦ z.1 * z.2) ∘
            (↑(extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).symm : ℂ × ℂ → ℂ × ℂ))
        ((extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).target ∩
          (↑(extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).symm : ℂ × ℂ → ℂ × ℂ) ⁻¹'
            (fun (z : ℂ × ℂ) ↦ z.1 * z.2) ⁻¹' (extChartAt 𝓘(ℝ, ℂ) y).source)
⊢ ContMDiff (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) (M' := ℂ) ω fun (z : ℂ × ℂ) ↦ z.1 * z.2

Tactic:
rw [contMDiff_iff]

Premises used: contMDiff_iff
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
⊢ (Continuous (Y := ℂ) fun (z : ℂ × ℂ) ↦ z.1 * z.2) ∧
    ∀ (x : ℂ × ℂ) (y : ℂ),
      ContDiffOn ℝ ω
        ((↑(extChartAt 𝓘(ℝ, ℂ) y) : ℂ → ℂ) ∘
          (fun (z : ℂ × ℂ) ↦ z.1 * z.2) ∘
            (↑(extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).symm : ℂ × ℂ → ℂ × ℂ))
        ((extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).target ∩
          (↑(extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).symm : ℂ × ℂ → ℂ × ℂ) ⁻¹'
            (fun (z : ℂ × ℂ) ↦ z.1 * z.2) ⁻¹' (extChartAt 𝓘(ℝ, ℂ) y).source)

Tactic:
⟨continuous_mul, fun x y => contDiff_mul.contDiffOn⟩

Premises used: ContDiff.contDiffOn, continuous_mul, And.intro, contDiff_mul
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : Circle → ℂ := Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
⊢ (Continuous (Y := ℂ) fun (z : ℂ × ℂ) ↦ z.1 * z.2) ∧
    ∀ (x : ℂ × ℂ) (y : ℂ),
      ContDiffOn ℝ ω
        ((↑(extChartAt 𝓘(ℝ, ℂ) y) : ℂ → ℂ) ∘
          (fun (z : ℂ × ℂ) ↦ z.1 * z.2) ∘
            (↑(extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).symm : ℂ × ℂ → ℂ × ℂ))
        ((extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).target ∩
          (↑(extChartAt (ModelWithCorners.prod 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)) x).symm : ℂ × ℂ → ℂ × ℂ) ⁻¹'
            (fun (z : ℂ × ℂ) ↦ z.1 * z.2) ⁻¹' (extChartAt 𝓘(ℝ, ℂ) y).source)

Tactic:
exact ⟨continuous_mul, fun x y => contDiff_mul.contDiffOn⟩