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
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 ℝ 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))ᗮ
have this : 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)
Tactic: have :
    HasFDerivAt (stereoInvFunAux (-v : E) ∘ (Subtype.val : (ℝ ∙ (↑(-v) : E))ᗮ → E))
      (ℝ ∙ (↑(-v) : E))ᗮ.subtypeL (U.symm 0) := by
    convert! hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)
    simp
-- 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 :
  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)
⊢ 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))ᗮ
have h : (ℝ ∙ (↑v : E))ᗮ =
  (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range
Tactic: convert! congr($((this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv).range)
-- 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 :
  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)
⊢ (ℝ ∙ (↑v : E))ᗮ =
    (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
            (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
              EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range
have h : (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range =
  (ℝ ∙ (↑v : E))ᗮ
Tactic: symm
-- 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 :
  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)
⊢ (↑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
            (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
              EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
        EuclideanSpace ℝ (Fin n) →ₗ[ℝ] E).range =
    (ℝ ∙ (↑v : E))ᗮ
have h : Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E))ᗮ
  (LinearMap.range (M := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (Submodule.subtype (ℝ ∙ (↑(-v) : E))ᗮ))
Tactic: convert!
    (U.symm : EuclideanSpace ℝ (Fin n) ≃ₗᵢ[ℝ] (ℝ ∙ (↑(-v) : E))ᗮ).range_comp
      (ℝ ∙ (↑(-v) : E))ᗮ.subtype 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 : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  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)
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E))ᗮ
    (LinearMap.range (M := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (Submodule.subtype (ℝ ∙ (↑(-v) : E))ᗮ))
have h : Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E))ᗮ (ℝ ∙ -(↑v : E))ᗮ
Tactic: simp only [Submodule.range_subtype, coe_neg_sphere]
-- 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 :
  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)
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E))ᗮ (ℝ ∙ -(↑v : E))ᗮ
have h : Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E)) (ℝ ∙ -(↑v : E))
Tactic: congr 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 : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  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)
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E)) (ℝ ∙ -(↑v : E))
have h : {(↑v : E)} ⊆ (↑(ℝ ∙ -(↑v : E)) : Set E)
Tactic: apply Submodule.span_eq_span
-- 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 :
  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)
h : {(↑v : E)} ⊆ (↑(ℝ ∙ -(↑v : E)) : Set E)
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ (↑v : E)) (ℝ ∙ -(↑v : E))
have h₁ : {-(↑v : E)} ⊆ (↑(ℝ ∙ (↑v : E)) : Set E)
Tactic: apply Submodule.span_eq_span
-- 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 :
  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)
⊢ {(↑v : E)} ⊆ (↑(ℝ ∙ -(↑v : E)) : Set E)
have h : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E)) (↑v : E)
Tactic: simp only [Set.singleton_subset_iff, SetLike.mem_coe]
-- 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 :
  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)
⊢ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E)) (↑v : E)
have h : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ -(↑v : E)) (-(↑v : E))
Tactic: rw [← Submodule.neg_mem_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)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  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)
⊢ {-(↑v : E)} ⊆ (↑(ℝ ∙ (↑v : E)) : Set E)
have h : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑v : E)) (-(↑v : E))
Tactic: simp only [Set.singleton_subset_iff, SetLike.mem_coe]
-- 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 :
  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)
⊢ Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑v : E)) (-(↑v : E))
have h : Membership.mem (γ := Submodule ℝ E) (ℝ ∙ (↑v : E)) (↑v : E)
Tactic: rw [Submodule.neg_mem_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)
⊢ Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(mfderiv% (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x)) v) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))
have rw : Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
  (⇑(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)) :
    (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, 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)
⊢ Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(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)) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))
have simp : Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
  (⇑(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)) :
    (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))
Tactic: simp only [chartAt, 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 :
  Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
⊢ Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(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)) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))
have h : TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v = EuclideanSpace ℝ (Fin n) →
  TangentSpace 𝓘(ℝ, E) (↑v : E) = E →
    (TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v →L[ℝ] TangentSpace 𝓘(ℝ, E) (↑v : E)) =
        (EuclideanSpace ℝ (Fin n) →L[ℝ] E) →
      Eq (α := EuclideanSpace ℝ (Fin n))
        ((↑(ChartedSpace.chartAt v) : { x : E // x ∈ sphere 0 1 } → EuclideanSpace ℝ (Fin n)) v) 0
Tactic: convert! this using 3
-- 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 ⋯)
⊢ Injective (α := TangentSpace (E := EuclideanSpace ℝ (Fin n)) (𝓡 n) v) (β := TangentSpace 𝓘(ℝ, E) (↑v : E))
    (⇑(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)) :
      (a : TangentSpace (𝓡 n) v) → TangentSpace 𝓘(ℝ, E) (↑v : E))
have suffices : Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
  (⇑(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) :
    (a : EuclideanSpace ℝ (Fin n)) → E)
Tactic: suffices Injective (fderiv ℝ ((stereoInvFunAux (-v : E) ∘ (↑)) ∘ U.symm) 0) by
    convert! this using 3
    apply stereographic'_neg
-- 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 : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
have this : 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)
Tactic: have : HasFDerivAt (stereoInvFunAux (-v : E) ∘ (Subtype.val : (ℝ ∙ (↑(-v) : E))ᗮ → E))
      (ℝ ∙ (↑(-v) : E))ᗮ.subtypeL (U.symm 0) := by
    convert! hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)
    simp
-- 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 : (↑(sphere 0 1) : Type u_1)
U : ↥(ℝ ∙ (↑(-v) : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  OrthonormalBasis.repr (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯)
this :
  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)
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
have this₁ : Eq (α := (a : EuclideanSpace ℝ (Fin n)) → E)
  (⇑(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) :
    (a : EuclideanSpace ℝ (Fin n)) → E)
  (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
        (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
          EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
    (a : EuclideanSpace ℝ (Fin n)) → E)
Tactic: have := congr_arg DFunLike.coe <| (this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv
-- 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_1 :
  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)
this :
  Eq (α := (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
have refine : Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
  (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
        (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
          EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
    (a : EuclideanSpace ℝ (Fin n)) → E)
Tactic: refine Eq.subst this.symm ?_
-- 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_1 :
  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)
this :
  Eq (α := (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(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) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
⊢ Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
    (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ ∘SL
          (↑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
            EuclideanSpace ℝ (Fin n) →L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ)) :
      (a : EuclideanSpace ℝ (Fin n)) → E)
have rw : Injective (α := EuclideanSpace ℝ (Fin n)) (β := E)
  (comp (β := ↥(ℝ ∙ (↑(-v) : E))ᗮ) (⇑(Submodule.subtypeL (ℝ ∙ (↑(-v) : E))ᗮ) : (a : ↥(ℝ ∙ (↑(-v) : E))ᗮ) → E)
    (⇑(↑U.symm : EuclideanSpace ℝ (Fin n) ≃L[ℝ] ↥(ℝ ∙ (↑(-v) : E))ᗮ) :
      (a : EuclideanSpace ℝ (Fin n)) → ↥(ℝ ∙ (↑(-v) : E))ᗮ))
Tactic: rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe]