awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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' := 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 I 𝓘(ℝ, E) m f Set.univ
Tactic: have H₂ : CMDiff[Set.univ] m f := hf.contMDiffOn
-- 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)
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
    ((↑(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₁ : 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: convert! (H₁.of_le le_top).comp' H₂ 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
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
⊢ 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)
have 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)
Tactic: ext x
-- 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
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
have hfx : ‖f x‖ = 1
Tactic: have hfx : ‖f x‖ = 1 := by simpa using hf' x
-- 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)
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
⊢ f x = -(↑v : E) ↔ ⟪f x, -(↑v : E)⟫_ℝ = 1
have rw : ‖-(↑v : E)‖ = 1
Tactic: rw [inner_eq_one_iff_of_norm_eq_one hfx]
-- 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
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
⊢ 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)
have hfxv : 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)
-- 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) (E' := EuclideanSpace ℝ (Fin n)) (𝓡 n) (M' :=
    (↑(sphere 0 1) : Type u_1)) m fun (x : (↑(sphere 0 1) : Type u_1)) ↦ -x
have hf : ContMDiff (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) 𝓘(ℝ, E) (M' := E) m fun (x : (↑(sphere 0 1) : Type u_1)) ↦ -(↑x : E)
Tactic: apply ContMDiff.codRestrict_sphere
-- 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) 𝓘(ℝ, E) (M' := E) m fun (x : (↑(sphere 0 1) : Type u_1)) ↦ -(↑x : E)
have 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))
Tactic: apply contDiff_neg.contMDiff.comp _
-- 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 : (↑(sphere 0 1) : Type u_1)
⊢ (↑(stereographic' n (-v)) : (↑(sphere 0 1) : Type u_1) → EuclideanSpace ℝ (Fin n)) v = 0
have dsimp : Eq (α := EuclideanSpace ℝ (Fin n))
  (((OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n sorry) :
          ↥(ℝ ∙ -(↑v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) :
        (a : ↥(ℝ ∙ -(↑v : E))ᗮ) → EuclideanSpace ℝ (Fin n))
      ((↑(stereographic sorry) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ -(↑v : E))ᗮ) v) :
    EuclideanSpace ℝ (Fin n))
  (0 : EuclideanSpace ℝ (Fin n))
Tactic: dsimp [stereographic']
-- 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 : (↑(sphere 0 1) : Type u_1)
⊢ 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))
have simp : Eq (α := ↥(ℝ ∙ -(↑v : E))ᗮ) ((↑(stereographic sorry) : (↑(sphere 0 1) : Type u_1) → ↥(ℝ ∙ -(↑v : E))ᗮ) v) 0
Tactic: simp only [EmbeddingLike.map_eq_zero_iff]
-- 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 : (↑(sphere 0 1) : Type u_1)
⊢ 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))ᗮ
have 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))ᗮ
Tactic: rw [((contMDiff_coe_sphere v).mdifferentiableAt one_ne_zero).mfderiv]
-- 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 : (↑(sphere 0 1) : Type u_1)
⊢ 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))ᗮ
have 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))ᗮ
Tactic: dsimp [chartAt]
-- 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 : (↑(sphere 0 1) : Type u_1)
⊢ 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))ᗮ
have 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))ᗮ
Tactic: simp only [fderivWithin_univ, mfld_simps]
-- 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 : (↑(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 ℝ (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))ᗮ
have h : Submodule ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E)) = Submodule ℝ E →
  TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v = EuclideanSpace ℝ (Fin n) →
    TangentSpace 𝓘(ℝ, E) (↑v : E) = E →
      HEq (α := AddCommMonoid (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)) AddCommGroup.toAddCommMonoid (β :=
          AddCommMonoid (EuclideanSpace ℝ (Fin n))) AddCommGroup.toAddCommMonoid →
        HEq.{u_1 + 1} (α := AddCommMonoid (TangentSpace 𝓘(ℝ, E) (↑v : E))) AddCommGroup.toAddCommMonoid (β :=
            AddCommMonoid E) AddCommGroup.toAddCommMonoid →
          HEq (α := Module ℝ (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v)) (instModuleTangentSpace (𝓡 n) v)
              (β := Module ℝ (EuclideanSpace ℝ (Fin n)))
              (WithLp.instModule 2 ℝ ((i : Fin n) → (fun (x : Fin n) ↦ ℝ) i)) →
            HEq (α := Module ℝ (TangentSpace 𝓘(ℝ, E) (↑v : E))) (instModuleTangentSpace 𝓘(ℝ, E) (↑v : E)) (β :=
                Module ℝ E) (NormedSpace.toModule : Module ℝ E) →
              HEq (α := TopologicalSpace (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v))
                  (instTopologicalSpaceTangentSpace (𝓡 n) v) (β := TopologicalSpace (EuclideanSpace ℝ (Fin n)))
                  (PiLp.topologicalSpace 2 fun (x : Fin n) ↦ ℝ) →
                HEq (α := TopologicalSpace (TangentSpace 𝓘(ℝ, E) (↑v : E)))
                    (instTopologicalSpaceTangentSpace 𝓘(ℝ, E) (↑v : E)) (β := TopologicalSpace E)
                    UniformSpace.toTopologicalSpace →
                  Eq (α := EuclideanSpace ℝ (Fin n))
                    ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v) 0
Tactic: convert! this using 4
-- 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 : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
⊢ 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))ᗮ
have ℝ : 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: suffices
      (fderiv ℝ ((stereoInvFunAux (-v : E) ∘ (↑)) ∘ U.symm) 0).range = (ℝ ∙ (v : E))ᗮ by
    convert! this using 4
    apply stereographic'_neg
-- 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 : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
⊢ HasFDerivAt (E := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    (stereoInvFunAux (-(↑v : E)) ∘
      Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑(-v) : E))ᗮ x))
    (Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0)
have h : ↥(ℝ ∙ (↑(-v) : E))ᗮ = ↥(ℝ ∙ -(↑v : E))ᗮ →
  Eq (α := ↥(ℝ ∙ (↑(-v) : E))ᗮ)
    ((U.symm : (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ) 0 : ↥(ℝ ∙ (↑(-v) : E))ᗮ) (0 : ↥(ℝ ∙ -(↑v : E))ᗮ)
Tactic: convert! hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)