diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 3074b883b7..5eb2db2423 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -54,8 +54,8 @@ We don't want to waste your time by you implementing a feature and then us not b
 
 ## How to Contribute
 
-* Always follow the [commit convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).
+* Always follow the [commit convention](https://lean-lang.org/lean4/doc/dev/commit_convention.html).
 * Follow the style of the surrounding code. When in doubt, look at other files using the particular syntax as well.
 * Make sure your code is documented.
 * New features or bug fixes should come with appropriate tests.
-* Ensure all tests work before submitting a PR; see [Development Setup](https://leanprover.github.io/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://leanprover.github.io/lean4/doc/dev/fixing_tests.html).
+* Ensure all tests work before submitting a PR; see [Development Setup](https://lean-lang.org/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://lean-lang.org/lean4/doc/dev/fixing_tests.html).
diff --git a/README.md b/README.md
index e449019254..2e328b4a8a 100644
--- a/README.md
+++ b/README.md
@@ -8,18 +8,18 @@ and have just begun regular [stable point releases](https://github.com/leanprove
 - [Quickstart](https://github.com/leanprover/lean4/blob/master/doc/quickstart.md)
 - [Walkthrough installation video](https://www.youtube.com/watch?v=yZo6k48L0VY)
 - [Quick tour video](https://youtu.be/zyXtbb_eYbY)
-- [Homepage](https://leanprover.github.io)
-- [Theorem Proving Tutorial](https://leanprover.github.io/theorem_proving_in_lean4/)
-- [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/)
-- [Manual](https://leanprover.github.io/lean4/doc/)
+- [Homepage](https://lean-lang.org)
+- [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
+- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
+- [Manual](https://lean-lang.org/lean4/doc/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://leanprover.github.io/lean4/doc/examples.html)
+- [Examples](https://lean-lang.org/lean4/doc/examples.html)
 - [External Contribution Guidelines](https://github.com/leanprover/lean4/blob/master/doc/contributions.md)
-- [FAQ](https://leanprover.github.io/lean4/doc/faq.html)
+- [FAQ](https://lean-lang.org/lean4/doc/faq.html)
 
 # Installation
 
-See [Setting Up Lean](https://leanprover.github.io/lean4/doc/setup.html).
+See [Setting Up Lean](https://lean-lang.org/lean4/doc/setup.html).
 
 # Contributing
 
@@ -27,4 +27,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
 
 # Building from Source
 
-See [Building Lean](https://leanprover.github.io/lean4/doc/make/index.html).
+See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html).
diff --git a/doc/bin/README.md b/doc/bin/README.md
index 6fb6537690..d161c0af92 100644
--- a/doc/bin/README.md
+++ b/doc/bin/README.md
@@ -11,4 +11,4 @@ the following command executes a simple set of examples
 
 % bin/lean examples/ex.lean
 
-For more information on Lean and supported editors, please see https://leanprover.github.io/documentation/.
+For more information on Lean and supported editors, please see https://lean-lang.org/documentation/.
diff --git a/doc/dev/mdbook.md b/doc/dev/mdbook.md
index 103d4ee910..eab9f4a187 100644
--- a/doc/dev/mdbook.md
+++ b/doc/dev/mdbook.md
@@ -1,6 +1,6 @@
 # Documentation
 
-The Lean `doc` folder contains the [Lean Manual](https://leanprover.github.io/lean4/doc/) and is
+The Lean `doc` folder contains the [Lean Manual](https://lean-lang.org/lean4/doc/) and is
 authored in a combination of markdown (`*.md`) files and literate Lean files.  The .lean files are
 preprocessed using a tool called [LeanInk](https://github.com/leanprover/leanink) and
 [Alectryon](https://github.com/Kha/alectryon) which produces a generated markdown file.  We then run
@@ -83,7 +83,7 @@ Then run the following:
     ```
 
 This will put the HTML in a `out` folder so you can load `out/index.html` in your web browser and
-it should look like https://leanprover.github.io/lean4/doc/.
+it should look like https://lean-lang.org/lean4/doc/.
 
 1. It is also handy to use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html)
    in the `doc/` folder so that it keeps the html up to date while you are editing.
diff --git a/doc/faq.md b/doc/faq.md
index 733736683e..af8b4bfe02 100644
--- a/doc/faq.md
+++ b/doc/faq.md
@@ -27,7 +27,7 @@ It is a good place to interact with other Lean users.
 ### Should I use Lean to teach a course?
 
 Lean has been used to teach courses on logic, type theory and programming languages at CMU and the University of Washington.
-The lecture notes for the CMU course [Logic and Proof](https://leanprover.github.io/logic_and_proof) are available online,
+The lecture notes for the CMU course [Logic and Proof](https://lean-lang.org/logic_and_proof) are available online,
 but they are for Lean 3.
 If you decide to teach a course using Lean, we suggest you prepare all material before the beginning of the course, and
 make sure that Lean attends all your needs. You should not expect we will fix bugs and/or add features needed for your course.
diff --git a/doc/fplean.md b/doc/fplean.md
index 4f00130c6f..76e613884c 100644
--- a/doc/fplean.md
+++ b/doc/fplean.md
@@ -1,7 +1,7 @@
 Functional Programming in Lean
 =======================
 
-The goal of [this book](https://leanprover.github.io/functional_programming_in_lean/) is to be an accessible introduction to using Lean 4 as a programming language.
+The goal of [this book](https://lean-lang.org/functional_programming_in_lean/) is to be an accessible introduction to using Lean 4 as a programming language.
 It should be useful both to people who want to use Lean as a general-purpose programming language and to mathematicians who want to develop larger-scale proof automation but do not have a background in functional programming.
 It does not assume any background with functional programming, though it's probably not a good first book on programming in general.
 New content will be added once per month until it's done.
diff --git a/doc/inductive.md b/doc/inductive.md
index f93a81fc00..20f0dcace2 100644
--- a/doc/inductive.md
+++ b/doc/inductive.md
@@ -1,3 +1,3 @@
 # Inductive Types
 
-[Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html) has a chapter about inductive datatypes.
+[Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html) has a chapter about inductive datatypes.
diff --git a/doc/semantic_highlighting.md b/doc/semantic_highlighting.md
index 877706c75d..10807630b9 100644
--- a/doc/semantic_highlighting.md
+++ b/doc/semantic_highlighting.md
@@ -4,7 +4,7 @@ Semantic Highlighting
 The Lean language server provides semantic highlighting information to editors. In order to benefit from this in VSCode, you may need to activate the "Editor > Semantic Highlighting" option in the preferences (this is translates to `"editor.semanticHighlighting.enabled": true,`
 in `settings.json`). The default option here is to let your color theme decides whether it activates semantic highlighting (the default themes Dark+ and Light+ do activate it for instance).
 
-However this may be insufficient if your color theme does not distinguish enough syntax categories or distinguishes them very subtly. For instance the default Light+ theme uses color `#001080` for variables. This is awfully close to `#000000` that is used as the default text color. This makes it very easy to miss an accidental use of [auto bound implicit arguments](https://leanprover.github.io/lean4/doc/autobound.html). For instance in
+However this may be insufficient if your color theme does not distinguish enough syntax categories or distinguishes them very subtly. For instance the default Light+ theme uses color `#001080` for variables. This is awfully close to `#000000` that is used as the default text color. This makes it very easy to miss an accidental use of [auto bound implicit arguments](https://lean-lang.org/lean4/doc/autobound.html). For instance in
 ```lean
 def my_id (n : nat) := n
 ```
diff --git a/doc/tpil.md b/doc/tpil.md
index 891d29ad38..fac1006719 100644
--- a/doc/tpil.md
+++ b/doc/tpil.md
@@ -1,5 +1,5 @@
 Theorem Proving in Lean
 =======================
 
-We strongly encourage you to read the book [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/title_page.html).
+We strongly encourage you to read the book [Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean4/title_page.html).
 Many Lean users consider it to be the Lean Bible.
diff --git a/doc/whatIsLean.md b/doc/whatIsLean.md
index e1bcdeaeda..3c91dc80b6 100644
--- a/doc/whatIsLean.md
+++ b/doc/whatIsLean.md
@@ -36,7 +36,7 @@ Lean has numerous features, including:
 - [Monads](./monads/intro.md)
 - [Extensible syntax](./syntax.md)
 - Hygienic macros
-- [Dependent types](https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html)
+- [Dependent types](https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html)
 - [Metaprogramming](./metaprogramming.md)
 - Multithreading
 - Verification: you can prove properties of your functions using Lean itself
diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index f974028bc0..b45b1ef928 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -292,7 +292,7 @@ macro_rules
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
 by focusing on particular subexpressions.
 
-See <https://leanprover.github.io/theorem_proving_in_lean4/conv.html> for more details.
+See <https://lean-lang.org/theorem_proving_in_lean4/conv.html> for more details.
 
 Basic forms:
 * `conv => cs` will rewrite the goal with conv tactics `cs`.
diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 11b706038c..fb9c75d078 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -127,7 +127,7 @@ calc abc
 
 See [Theorem Proving in Lean 4][tpil4] for more information.
 
-[tpil4]: https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
+[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 -/
 syntax (name := calc) "calc" calcSteps : term
 
@@ -166,7 +166,7 @@ leave a subgoal proving `z = z'`.
 
 See [Theorem Proving in Lean 4][tpil4] for more information.
 
-[tpil4]: https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
+[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 -/
 syntax (name := calcTactic) "calc" calcSteps : tactic
 
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 68fec587bf..e8163cbb49 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -104,7 +104,7 @@ set_option bootstrap.inductiveCheckResultingUniverse false in
 The unit type, the canonical type with one element, named `unit` or `()`.
 This is the universe-polymorphic version of `Unit`; it is preferred to use
 `Unit` instead where applicable.
-For more information about universe levels: [Types as objects](https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects)
+For more information about universe levels: [Types as objects](https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects)
 -/
 inductive PUnit : Sort u where
   /-- `PUnit.unit : PUnit` is the canonical element of the unit type. -/
@@ -171,7 +171,7 @@ unsafe axiom lcUnreachable {α : Sort u} : α
 /--
 `True` is a proposition and has only an introduction rule, `True.intro : True`.
 In other words, `True` is simply true, and has a canonical proof, `True.intro`
-For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
+For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
 -/
 inductive True : Prop where
   /-- `True` is true, and `True.intro` (or more commonly, `trivial`)
@@ -184,7 +184,7 @@ It represents a contradiction. `False` elimination rule, `False.rec`,
 expresses the fact that anything follows from a contradiction.
 This rule is sometimes called ex falso (short for ex falso sequitur quodlibet),
 or the principle of explosion.
-For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
+For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
 -/
 inductive False : Prop
 
@@ -206,7 +206,7 @@ inductive PEmpty : Sort u where
 so if your goal is `¬p` you can use `intro h` to turn the goal into
 `h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
 and `(hn h).elim` will prove anything.
-For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
+For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
 -/
 def Not (a : Prop) : Prop := a → False
 
@@ -228,7 +228,7 @@ Anything follows from two contradictory hypotheses. Example:
 ```
 example (hp : p) (hnp : ¬p) : q := absurd hp hnp
 ```
-For more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
+For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
 -/
 @[macro_inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b :=
   (h₂ h₁).rec
@@ -258,7 +258,7 @@ example (α : Type) (a b : α) (p : α → Prop)
   h1 ▸ h2
 ```
 The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
-For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
+For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
 inductive Eq : α → α → Prop where
   /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the
@@ -294,7 +294,7 @@ essentially a fancy algorithm for finding good `motive` arguments to usefully
 apply this theorem to replace occurrences of `a` with `b` in the goal or
 hypotheses.
 
-For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
+For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
 theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) (h₂ : motive a) : motive b :=
   Eq.ndrec h₂ h₁
@@ -305,7 +305,7 @@ Equality is symmetric: if `a = b` then `b = a`.
 Because this is in the `Eq` namespace, if you have a variable `h : a = b`,
 `h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.
 
-For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
+For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
 theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
   h ▸ rfl
@@ -317,7 +317,7 @@ Because this is in the `Eq` namespace, if you have variables or expressions
 `h₁ : a = b` and `h₂ : b = c`, you can use `h₁.trans h₂ : a = c` as shorthand
 for `Eq.trans h₁ h₂`.
 
-For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
+For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
 theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : Eq a b) (h₂ : Eq b c) : Eq a c :=
   h₂ ▸ h₁
@@ -331,7 +331,7 @@ It is best to avoid this function if you can, because it is more complicated
 to reason about terms containing casts, but if the types don't match up
 definitionally sometimes there isn't anything better you can do.
 
-For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
+For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
 @[macro_inline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=
   h.rec a
@@ -344,7 +344,7 @@ you can also use a lambda expression for `f` to prove that
 internally by tactics like `congr` and `simp` to apply equalities inside
 subterms.
 
-For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
+For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
 theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
   h ▸ rfl
@@ -354,7 +354,7 @@ Congruence in both function and argument. If `f₁ = f₂` and `a₁ = a₂` the
 `f₁ a₁ = f₂ a₂`. This only works for nondependent functions; the theorem
 statement is more complex in the dependent case.
 
-For more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
+For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
 theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : Eq f₁ f₂) (h₂ : Eq a₁ a₂) : Eq (f₁ a₁) (f₂ a₂) :=
   h₁ ▸ h₂ ▸ rfl
@@ -461,7 +461,7 @@ as notation for `Prod.mk a b`. Moreover, `(a, b, c)` is notation for
 `Prod.mk a (Prod.mk b c)`.
 Given `p : Prod α β`, `p.1 : α` and `p.2 : β`. They are short for `Prod.fst p`
 and `Prod.snd p` respectively. You can also write `p.fst` and `p.snd`.
-For more information: [Constructors with Arguments](https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html?highlight=Prod#constructors-with-arguments)
+For more information: [Constructors with Arguments](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html?highlight=Prod#constructors-with-arguments)
 -/
 structure Prod (α : Type u) (β : Type v) where
   /-- The first projection out of a pair. if `p : α × β` then `p.1 : α`. -/
@@ -2744,7 +2744,7 @@ Like many functional programming languages, Lean makes extensive use of monads
 for structuring programs. In particular, the `do` notation is a very powerful
 syntax over monad operations, and it depends on a `Monad` instance.
 
-See [the `do` notation](https://leanprover.github.io/lean4/doc/do.html)
+See [the `do` notation](https://lean-lang.org/lean4/doc/do.html)
 chapter of the manual for details.
 -/
 class Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) where
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index e03f24ce17..18074aac93 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -60,7 +60,7 @@ def bar ⦃x : Nat⦄ : Nat := x
 #check bar -- bar : ⦃x : Nat⦄ → Nat
 ```
 
-See also the Lean manual: https://leanprover.github.io/lean4/doc/expressions.html#implicit-arguments
+See also the Lean manual: https://lean-lang.org/lean4/doc/expressions.html#implicit-arguments
 -/
 inductive BinderInfo where
   /-- Default binder annotation, e.g. `(x : α)` -/
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index d770151167..9aedcd7417 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -166,7 +166,7 @@ inductive List (α : Type u) where
 ```
 A list of elements of type `α` is either the empty list, `nil`,
 or an element `head : α` followed by a list `tail : List α`.
-For more information about [inductive types](https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html).
+For more information about [inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html).
 -/
 def «inductive»      := leading_parser
   "inductive " >> declId >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index d0140c99b8..c850938411 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -38,7 +38,7 @@ example (n : Nat) : n = n := by
   | i+1 => simp
 ```
 
-[tpil4]: https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html
+[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html
 -/
 @[builtin_tactic_parser] def «match» := leading_parser:leadPrec
   "match " >> optional Term.generalizingParam >>
diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
index a574103a7f..0699845ba4 100644
--- a/src/stdlib_flags.h
+++ b/src/stdlib_flags.h
@@ -3,7 +3,7 @@
 namespace lean {
 options get_default_options() {
     options opts;
-    // see https://leanprover.github.io/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
+    // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index a574103a7f..0699845ba4 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -3,7 +3,7 @@
 namespace lean {
 options get_default_options() {
     options opts;
-    // see https://leanprover.github.io/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
+    // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
diff --git a/tests/lean/interactive/lean3HoverIssue.lean.expected.out b/tests/lean/interactive/lean3HoverIssue.lean.expected.out
index 69490e2141..98836ec33b 100644
--- a/tests/lean/interactive/lean3HoverIssue.lean.expected.out
+++ b/tests/lean/interactive/lean3HoverIssue.lean.expected.out
@@ -4,7 +4,7 @@
  {"start": {"line": 0, "character": 54}, "end": {"line": 0, "character": 58}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://lean3HoverIssue.lean"},
  "position": {"line": 0, "character": 52}}
@@ -17,7 +17,7 @@
  {"start": {"line": 4, "character": 45}, "end": {"line": 4, "character": 49}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://lean3HoverIssue.lean"},
  "position": {"line": 7, "character": 54}}
@@ -25,7 +25,7 @@
  {"start": {"line": 7, "character": 53}, "end": {"line": 7, "character": 60}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://lean3HoverIssue.lean"},
  "position": {"line": 7, "character": 65}}
@@ -33,7 +33,7 @@
  {"start": {"line": 7, "character": 62}, "end": {"line": 7, "character": 69}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://lean3HoverIssue.lean"},
  "position": {"line": 7, "character": 70}}
@@ -46,5 +46,5 @@
  {"start": {"line": 7, "character": 72}, "end": {"line": 7, "character": 76}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}