Keep error explanations in sync

src/Lean/ErrorExplanations/DependsOnNoncomputable.lean

@@ -63,7 +63,7 @@ def endsOrDefault (ns : List Nat) : Nat × Nat :=
   (head, tail)
 ```
 ```output
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable'
+failed to compile definition, consider marking it as 'noncomputable' because it depends on 'getOrDefault', which is 'noncomputable'
 ```
 ```lean fixed (title := "Fixed (computable)")
 def getOrDefault [Inhabited α] : Option α → α
@@ -96,7 +96,7 @@ def fromImage (f : Nat → Nat) (y : Nat) :=
     f 0
 ```
 ```output
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.propDecidable', which is 'noncomputable'
+failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable'
 ```
 ```lean fixed
 open Classical in

src/Lean/ErrorExplanations/PropRecLargeElim.lean

@@ -44,7 +44,7 @@ Tactic `cases` failed with a nested error:
 Tactic `induction` failed: recursor `Nonempty.casesOn` can only eliminate into `Prop`
 
 α : Type
-motive : Nonempty α → Sort ?u.52
+motive : Nonempty α → Sort ?u.48
 h_1 : (x : α) → motive ⋯
 inst✝ : Nonempty α
 ⊢ motive inst✝
@@ -81,7 +81,7 @@ Tactic `induction` failed: recursor `Exists.casesOn` can only eliminate into `Pr
 
 α : Type u
 p : α → Prop
-motive : (∃ x, p x) → Sort ?u.48
+motive : (∃ x, p x) → Sort ?u.52
 h_1 : (x : α) → (h : p x) → motive ⋯
 h✝ : ∃ x, p x
 ⊢ motive h✝

src/Lean/ErrorExplanations/UnknownIdentifier.lean

@@ -188,11 +188,11 @@ qualified function name.
 ## Auto-bound variables
 
 ```lean broken
-set autoImplicit false in
+set_option relaxedAutoImplicit false in
 def thisBreaks (x : α₁) (y : size₁) := ()
 
-set relaxedAutoImplicit false in
-def thisBreaks (x : α₂) (y : size₂) := ()
+set_option autoImplicit false in
+def thisAlsoBreaks (x : α₂) (y : size₂) := ()
 ```
 ```output
 Unknown identifier `size₁`
@@ -206,18 +206,18 @@ Unknown identifier `size₂`
 Note: It is not possible to treat `size₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
 ```
 ```lean fixed (title := "Fixed (modifying options)")
-set autoImplicit true in
-def thisBreaks (x : α₁) (y : size₁) := ()
+set_option relaxedAutoImplicit true in
+def thisWorks (x : α₁) (y : size₁) := ()
 
-set relaxedAutoImplicit true in
-def thisBreaks (x : α₂) (y : size₂) := ()
+set_option autoImplicit true in
+def thisAlsoWorks (x : α₂) (y : size₂) := ()
 ```
 ```lean fixed (title := "Fixed (add implicit bindings for the unknown identifiers)")
-set autoImplicit false in
-def thisBreaks {size₁} (x : α₁) (y : size₁) := ()
+set_option relaxedAutoImplicit false in
+def thisWorks {size₁} (x : α₁) (y : size₁) := ()
 
-set relaxedAutoImplicit false in
-def thisBreaks {α₂ size₂} (x : α₂) (y : size₂) := ()
+set_option autoImplicit false in
+def thisAlsoWorks {α₂ size₂} (x : α₂) (y : size₂) := ()
 ```
 
 Lean's default behavior, when it encounters an identifier it can't identify in the type of a