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
v : E
hv : ‖v‖ = 1
⊢ ∀ ⦃x : (↑(sphere 0 1) : Type u_1)⦄,
    Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
        {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x →
      Membership.mem (γ := Set ↥(ℝ ∙ v)ᗮ) Set.univ
        ((stereoToFun v ∘ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x)) x)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h : (↑x : E) = v
⊢ ‖(↑x : E)‖ = 1

Tactic:
rw [← h] at hv
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h : (↑x : E) = v
hv₁ : ‖(↑x : E)‖ = 1
⊢ Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x

Tactic:
rw [← h] at hv
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hx :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h : (↑x : E) = v
hv₁ : ‖(↑x : E)‖ = 1
hx₁ :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
⊢ (↑x : E) = v

Tactic:
rw [← h] at hv
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv_1 : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hv : ‖(↑x : E)‖ = 1
hx :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h : (↑x : E) = v
a : (↑x : E) = (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯) : E)
⊢ Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯} x

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv_1 : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hv : ‖(↑x : E)‖ = 1
hx :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h a : (↑x : E) = v
⊢ (↑x : E) = (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯) : E)

Tactic:
dsimp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv_1 : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hv : ‖(↑x : E)‖ = 1
hx :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h : (↑x : E) = v
⊢ (↑x : E) = v

Tactic:
h
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv_1 : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
hv : ‖(↑x : E)‖ = 1
hx :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ x
h : (↑x : E) = v
⊢ (↑x : E) = v

Tactic:
exact h
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : (↑(sphere 0 1) : Type u_1)
h :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ w
dsimp : ¬⟪v, (↑w : E)⟫ = 1
⊢ Membership.mem (γ := Set E)
    {x : E | Ne (α := ℝ) ((((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) v : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (1 : ℝ)} (↑w : E)

Tactic:
dsimp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : (↑(sphere 0 1) : Type u_1)
h :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ w
⊢ ‖(↑w : E)‖ = 1

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : (↑(sphere 0 1) : Type u_1)
h :
  Membership.mem (γ := Set (↑(sphere 0 1) : Type u_1))
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ w
⊢ ¬⟪v, (↑w : E)⟫ = 1

Tactic:
exact
        h ∘ Subtype.ext ∘ Eq.symm ∘ (inner_eq_one_iff_of_norm_eq_one hv (by simp)).mp

Premises used: inner_eq_one_iff_of_norm_eq_one, Iff.mp, Eq.symm, Subtype.ext
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : (↑(sphere 0 1) : Type u_1)
⊢ (↑(stereographic hv) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ v)ᗮ) x =
    HSMul.hSMul (β := ↥(ℝ ∙ v)ᗮ) (2 / (1 - ⟪v, (↑x : E)⟫))
      ((Submodule.orthogonalProjection (ℝ ∙ v)ᗮ : (a : E) → ↥(ℝ ∙ v)ᗮ) (↑x : E) : ↥(ℝ ∙ v)ᗮ)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', stereoToFun, rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
⊢ PartialEquiv.source (β := ↥(ℝ ∙ v)ᗮ) (OpenPartialHomeomorph.toPartialEquiv (stereographic hv)) =
    {Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) v ⋯}ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
⊢ Eq (α := Set ↥(ℝ ∙ v)ᗮ) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (stereographic hv))) Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : (↑(sphere 0 1) : Type u_1)
⊢ Eq (α := ↥(ℝ ∙ (↑v : E))ᗮ) ((↑(stereographic ⋯) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ (↑v : E))ᗮ) (-v)) 0

Tactic:
simp [stereographic_apply, Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero]

Premises used: stereographic_apply, Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : (↑(sphere 0 1) : Type u_1)
⊢ Eq (α := ↥(ℝ ∙ (↑(-v) : E))ᗮ) ((↑(stereographic ⋯) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) (- -v)) 0

Tactic:
stereographic_apply_neg (-v)

Premises used: stereographic_apply_neg, Neg.neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : (↑(sphere 0 1) : Type u_1)
h : v = - -v
⊢ Eq (α := ↥(ℝ ∙ (↑(-v) : E))ᗮ) ((↑(stereographic ⋯) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) v) 0

Tactic:
convert! stereographic_apply_neg (-v)

Premises used: stereographic_apply_neg, Neg.neg
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : (↑(sphere 0 1) : Type u_1)
h : (↑v : E) = (↑(- -v) : E)
⊢ v = - -v

Tactic:
ext1
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : (↑(sphere 0 1) : Type u_1)
⊢ (↑v : E) = (↑(- -v) : E)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
⊢ Surjective (β := ↥(ℝ ∙ v)ᗮ) (↑(stereographic hv) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ v)ᗮ)

Tactic:
(stereographic hv).surjective_of_target_eq_univ rfl

Premises used: stereographic, OpenPartialHomeomorph.toFun', PartialEquiv.surjective_of_target_eq_univ, OpenPartialHomeomorph.toPartialEquiv, rfl
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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'}ᶜ

Tactic:
le_antisymm ?_ (stereographic hv).symm.target_subset_range

Premises used: stereographic, PartialEquiv.target_subset_range, le_antisymm, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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
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'}ᶜ
⊢ 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

Premises used: stereographic, PartialEquiv.target_subset_range, le_antisymm, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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)ᗮ
suffices :
  Membership.mem (γ := Set ↥(ℝ ∙ v)ᗮ) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (stereographic hv))) y
⊢ 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)

Tactic:
suffices y ∈ (stereographic hv).target from (fun _ ↦ (stereographic hv).map_target) y this
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
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 ↥(ℝ ∙ v)ᗮ) (PartialEquiv.target (OpenPartialHomeomorph.toPartialEquiv (stereographic hv))) y

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
⊢ Eq (α := Set ↥(ℝ ∙ v)ᗮ)
    (PartialEquiv.source (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (stereographic hv))))
    Set.univ

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)
⊢ (stereographic' n v).source = {v}ᶜ

Tactic:
simp [stereographic']

Premises used: stereographic'
-- 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)
⊢ (stereographic' n v).target = Set.univ

Tactic:
simp [stereographic']

Premises used: stereographic'
-- 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)
⊢ v ∈ (stereographic' n (-v)).source

Tactic:
simpa using ne_neg_of_mem_unit_sphere ℝ v

Premises used: Real, ne_neg_of_mem_unit_sphere
-- Module: Mathlib.Geometry.Manifold.Instances.Sphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
u v : (↑(sphere 0 1) : Type u_1)
⊢ u = v ↔ ⟪(↑u : E), (↑v : E)⟫_ℝ = 1

Tactic:
simp [Subtype.ext_iff, inner_eq_one_iff_of_norm_eq_one]

Premises used: Subtype.ext_iff, inner_eq_one_iff_of_norm_eq_one
-- 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)
x : EuclideanSpace ℝ (Fin n)
⊢ (↑((↑(stereographic' n v).symm : EuclideanSpace ℝ (Fin n) → (↑(sphere 0 1) : Type u_1)) x) : E) =
    let U : ↥(ℝ ∙ (↑v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
      OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯);
    (HPow.hPow (β := ℕ) (norm.{u_1} (E := E) (↑((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) x) : E))
              2 +
            4)⁻¹ •
        HSMul.hSMul (α := ℝ) (β := E) 4 (↑((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) x) : E) +
      (HPow.hPow (β := ℕ) (norm.{u_1} (E := E) (↑((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) x) : E))
              2 +
            4)⁻¹ •
        (HPow.hPow (β := ℕ)
              (norm.{u_1} (E := E) (↑((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ) x) : E)) 2 -
            4) •
          (↑v : E)

Tactic:
simp [stereographic, stereographic', ← Submodule.coe_norm]

Premises used: stereographic', stereographic, Submodule.coe_norm
-- 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 ⋯)
⊢ 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 := ω))
-- 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 : ℝ)}
⊢ 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
-- 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))ᗮ))
⊢ ContDiffOn ℝ (E := EuclideanSpace ℝ (Fin n)) (F := EuclideanSpace ℝ (Fin n)) ω
    (comp (β := ↥(ℝ ∙ (↑v' : E))ᗮ) (⇑U' : (a : ↥(ℝ ∙ (↑v' : E))ᗮ) → EuclideanSpace ℝ (Fin n)) (stereoToFun (↑v' : E)) ∘
      comp (β := ↥(ℝ ∙ (↑v : E))ᗮ)
        (stereoInvFunAux (↑v : E) ∘ (⇑(Submodule.subtypeL (ℝ ∙ (↑v : E))ᗮ) : (a : ↥(ℝ ∙ (↑v : E))ᗮ) → E))
        (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑v : E))ᗮ))
    (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:
H₁.comp_inter (H₂.contDiffOn : ContDiffOn ℝ ω _ Set.univ)

Premises used: ContDiff.contDiffOn, ContDiffOn.comp_inter
-- 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 :
  (↑(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 : ℝ)}
⊢ 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)))

Tactic:
convert! H₁.comp_inter (H₂.contDiffOn : ContDiffOn ℝ ω _ Set.univ) using 1

Premises used: ContDiff.contDiffOn, ContDiffOn.comp_inter
-- 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 :
  (↑(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 : ℝ)}
⊢ (↑(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:
simp only [OpenPartialHomeomorph.trans_toPartialEquiv,
        OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source,
        PartialEquiv.symm_source, stereographic'_target, stereographic'_source]

Premises used: OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source, stereographic'_source, stereographic'_target, OpenPartialHomeomorph.trans_toPartialEquiv, PartialEquiv.symm_source