improve comments

leanprover-community · Oct 23, 2023 · f005fb5 · f005fb5
1 parent 119d99e
commit f005fb5
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/exercises_sources/friday/manifolds.lean b/src/exercises_sources/friday/manifolds.lean
@@ -462,8 +462,7 @@ be a smooth manifold. -/
 So, one can prescribe an element of the tangent bundle as a pair (more on this below) -/
 example : tangent_bundle 𝓡1 myℝ := ⟨(4 : ℝ), 0⟩
 
-/- Construct the smooth manifold structure on the tangent bundle. Hint: the answer is a one-liner,
-and this instance is not really needed. -/
+/- Type-class inference can construct the smooth manifold structure on the tangent bundle. -/
 example : smooth_manifold_with_corners (𝓡1.prod 𝓡1) (tangent_bundle 𝓡1 myℝ) :=
 sorry
 
@@ -475,6 +474,7 @@ equal. And this would be bad.
 -/
 example : charted_space (model_prod ℝ ℝ) (tangent_bundle 𝓡1 myℝ) :=
 sorry
+
 /-
 The charts of any smooth vector bundle are characterized by `fiber_bundle.charted_space_chart_at`
 -/

diff --git a/src/solutions/friday/manifolds.lean b/src/solutions/friday/manifolds.lean
@@ -515,8 +515,7 @@ be a smooth manifold. -/
 So, one can prescribe an element of the tangent bundle as a pair (more on this below) -/
 example : tangent_bundle 𝓡1 myℝ := ⟨(4 : ℝ), 0⟩
 
-/- Construct the smooth manifold structure on the tangent bundle. Hint: the answer is a one-liner,
-and this instance is not really needed. -/
+/- Type-class inference can construct the smooth manifold structure on the tangent bundle. -/
 example : smooth_manifold_with_corners (𝓡1.prod 𝓡1) (tangent_bundle 𝓡1 myℝ) :=
 -- sorry
 by apply_instance
@@ -532,6 +531,7 @@ example : charted_space (model_prod ℝ ℝ) (tangent_bundle 𝓡1 myℝ) :=
 -- sorry
 by apply_instance
 -- sorry
+
 /-
 The charts of any smooth vector bundle are characterized by `fiber_bundle.charted_space_chart_at`
 -/