fix: Mathlib/Control/ULiftable doc typos (#6349)

small typos in docstrings
leanprover-community · Aug 3, 2023 · 74ee5fb · 74ee5fb
1 parent 32fa6fe
commit 74ee5fb
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Control/ULiftable.lean b/Mathlib/Control/ULiftable.lean
@@ -48,7 +48,7 @@ class ULiftable (f : Type u₀ → Type u₁) (g : Type v₀ → Type v₁) wher
 
 namespace ULiftable
 
-/-- The most common practical use `ULiftable` (together with `up`), this function takes
+/-- The most common practical use `ULiftable` (together with `down`), this function takes
 `x : M.{u} α` and lifts it to `M.{max u v} (ULift.{v} α)` -/
 @[reducible]
 def up {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [ULiftable f g] {α} :
@@ -57,7 +57,7 @@ def up {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [ULi
 #align uliftable.up ULiftable.up
 
 /-- The most common practical use of `ULiftable` (together with `up`), this function takes
-`x : M.{max u v} (ulift.{v} α)` and lowers it to `M.{u} α` -/
+`x : M.{max u v} (ULift.{v} α)` and lowers it to `M.{u} α` -/
 @[reducible]
 def down {f : Type u₀ → Type u₁} {g : Type max u₀ v₀ → Type v₁} [ULiftable f g] {α} :
     g (ULift.{v₀} α) → f α :=