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 v' : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
U' : ↥(ℝ ∙ (↑v' : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
H₁ :
  ContDiffOn ℝ (F := EuclideanSpace ℝ (Fin n)) ω
    (comp (β := ↥(ℝ ∙ (↑v' : E))ᗮ) (⇑U' : (a : ↥(ℝ ∙ (↑v' : E))ᗮ) → EuclideanSpace ℝ (Fin n)) (stereoToFun (↑v' : E)))
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑v' : E) : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
H₂ :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin n)) ω
    (comp (β := ↥(ℝ ∙ (↑v : E))ᗮ)
      (stereoInvFunAux (↑v : E) ∘ (⇑(Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ) : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E))
      (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ))
h :
  Eq (α := Set (EuclideanSpace ℝ (Fin n)))
    {a : EuclideanSpace ℝ (Fin n) |
      (↑(stereographic' n v).symm : EuclideanSpace ℝ (Fin n) → (↑(sphere 0 1) : Type u_1)) (id a) ≠ v'}
    {a : EuclideanSpace ℝ (Fin n) |
      Ne (α := ℝ)
        ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑v' : E) : E →L[ℝ] ℝ) : (a : E) → ℝ)
            (comp (β := ↥(ℝ ∙ (↑v : E))ᗮ)
              (stereoInvFunAux (↑v : E) ∘ (⇑(Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ) : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) a) :
          ℝ)
        (1 : ℝ)}
⊢ (↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ⁻¹'
        (Set.univ ∩ (↑(stereographic' n v).symm : EuclideanSpace ℝ (Fin n) → (↑(sphere 0 1) : Type u_1)) ⁻¹' {v'}ᶜ) ∩
      Set.range (↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) =
    Set.univ ∩
      comp (β := ↥(ℝ ∙ (↑v : E))ᗮ)
          (stereoInvFunAux (↑v : E) ∘ (⇑(Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ) : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E))
          (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) ⁻¹'
        {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑v' : E) : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}

Tactic:
simp only [modelWithCornersSelf_coe, modelWithCornersSelf_coe_symm,
        Set.range_id, Set.inter_univ, Set.univ_inter, Set.compl_singleton_eq, Set.preimage_setOf_eq]

Premises used: modelWithCornersSelf_coe_symm, Set.inter_univ, Set.univ_inter, Set.preimage_setOf_eq, Set.range_id, Set.compl_singleton_eq, modelWithCornersSelf_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 v' : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
U' : ↥(ℝ ∙ (↑v' : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
H₁ :
  ContDiffOn ℝ (F := EuclideanSpace ℝ (Fin n)) ω
    (comp (β := ↥(ℝ ∙ (↑v' : E))ᗮ) (⇑U' : (a : ↥(ℝ ∙ (↑v' : E))ᗮ) → EuclideanSpace ℝ (Fin n)) (stereoToFun (↑v' : E)))
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑v' : E) : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
H₂ :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin n)) ω
    (comp (β := ↥(ℝ ∙ (↑v : E))ᗮ)
      (stereoInvFunAux (↑v : E) ∘ (⇑(Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ) : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E))
      (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ))
h :
  Eq (α := Set (EuclideanSpace ℝ (Fin n)))
    {a : EuclideanSpace ℝ (Fin n) |
      ¬⟪(↑v' : E), (↑((↑(stereographic' n v).symm : EuclideanSpace ℝ (Fin n) → (↑(sphere 0 1) : Type u_1)) a) : E)⟫_ℝ =
          1}
    {a : EuclideanSpace ℝ (Fin n) |
      ¬⟪(↑v' : E),
            stereoInvFunAux (↑v : E)
              ((Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E)
                ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) a : ↥(ℝ ∙ (↑v : E))ᗮ))⟫_ℝ =
          1}
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin n)))
    {a : EuclideanSpace ℝ (Fin n) |
      (↑(stereographic' n v).symm : EuclideanSpace ℝ (Fin n) → (↑(sphere 0 1) : Type u_1)) (id a) ≠ v'}
    {a : EuclideanSpace ℝ (Fin n) |
      Ne (α := ℝ)
        ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑v' : E) : E →L[ℝ] ℝ) : (a : E) → ℝ)
            (comp (β := ↥(ℝ ∙ (↑v : E))ᗮ)
              (stereoInvFunAux (↑v : E) ∘ (⇑(Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ) : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) a) :
          ℝ)
        (1 : ℝ)}

Tactic:
simp only [id, comp_apply, OpenPartialHomeomorph.coe_coe_symm,
        innerSL_apply_apply, Ne, sphere_ext_iff, real_inner_comm (v' : E)]

Premises used: innerSL_apply_apply, id, Ne, Function.comp_apply, sphere_ext_iff, Subtype.val, OpenPartialHomeomorph.coe_coe_symm, real_inner_comm
-- 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 v' : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
U' : ↥(ℝ ∙ (↑v' : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
H₁ :
  ContDiffOn ℝ (F := EuclideanSpace ℝ (Fin n)) ω
    (comp (β := ↥(ℝ ∙ (↑v' : E))ᗮ) (⇑U' : (a : ↥(ℝ ∙ (↑v' : E))ᗮ) → EuclideanSpace ℝ (Fin n)) (stereoToFun (↑v' : E)))
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑v' : E) : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)}
H₂ :
  ContDiff ℝ (E := EuclideanSpace ℝ (Fin n)) ω
    (comp (β := ↥(ℝ ∙ (↑v : E))ᗮ)
      (stereoInvFunAux (↑v : E) ∘ (⇑(Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ) : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E))
      (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ))
⊢ Eq (α := Set (EuclideanSpace ℝ (Fin n)))
    {a : EuclideanSpace ℝ (Fin n) |
      ¬⟪(↑v' : E), (↑((↑(stereographic' n v).symm : EuclideanSpace ℝ (Fin n) → (↑(sphere 0 1) : Type u_1)) a) : E)⟫_ℝ =
          1}
    {a : EuclideanSpace ℝ (Fin n) |
      ¬⟪(↑v' : E),
            stereoInvFunAux (↑v : E)
              ((Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E)
                ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) a : ↥(ℝ ∙ (↑v : E))ᗮ))⟫_ℝ =
          1}

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
⊢ IsManifold (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) ω (↑(sphere 0 1) : Type)

Tactic:
haveI := Fact.mk (@finrank_euclideanSpace_fin ℝ _ (n + 1))
  EuclideanSpace.instIsManifoldSphere

Premises used: Set.Mem, EuclideanSpace.instIsManifoldSphere
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
rw :
  Continuous.{u_1, u_1} (X := { x : E // Membership.mem (γ := Set E) (sphere 0 1) x })
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x)) ∧
    ∀ (x : { x : E // Membership.mem (γ := Set E) (sphere 0 1) x }) (y : E),
      ContDiffOn ℝ (E := EuclideanSpace ℝ (Fin n)) m
        ((↑(extChartAt 𝓘(ℝ, E) y) : E → E) ∘
          Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
            (↑(PartialEquiv.symm (extChartAt (𝓡 n) x)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
        (PartialEquiv.target (extChartAt (𝓡 n) x) ∩
          (↑(PartialEquiv.symm (extChartAt (𝓡 n) x)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }) ⁻¹'
            Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ⁻¹'
              (extChartAt 𝓘(ℝ, E) y).source)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M := { x : E // Membership.mem (γ := Set E) (sphere 0 1) x }) 𝓘(ℝ, E)
    m (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x))

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
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
left :
  Continuous.{u_1, u_1} (X := { x : E // Membership.mem (γ := Set E) (sphere 0 1) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x))
right :
  ∀ (x : { x : E // Membership.mem (γ := Set E) (sphere 0 1) x }) (y : E),
    ContDiffOn ℝ (E := EuclideanSpace ℝ (Fin n)) m
      ((↑(extChartAt 𝓘(ℝ, E) y) : E → E) ∘
        Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
          (↑(PartialEquiv.symm (extChartAt (𝓡 n) x)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
      (PartialEquiv.target (extChartAt (𝓡 n) x) ∩
        (↑(PartialEquiv.symm (extChartAt (𝓡 n) x)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }) ⁻¹'
          Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)
⊢ Continuous.{u_1, u_1} (X := { x : E // Membership.mem (γ := Set E) (sphere 0 1) x })
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x)) ∧
    ∀ (x : { x : E // Membership.mem (γ := Set E) (sphere 0 1) x }) (y : E),
      ContDiffOn ℝ (E := EuclideanSpace ℝ (Fin n)) m
        ((↑(extChartAt 𝓘(ℝ, E) y) : E → E) ∘
          Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
            (↑(PartialEquiv.symm (extChartAt (𝓡 n) x)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
        (PartialEquiv.target (extChartAt (𝓡 n) x) ∩
          (↑(PartialEquiv.symm (extChartAt (𝓡 n) x)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }) ⁻¹'
            Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ⁻¹'
              (extChartAt 𝓘(ℝ, E) y).source)

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
⊢ Continuous.{u_1, u_1} (X := { x : E // Membership.mem (γ := Set E) (sphere 0 1) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x))

Tactic:
continuous_subtype_val

Premises used: continuous_subtype_val
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
⊢ Continuous.{u_1, u_1} (X := { x : E // Membership.mem (γ := Set E) (sphere 0 1) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x))

Tactic:
exact continuous_subtype_val

Premises used: continuous_subtype_val
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : { x : E // Membership.mem (γ := Set E) (sphere 0 1) x }
right :
  ∀ (y : E),
    ContDiffOn ℝ (E := EuclideanSpace ℝ (Fin n)) m
      ((↑(extChartAt 𝓘(ℝ, E) y) : E → E) ∘
        Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
          (↑(PartialEquiv.symm (extChartAt (𝓡 n) v)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
      (PartialEquiv.target (extChartAt (𝓡 n) v) ∩
        (↑(PartialEquiv.symm (extChartAt (𝓡 n) v)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }) ⁻¹'
          Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)
⊢ ∀ (y : E),
    ContDiffOn ℝ (E := EuclideanSpace ℝ (Fin n)) m
      ((↑(extChartAt 𝓘(ℝ, E) y) : E → E) ∘
        Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
          (↑(PartialEquiv.symm (extChartAt (𝓡 n) v)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
      (PartialEquiv.target (extChartAt (𝓡 n) v) ∩
        (↑(PartialEquiv.symm (extChartAt (𝓡 n) v)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }) ⁻¹'
          Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)

Tactic:
_
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : { x : E // Membership.mem (γ := Set E) (sphere 0 1) x }
y : E
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
⊢ ContDiffOn ℝ (E := EuclideanSpace ℝ (Fin n)) m
    ((↑(extChartAt 𝓘(ℝ, E) y) : E → E) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
        (↑(PartialEquiv.symm (extChartAt (𝓡 n) v)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
    (PartialEquiv.target (extChartAt (𝓡 n) v) ∩
      (↑(PartialEquiv.symm (extChartAt (𝓡 n) v)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }) ⁻¹'
        Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)

Tactic:
((contDiff_stereoInvFunAux.comp (ℝ ∙ (-v : E))ᗮ.subtypeL.contDiff).comp
          U.symm.contDiff).contDiffOn

Premises used: Submodule.subtypeL, Real, LinearIsometryEquiv.symm, ContDiff.contDiffOn, Set.Mem, setOf, LinearIsometryEquiv.contDiff, Submodule.orthogonal, ContDiff.comp, contDiff_stereoInvFunAux, Submodule.span, stereoInvFunAux, ContinuousLinearMap.contDiff, Singleton.singleton, Subtype.val, Neg.neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
v : { x : E // Membership.mem (γ := Set E) (sphere 0 1) x }
y : E
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
⊢ ContDiffOn ℝ (E := EuclideanSpace ℝ (Fin n)) m
    ((↑(extChartAt 𝓘(ℝ, E) y) : E → E) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
        (↑(PartialEquiv.symm (extChartAt (𝓡 n) v)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
    (PartialEquiv.target (extChartAt (𝓡 n) v) ∩
      (↑(PartialEquiv.symm (extChartAt (𝓡 n) v)) : EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }) ⁻¹'
        Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)

Tactic:
exact
      ((contDiff_stereoInvFunAux.comp (ℝ ∙ (-v : E))ᗮ.subtypeL.contDiff).comp
          U.symm.contDiff).contDiffOn

Premises used: Submodule.subtypeL, Real, LinearIsometryEquiv.symm, ContDiff.contDiffOn, LinearIsometryEquiv.contDiff, Submodule.orthogonal, ContDiff.comp, contDiff_stereoInvFunAux, Submodule.span, ContinuousLinearMap.contDiff, Singleton.singleton, Subtype.val, Neg.neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I m M
n : ℕ
inst_8 : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), Membership.mem (γ := Set E) (sphere 0 1) (f x)
rw :
  Continuous (Set.codRestrict f (sphere 0 1) hf') ∧
    ∀ (y : (↑(sphere 0 1) : Type u_1)),
      ContMDiffOn I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) m
        ((↑(extChartAt (𝓡 n) y) : (↑(sphere 0 1) : Type u_1) → EuclideanSpace ℝ (Fin n)) ∘
          Set.codRestrict f (sphere 0 1) hf')
        (Set.codRestrict f (sphere 0 1) hf' ⁻¹'
          PartialEquiv.source (β := EuclideanSpace ℝ (Fin n)) (extChartAt (𝓡 n) y))
⊢ ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) m (Set.codRestrict f (sphere 0 1) hf')

Tactic:
rw [contMDiff_iff_target]

Premises used: contMDiff_iff_target
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I m M
n : ℕ
inst_8 : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), Membership.mem (γ := Set E) (sphere 0 1) (f x)
⊢ Continuous (Set.codRestrict f (sphere 0 1) hf') ∧
    ∀ (y : (↑(sphere 0 1) : Type u_1)),
      ContMDiffOn I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) m
        ((↑(extChartAt (𝓡 n) y) : (↑(sphere 0 1) : Type u_1) → EuclideanSpace ℝ (Fin n)) ∘
          Set.codRestrict f (sphere 0 1) hf')
        (Set.codRestrict f (sphere 0 1) hf' ⁻¹'
          PartialEquiv.source (β := EuclideanSpace ℝ (Fin n)) (extChartAt (𝓡 n) y))

Tactic:
⟨continuous_induced_rng.2 hf.continuous, ?_⟩

Premises used: Iff.mpr, ContMDiff.continuous, And.intro, continuous_induced_rng
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I m M
n : ℕ
inst_8 : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), Membership.mem (γ := Set E) (sphere 0 1) (f x)
refine :
  ∀ (y : (↑(sphere 0 1) : Type u_1)),
    ContMDiffOn I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) m
      ((↑(extChartAt (𝓡 n) y) : (↑(sphere 0 1) : Type u_1) → EuclideanSpace ℝ (Fin n)) ∘
        Set.codRestrict f (sphere 0 1) hf')
      (Set.codRestrict f (sphere 0 1) hf' ⁻¹' PartialEquiv.source (β := EuclideanSpace ℝ (Fin n)) (extChartAt (𝓡 n) y))
⊢ Continuous (Set.codRestrict f (sphere 0 1) hf') ∧
    ∀ (y : (↑(sphere 0 1) : Type u_1)),
      ContMDiffOn I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) m
        ((↑(extChartAt (𝓡 n) y) : (↑(sphere 0 1) : Type u_1) → EuclideanSpace ℝ (Fin n)) ∘
          Set.codRestrict f (sphere 0 1) hf')
        (Set.codRestrict f (sphere 0 1) hf' ⁻¹'
          PartialEquiv.source (β := EuclideanSpace ℝ (Fin n)) (extChartAt (𝓡 n) y))

Tactic:
refine ⟨continuous_induced_rng.2 hf.continuous, ?_⟩
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I m M
n : ℕ
inst_8 : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), Membership.mem (γ := Set E) (sphere 0 1) (f x)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
⊢ ContDiffOn ℝ (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (F := EuclideanSpace ℝ (Fin n)) ω
    (⇑U : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → EuclideanSpace ℝ (Fin n)) Set.univ

Tactic:
have h : ContDiffOn ℝ ω _ Set.univ := U.contDiff.contDiffOn
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I m M
n : ℕ
inst_8 : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), Membership.mem (γ := Set E) (sphere 0 1) (f x)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
h :
  ContDiffOn ℝ (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (F := EuclideanSpace ℝ (Fin n)) ω
    (⇑U : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → EuclideanSpace ℝ (Fin n)) Set.univ
⊢ ContMDiffOn 𝓘(ℝ, E) (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) ω
    (Function.comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (⇑U : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → EuclideanSpace ℝ (Fin n))
      (stereoToFun (↑(-v) : E)))
    ({x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑(-v) : E) : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} ∩
      Set.preimage (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (stereoToFun (↑(-v) : E)) Set.univ)

Tactic:
have H₁ := (h.comp_inter contDiffOn_stereoToFun).contMDiffOn
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I m M
n : ℕ
inst_8 : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), Membership.mem (γ := Set E) (sphere 0 1) (f x)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
h :
  ContDiffOn ℝ (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (F := EuclideanSpace ℝ (Fin n)) ω
    (⇑U : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → EuclideanSpace ℝ (Fin n)) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) ω
    (Function.comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (⇑U : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → EuclideanSpace ℝ (Fin n))
      (stereoToFun (↑(-v) : E)))
    ({x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑(-v) : E) : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} ∩
      Set.preimage (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (stereoToFun (↑(-v) : E)) Set.univ)
⊢ ContMDiffOn I 𝓘(ℝ, E) m f Set.univ

Tactic:
have H₂ : CMDiff[Set.univ] m f := hf.contMDiffOn
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type u_3
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I m M
n : ℕ
inst_8 : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), Membership.mem (γ := Set E) (sphere 0 1) (f x)
v : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
h :
  ContDiffOn ℝ (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (F := EuclideanSpace ℝ (Fin n)) ω
    (⇑U : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → EuclideanSpace ℝ (Fin n)) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) ω
    (Function.comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (⇑U : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → EuclideanSpace ℝ (Fin n))
      (stereoToFun (↑(-v) : E)))
    ({x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑(-v) : E) : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} ∩
      Set.preimage (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (stereoToFun (↑(-v) : E)) Set.univ)
H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ
⊢ ContMDiffOn I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) m
    (Function.comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (⇑U : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → EuclideanSpace ℝ (Fin n))
        (stereoToFun (↑(-v) : E)) ∘
      f)
    (Set.univ ∩
      f ⁻¹'
        ({x : E |
            Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (↑(-v) : E) : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} ∩
          Set.preimage (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (stereoToFun (↑(-v) : E)) Set.univ))

Tactic:
(H₁.of_le le_top).comp' H₂

Premises used: ContMDiffOn.of_le, ContMDiffOn.comp', le_top