-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem contMDiff_coe_sphere {m : WithTop ℕ∞} {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
    ContMDiff (𝓡 n) 𝓘(ℝ, E) m ((↑) : sphere (0 : E) 1 → E)

Proof state:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
v : { x // x ∈ sphere 0 1 }
y✝ : E
⊢ ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y✝) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) v).symm)
    ((extChartAt (𝓡 n) v).target ∩ ↑(extChartAt (𝓡 n) v).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y✝).source))

Tactic:
let U : _ ≃ₗᵢ[ℝ] _ :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton
      n (ne_zero_of_mem_unit_sphere (-v))).repr

Result:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
v : { x // x ∈ sphere 0 1 }
y✝ : E
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
⊢ ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y✝) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) v).symm)
    ((extChartAt (𝓡 n) v).target ∩ ↑(extChartAt (𝓡 n) v).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y✝).source))

Proof state:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
v : { x // x ∈ sphere 0 1 }
y✝ : E
U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
  (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
⊢ ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y✝) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) v).symm)
    ((extChartAt (𝓡 n) v).target ∩ ↑(extChartAt (𝓡 n) v).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y✝).source))

Tactic:
exact
  ((contDiff_stereoInvFunAux.comp (ℝ ∙ (-v : E))ᗮ.subtypeL.contDiff).comp
      U.symm.contDiff).contDiffOn

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m Subtype.val

Tactic:
rw [contMDiff_iff]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
⊢ Continuous Subtype.val ∧
    ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
      ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
        ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source))

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
⊢ Continuous Subtype.val ∧
    ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
      ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
        ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source))

Tactic:
constructor

Result:
case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
⊢ Continuous Subtype.val

case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
⊢ ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
    ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
      ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source))

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m Subtype.val

Tactic:
have := EuclideanSpace.instIsManifoldSphere (E := E) (n := n)

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m Subtype.val

Proof state:
case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
⊢ Continuous Subtype.val

Tactic:
exact continuous_subtype_val

Result:
no goals

Proof state:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
⊢ ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
    ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
      ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source))

Tactic:
intro v _

Result:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
this : IsManifold (𝓡 n) ω ↑(sphere 0 1)
v : { x // x ∈ sphere 0 1 }
y✝ : E
⊢ ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y✝) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) v).symm)
    ((extChartAt (𝓡 n) v).target ∩ ↑(extChartAt (𝓡 n) v).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y✝).source))