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
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
h₁ :
  Set.codRestrict f (sphere 0 1) hf' ⁻¹' PartialEquiv.source (β := EuclideanSpace ℝ (Fin n)) (extChartAt (𝓡 n) v) =
    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)
⊢ 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))

Tactic:
convert! (H₁.of_le le_top).comp' H₂ using 1

Premises used: ContMDiffOn.of_le, ContMDiffOn.comp', le_top
-- 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
h₁ :
  ∀ (x : M),
    x ∈
        Set.codRestrict f (sphere 0 1) hf' ⁻¹'
          PartialEquiv.source (β := EuclideanSpace ℝ (Fin n)) (extChartAt (𝓡 n) v) ↔
      x ∈
        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)
⊢ Set.codRestrict f (sphere 0 1) hf' ⁻¹' PartialEquiv.source (β := EuclideanSpace ℝ (Fin n)) (extChartAt (𝓡 n) v) =
    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:
ext x
-- 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
x : M
⊢ ‖f x‖ = 1

Tactic:
simpa using hf' x
-- 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
x : M
⊢ ‖f x‖ = 1

Tactic:
have hfx : ‖f x‖ = 1 := by simpa using hf' x
-- 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
x : M
hfx : ‖f x‖ = 1
rw : ‖-(↑v : E)‖ = 1
⊢ f x = -(↑v : E) ↔ ⟪f x, -(↑v : E)⟫_ℝ = 1

Tactic:
rw [inner_eq_one_iff_of_norm_eq_one hfx]

Premises used: 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
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
x : M
hfx : ‖f x‖ = 1
⊢ ‖-(↑v : E)‖ = 1

Tactic:
norm_eq_of_mem_sphere (-v)

Premises used: norm_eq_of_mem_sphere, 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)
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
x : M
hfx : ‖f x‖ = 1
⊢ ‖-(↑v : E)‖ = 1

Tactic:
exact norm_eq_of_mem_sphere (-v)

Premises used: norm_eq_of_mem_sphere, 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)
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
x : M
⊢ f x = -(↑v : E) ↔ ⟪f x, -(↑v : E)⟫_ℝ = 1

Tactic:
have hfxv : f x = -↑v ↔ ⟪f x, -↑v⟫_ℝ = 1 := by
    have hfx : ‖f x‖ = 1 := by simpa using hf' x
    rw [inner_eq_one_iff_of_norm_eq_one hfx]
    exact norm_eq_of_mem_sphere (-v)
-- 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
x : M
hfxv : f x = -(↑v : E) ↔ ⟪f x, -(↑v : E)⟫_ℝ = 1
⊢ x ∈ Set.codRestrict f (sphere 0 1) hf' ⁻¹' PartialEquiv.source (β := EuclideanSpace ℝ (Fin n)) (extChartAt (𝓡 n) v) ↔
    x ∈
      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:
simp [chartAt, ChartedSpace.chartAt, Subtype.ext_iff, hfxv, real_inner_comm]

Premises used: chartAt, ChartedSpace.chartAt, Subtype.ext_iff, real_inner_comm
-- 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)
hf :
  ContMDiff (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) 𝓘(ℝ, E) (M' := E) m fun (x : (↑(sphere 0 1) : Type u_1)) ↦ -(↑x : E)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' :=
    (↑(sphere 0 1) : Type u_1)) m fun (x : (↑(sphere 0 1) : Type u_1)) ↦ -x

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
m : ℕ∞ω
n : ℕ
inst_2 : Fact (finrank ℝ E = n + 1)
apply :
  ContMDiff (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M := (↑(sphere 0 1) : Type u_1)) 𝓘(ℝ, E) m
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x))
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) 𝓘(ℝ, E) (M' := E) m fun (x : (↑(sphere 0 1) : Type u_1)) ↦ -(↑x : E)

Tactic:
apply contDiff_neg.contMDiff.comp _

Premises used: ContMDiff.comp, ContDiff.contMDiff, contDiff_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)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M := (↑(sphere 0 1) : Type u_1)) 𝓘(ℝ, E) m
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x))

Tactic:
contMDiff_coe_sphere

Premises used: Set.Mem, contMDiff_coe_sphere
-- 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)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M := (↑(sphere 0 1) : Type u_1)) 𝓘(ℝ, E) m
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x))

Tactic:
exact contMDiff_coe_sphere

Premises used: contMDiff_coe_sphere
-- 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)
dsimp :
  Eq (α := EuclideanSpace ℝ (Fin n))
    (((OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯) :
            ↥(ℝ ∙ -(↑v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) :
          (a : ↥(ℝ ∙ -(↑v : E))ᗮ) → EuclideanSpace ℝ (Fin n))
        ((↑(stereographic ⋯) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ -(↑v : E))ᗮ) v) :
      EuclideanSpace ℝ (Fin n))
    (0 : EuclideanSpace ℝ (Fin n))
⊢ (↑(stereographic' n (-v)) : (↑(sphere 0 1) : Type u_1) → EuclideanSpace ℝ (Fin n)) v = 0

Tactic:
dsimp [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)
simp : Eq (α := ↥(ℝ ∙ -(↑v : E))ᗮ) ((↑(stereographic ⋯) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ -(↑v : E))ᗮ) v) 0
⊢ Eq (α := EuclideanSpace ℝ (Fin n))
    (((OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯) :
            ↥(ℝ ∙ -(↑v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) :
          (a : ↥(ℝ ∙ -(↑v : E))ᗮ) → EuclideanSpace ℝ (Fin n))
        ((↑(stereographic ⋯) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ -(↑v : E))ᗮ) v) :
      EuclideanSpace ℝ (Fin n))
    (0 : EuclideanSpace ℝ (Fin n))

Tactic:
simp only [EmbeddingLike.map_eq_zero_iff]

Premises used: EmbeddingLike.map_eq_zero_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)
⊢ Eq (α := ↥(ℝ ∙ -(↑v : E))ᗮ) ((↑(stereographic ⋯) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ -(↑v : E))ᗮ) v) 0

Tactic:
apply stereographic_neg_apply

Premises used: stereographic_neg_apply
-- 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 :
  Eq (α := Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (LinearMap.range (M := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)
      (↑(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)) :
        TangentSpace (𝓡 n) v →ₗ[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (ℝ ∙ (↑v : E))ᗮ
⊢ Eq (α := Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (LinearMap.range (M := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)
      (↑(mfderiv% (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x)) v) :
        TangentSpace (𝓡 n) v →ₗ[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : 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)
dsimp :
  Eq (α := Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (LinearMap.range (M := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)
      (↑(fderivWithin ℝ
            (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 }))
            (Set.range id) ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v)) :
        TangentSpace (𝓡 n) v →ₗ[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (ℝ ∙ (↑v : E))ᗮ
⊢ Eq (α := Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (LinearMap.range (M := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)
      (↑(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)) :
        TangentSpace (𝓡 n) v →ₗ[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (ℝ ∙ (↑v : E))ᗮ

Tactic:
dsimp [chartAt]

Premises used: chartAt
-- 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 :
  Eq (α := Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (LinearMap.range (M := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)
      (↑(fderiv ℝ
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) ∘
              (↑(OpenPartialHomeomorph.symm (ChartedSpace.chartAt v)) :
                EuclideanSpace ℝ (Fin n) → { x : E // x ∈ sphere 0 1 }))
            ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v)) :
        TangentSpace (𝓡 n) v →ₗ[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (ℝ ∙ (↑v : E))ᗮ
⊢ Eq (α := Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (LinearMap.range (M := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)
      (↑(fderivWithin ℝ
            (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 }))
            (Set.range id) ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v)) :
        TangentSpace (𝓡 n) v →ₗ[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)))
    (ℝ ∙ (↑v : E))ᗮ

Tactic:
simp only [fderivWithin_univ, mfld_simps]

Premises used: 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 :
  Eq (α := Submodule ℝ E)
    (LinearMap.range (M := EuclideanSpace ℝ (Fin n))
      (↑(fderiv ℝ
            (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
              (stereoInvFunAux (-(↑v : E)) ∘
                Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
            0) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E))
    (ℝ ∙ (↑v : E))ᗮ
⊢ Eq (α := Submodule ℝ E)
    (LinearMap.range (M := EuclideanSpace ℝ (Fin n))
      (↑(fderiv ℝ
            (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
              (stereoInvFunAux (-(↑v : E)) ∘
                Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
              (⇑U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
            0) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E))
    (ℝ ∙ (↑v : E))ᗮ

Tactic:
this