awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
hv' : Membership.mem (γ := Set E) (sphere 0 1) v
⊢ Set.range (ι := ↥(ℝ ∙ v)ᗮ)
      (↑(OpenPartialHomeomorph.symm (stereographic hv)) : ↥(ℝ ∙ v)ᗮ → (↑(sphere 0 1) : Type u_1)) =
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v hv'}ᶜ
have refine : Set.range (ι := ↥(ℝ ∙ v)ᗮ) (↑(OpenPartialHomeomorph.symm (stereographic hv)) : ↥(ℝ ∙ v)ᗮ → (↑(sphere 0 1) : Type u_1)) ≤
  {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v hv'}ᶜ
Tactic: refine le_antisymm ?_ (stereographic hv).symm.target_subset_range
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
hv' : Membership.mem (γ := Set E) (sphere 0 1) v
y : ↥(ℝ ∙ v)ᗮ
⊢ Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v hv'}ᶜ
    ((↑(OpenPartialHomeomorph.symm (stereographic hv)) : ↥(ℝ ∙ v)ᗮ → (↑(sphere 0 1) : Type u_1)) y)
have suffices : Membership.mem (γ := Set ↥(ℝ ∙ v)ᗮ) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (stereographic hv))) y
Tactic: suffices y ∈ (stereographic hv).target from (fun _ ↦ (stereographic hv).map_target) y this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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 ⋯)
⊢ ContDiffOn ℝ ω
    ((↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ∘
      (↑((stereographic' n v).symm ≫ₕ stereographic' n v') : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ∘
        (↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
    ((↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ⁻¹'
        ((stereographic' n v).symm ≫ₕ stereographic' n v').source ∩
      Set.range (↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
have 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 : ℝ)}
Tactic: have H₁ := U'.contDiff.comp_contDiffOn (contDiffOn_stereoToFun (n := ω))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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 : ℝ)}
⊢ ContDiffOn ℝ ω
    ((↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ∘
      (↑((stereographic' n v).symm ≫ₕ stereographic' n v') : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ∘
        (↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
    ((↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ⁻¹'
        ((stereographic' n v).symm ≫ₕ stereographic' n v').source ∩
      Set.range (↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
have 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))ᗮ))
Tactic: have H₂ := (contDiff_stereoInvFunAux (m := ω) (v := v.val) |>.comp
        (ℝ ∙ (v : E))ᗮ.subtypeL.contDiff).comp U.symm.contDiff
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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))ᗮ))
⊢ ContDiffOn ℝ ω
    ((↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ∘
      (↑((stereographic' n v).symm ≫ₕ stereographic' n v') : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ∘
        (↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
    ((↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ⁻¹'
        ((stereographic' n v).symm ≫ₕ stereographic' n v').source ∩
      Set.range (↑(𝓡 n) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)))
have h : (↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ⁻¹'
      ((stereographic' n v).symm ≫ₕ stereographic' n v').source ∩
    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: convert! H₁.comp_inter (H₂.contDiffOn : ContDiffOn ℝ ω _ Set.univ) using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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))ᗮ))
⊢ (↑(ModelWithCorners.symm (𝓡 n)) : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) ⁻¹'
        ((stereographic' n v).symm ≫ₕ stereographic' n v').source ∩
      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 : ℝ)}
have h : (↑(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 [OpenPartialHomeomorph.trans_toPartialEquiv,
        OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source,
        PartialEquiv.symm_source, stereographic'_target, stereographic'_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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))ᗮ))
⊢ (↑(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 : ℝ)}
have 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 : ℝ)}
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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) |
      (↑(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 : ℝ)}
have 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}
Tactic: simp only [id, comp_apply, OpenPartialHomeomorph.coe_coe_symm,
        innerSL_apply_apply, Ne, sphere_ext_iff, real_inner_comm (v' : E)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
⊢ 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))
have 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)
Tactic: rw [contMDiff_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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)) ∧
    ∀ (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)
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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))
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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)
⊢ ContMDiff I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) m (Set.codRestrict f (sphere 0 1) hf')
have 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))
Tactic: rw [contMDiff_iff_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (goal)
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))
have 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))
Tactic: refine ⟨continuous_induced_rng.2 hf.continuous, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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 ⋯)
⊢ ContMDiffOn I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) m
    ((↑(extChartAt (𝓡 n) v) : (↑(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) v))
have h : 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Instances.Sphere (hypothesis)
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 I (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' := EuclideanSpace ℝ (Fin n)) m
    ((↑(extChartAt (𝓡 n) v) : (↑(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) v))
have 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)
Tactic: have H₁ := (h.comp_inter contDiffOn_stereoToFun).contMDiffOn