-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem mfderiv_coe_sphere_injective {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) :
    Injective (mfderiv (𝓡 n) 𝓘(ℝ, E) ((↑) : sphere (0 : E) 1 → E) v)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ Injective ⇑(mfderiv (𝓡 n) 𝓘(ℝ, E) Subtype.val v)

Tactic:
rw [((contMDiff_coe_sphere v).mdifferentiableAt le_top).mfderiv]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ Injective
    ⇑(fderivWithin ℝ (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑(𝓡 n)) (↑(extChartAt (𝓡 n) v) v))

Proof state:
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
⊢ Injective ⇑(fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v))

Tactic:
suffices Injective (fderiv ℝ ((stereoInvFunAux (-v : E) ∘ (↑)) ∘ U.symm) 0) by
  convert this using 3
  apply stereographic'_neg

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
⊢ Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)

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

Proof state:
case h.e'_3.h.h.e'_5.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 : Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)
e_1✝¹ : TangentSpace (𝓡 n) v = EuclideanSpace ℝ (Fin n)
e_2✝ : TangentSpace 𝓘(ℝ, E) ↑v = E
e_1✝ : (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:
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)
this :
  ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) =
    ⇑((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)
⊢ Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)

Tactic:
refine Eq.subst this.symm ?_

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
this✝ : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)
this :
  ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) =
    ⇑((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)
⊢ Injective ⇑((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)

Proof state:
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)
this :
  ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) =
    ⇑((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)
⊢ Injective (⇑(Submodule.span ℝ {↑(-v)})ᗮ.subtypeL ∘ ⇑U.symm.toContinuousLinearEquiv)

Tactic:
simpa [- Subtype.val_injective] using Subtype.val_injective

Result:
no goals

Proof state:
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
⊢ Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 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

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
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)
⊢ Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)

Proof state:
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
⊢ HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)

Tactic:
convert hasFDerivAt_stereoInvFunAux_comp_coe (-v : E)

Result:
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

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ Injective
    ⇑(fderivWithin ℝ (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑(𝓡 n)) (↑(extChartAt (𝓡 n) v) v))

Tactic:
simp only [chartAt, stereographic', stereographic_neg_apply, fderivWithin_univ,
  LinearIsometryEquiv.toHomeomorph_symm, LinearIsometryEquiv.coe_toHomeomorph,
  LinearIsometryEquiv.map_zero, mfld_simps]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ Injective ⇑(fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v))