-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem range_mfderiv_coe_sphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) :
    LinearMap.range (mfderiv (𝓡 n) 𝓘(ℝ, E) ((↑) : sphere (0 : E) 1 → E) v :
    TangentSpace (𝓡 n) v →L[ℝ] E) = (ℝ ∙ (v : E))ᗮ

Proof state:
case h.e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)
⊢ (Submodule.span ℝ {↑v})ᗮ = LinearMap.range ((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)

Tactic:
symm

Result:
case h.e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)
⊢ LinearMap.range ((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv) = (Submodule.span ℝ {↑v})ᗮ

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ LinearMap.range (fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v)) =
    (Submodule.span ℝ {↑v})ᗮ

Tactic:
let U := (OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ) n
  (ne_zero_of_mem_unit_sphere (-v))).repr

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
⊢ LinearMap.range (fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v)) =
    (Submodule.span ℝ {↑v})ᗮ

Proof state:
case h.e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)
⊢ (Submodule.span ℝ {↑v})ᗮ = LinearMap.range (Submodule.span ℝ {↑(-v)})ᗮ.subtype

Tactic:
simp only [Submodule.range_subtype, coe_neg_sphere]

Result:
case h.e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)
⊢ (Submodule.span ℝ {↑v})ᗮ = (Submodule.span ℝ {-↑v})ᗮ

Proof state:
case h.e'_2.h.h.e'_16.h.h.e'_12
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : LinearMap.range (fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = (Submodule.span ℝ {↑v})ᗮ
e_1✝ : Submodule ℝ (TangentSpace 𝓘(ℝ, E) ↑v) = Submodule ℝ E
e_12✝ : (TangentSpace (𝓡 n) v →L[ℝ] TangentSpace 𝓘(ℝ, E) ↑v) = (EuclideanSpace ℝ (Fin n) →L[ℝ] E)
⊢ ↑(ChartedSpace.chartAt v) v = 0

Tactic:
apply stereographic'_neg

Result:
no goals

Proof state:
case h.e'_13.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
e_3✝ : ↥(Submodule.span ℝ {↑(-v)})ᗮ = ↥(Submodule.span ℝ {-↑v})ᗮ
⊢ U.symm 0 = 0

Tactic:
simp

Result:
no goals