chore: fix Inv.inv upstream

doc/std/README.md

@@ -1,9 +0,0 @@
-# The Lean standard library
-
-This directory contains development information about the Lean standard library. The user-facing documentation of the standard library
-is part of the [Lean Language Reference](https://lean-lang.org/doc/reference/latest/).
-
-Here you will find
-* the [standard library vision document](./vision.md), including the call for contributions,
-* the [standard library style guide](./style.md), and
-* the [standard library naming conventions](./naming.md).

doc/std/naming.md

@@ -1,260 +0,0 @@
-# Standard library naming conventions
-
-The easiest way to access a result in the standard library is to correctly guess the name of the declaration (possibly with the help of identifier autocompletion). This is faster and has lower friction than more sophisticated search tools, so easily guessable names (which are still reasonably short) make Lean users more productive.
-
-The guide that follows contains very few hard rules, many heuristics and a selection of examples. It cannot and does not present a deterministic algorithm for choosing good names in all situations. It is intended as a living document that gets clarified and expanded as situations arise during code reviews for the standard library. If applying one of the suggestions in this guide leads to nonsensical results in a certain situation, it is
-probably safe to ignore the suggestion (or even better, suggest a way to improve the suggestion).
-
-## Prelude
-
-Identifiers use a mix of `UpperCamelCase`, `lowerCamelCase` and `snake_case`, used for types, data, and theorems, respectively.
-
-Structure fields should be named such that the projections have the correct names.
-
-## Naming convention for types
-
-When defining a type, i.e., a (possibly 0-ary) function whose codomain is Sort u for some u, it should be named in UpperCamelCase. Examples include `List`, and `List.IsPrefix`.
-
-When defining a predicate, prefix the name by `Is`, like in `List.IsPrefix`. The `Is` prefix may be omitted if
-* the resulting name would be ungrammatical, or
-* the predicate depends on additional data in a way where the `Is` prefix would be confusing (like `List.Pairwise`), or
-* the name is an adjective (like `Std.Time.Month.Ordinal.Valid`)
-
-## Namespaces and generalized projection notation
-
-Almost always, definitions and theorems relating to a type should be placed in a namespace with the same name as the type. For example, operations and theorems about lists should be placed in the `List` namespace, and operations and theorems about `Std.Time.PlainDate` should be placed in the `Std.Time.PlainDate` namespace.
-
-Declarations in the root namespace will be relatively rare. The most common type of declaration in the root namespace are declarations about data and properties exported by notation type classes, as long as they are not about a specific type implementing that type class. For example, we have
-
-```lean
-theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a == b ↔ a = b := sorry
-```
-
-in the root namespace, but
-
-```lean
-theorem List.cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
-    (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
-```
-
-belongs in the `List` namespace.
-
-Subtleties arise when multiple namespaces are in play. Generally, place your theorem in the most specific namespace that appears in one of the hypotheses of the theorem. The following names are both correct according to this convention:
-
-```lean
-theorem List.Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse := sorry
-theorem List.reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ := sorry
-```
-
-Notice that the second theorem does not have a hypothesis of type `List.Sublist l` for some `l`, so the name `List.Sublist.reverse_iff` would be incorrect.
-
-The advantage of placing results in a namespace like `List.Sublist` is that it enables generalized projection notation, i.e., given `h : l₁ <+ l₂`,
-one can write `h.reverse` to obtain a proof of `l₁.reverse <+ l₂.reverse`. Thinking about which dot notations are convenient can act as a guideline
-for deciding where to place a theorem, and is, on occasion, a good reason to duplicate a theorem into multiple namespaces.
-
-### The `Std` namespace
-
-New types that are added will usually be placed in the `Std` namespace and in the `Std/` source directory, unless there are good reasons to place
-them elsewhere.
-
-Inside the `Std` namespace, all internal declarations should be `private` or else have a name component that clearly marks them as internal, preferably
-`Internal`.
-
-
-## Naming convention for data
-
-When defining data, i.e., a (possibly 0-ary) function whose codomain is not Sort u, but has type Type u for some u, it should be named in lowerCamelCase. Examples include `List.append` and `List.isPrefixOf`.
-If your data is morally fully specified by its type, then use the naming procedure for theorems described below and convert the result to lower camel case.
-
-If your function returns an `Option`, consider adding `?` as a suffix. If your function may panic, consider adding `!` as a suffix. In many cases, there will be multiple variants of a function; one returning an option, one that may panic and possibly one that takes a proof argument.
-
-## Naming algorithm for theorems and some definitions
-
-There is, in principle, a general algorithm for naming a theorem. The problem with this algorithm is that it produces very long and unwieldy names which need to be shortened. So choosing a name for a declaration can be thought of as consisting of a mechanical part and a creative part.
-
-Usually the first part is to decide which namespace the result should live in, according to the guidelines described above.
-
-Next, consider the type of your declaration as a tree. Inner nodes of this tree are function types or function applications. Leaves of the tree are 0-ary functions or bound variables.
-
-As an example, consider the following result from the standard library:
-
-```lean
-example {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
-    [Inhabited β] {m : Std.HashMap α β} {a : α} {h' : a ∈ m} : m[a]? = some (m[a]'h') :=
-  sorry
-```
-
-The correct namespace is clearly `Std.HashMap`. The corresponding tree looks like this:
-
-![](naming-tree.svg)
-
-The preferred spelling of a notation can be looked up by hovering over the notation.
-
-Now traverse the tree and build a name according to the following rules:
-
-* When encountering a function type, first turn the result type into a name, then all of the argument types from left to right, and join the names using `_of_`.
-* When encountering a function that is neither an infix notation nor a structure projection, first put the function name and then the arguments, joined by an underscore.
-* When encountering an infix notation, join the arguments using the name of the notation, separated by underscores.
-* When encountering a structure projection, proceed as for normal functions, but put the name of the projection last.
-* When encountering a name, put it in lower camel case.
-* Skip bound variables and proofs.
-* Type class arguments are also generally skipped.
-
-When encountering namespaces names, concatenate them in lower camel case.
-
-Applying this algorithm to our example yields the name `Std.HashMap.getElem?_eq_optionSome_getElem_of_mem`.
-
-From there, the name should be shortened, using the following heuristics:
-
-* The namespace of functions can be omitted if it is clear from context or if the namespace is the current one. This is almost always the case.
-* For infix operators, it is possible to leave out the RHS or the name of the notation and the RHS if they are clear from context.
-* Hypotheses can be left out if it is clear that they are required or if they appear in the conclusion.
-
-Based on this, here are some possible names for our example:
-
-1. `Std.HashMap.getElem?_eq`
-2. `Std.HashMap.getElem?_eq_of_mem`
-3. `Std.HashMap.getElem?_eq_some`
-4. `Std.HashMap.getElem?_eq_some_of_mem`
-5. `Std.HashMap.getElem?_eq_some_getElem`
-6. `Std.Hashmap.getElem?_eq_some_getElem_of_mem`
-
-Choosing a good name among these then requires considering the context of the lemma. In this case it turns out that the first four options are underspecified as there is also a lemma relating `m[a]?` and `m[a]!` which could have the same name. This leaves the last two options, the first of which is shorter, and this is how the lemma is called in the Lean standard library.
-
-Here are some additional examples:
-
-```lean
-example {x y : List α} (h : x <+: y) (hx : x ≠ []) :
-  x.head hx = y.head (h.ne_nil hx) := sorry
-```
-
-Since we have an `IsPrefix` parameter, this should live in the `List.IsPrefix` namespace, and the algorithm suggests `List.IsPrefix.head_eq_head_of_ne_nil`, which is shortened to `List.IsPrefix.head`. Note here the difference between the namespace name (`IsPrefix`) and the recommended spelling of the corresponding notation (`prefix`).
-
-```lean
-example : l₁ <+: l₂ → reverse l₁ <:+ reverse l₂ := sorry
-```
-
-Again, this result should be in the `List.IsPrefix` namespace; the algorithm suggests `List.IsPrefix.reverse_prefix_reverse`, which becomes `List.IsPrefix.reverse`.
-
-The following examples show how the traversal order often matters.
-
-```lean
-theorem Nat.mul_zero (n : Nat) : n * 0 = 0 := sorry
-theorem Nat.zero_mul (n : Nat) : 0 * n = 0 := sorry
-```
-
-Here we see that one name may be a prefix of another name:
-
-```lean
-theorem Int.mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 := sorry
-theorem Int.mul_ne_zero_iff {a b : Int} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := sorry
-```
-
-It is usually a good idea to include the `iff` in a theorem name even if the name would still be unique without the name. For example,
-
-```lean
-theorem List.head?_eq_none_iff : l.head? = none ↔ l = [] := sorry
-```
-
-is a good name: if the lemma was simply called `List.head?_eq_none`, users might try to `apply` it when the goal is `l.head? = none`, leading
-to confusion.
-
-The more common you expect (or want) a theorem to be, the shorter you should try to make the name. For example, we have both
-
-```lean
-theorem Std.HashMap.getElem?_eq_none_of_contains_eq_false {a : α} : m.contains a = false → m[a]? = none := sorry
-theorem Std.HashMap.getElem?_eq_none {a : α} : ¬a ∈ m → m[a]? = none := sorry
-```
-
-As users of the hash map are encouraged to use ∈ rather than contains, the second lemma gets the shorter name.
-
-## Special cases
-
-There are certain special “keywords” that may appear in identifiers.
-
-| Keyword | Meaning | Example |
-| :---- | :---- | :---- |
-| `def` | Unfold a definition. Avoid this for public APIs. | `Nat.max_def` |
-| `refl` | Theorems of the form `a R a`, where R is a reflexive relation and `a` is an explicit parameter | `Nat.le_refl` |
-| `rfl` | Like `refl`, but with `a` implicit | `Nat.le_rfl` |
-| `irrefl` | Theorems of the form `¬a R a`, where R is an irreflexive relation | `Nat.lt_irrefl` |
-| `symm` | Theorems of the form `a R b → b R a`, where R is a symmetric relation (compare `comm` below) | `Eq.symm` |
-| `trans` | Theorems of the form `a R b → b R c → a R c`, where R is a transitive relation (R may carry data) | `Eq.trans` |
-| `antisymmm` | Theorems of the form `a R b → b R a → a = b`, where R is an antisymmetric relation | `Nat.le_antisymm` |
-| `congr` | Theorems of the form `a R b → f a S f b`, where R and S are usually equivalence relations | `Std.HashMap.mem_congr` |
-| `comm` | Theorems of the form `f a b = f b a` (compare `symm` above) | `Eq.comm`, `Nat.add_comm` |
-| `assoc` | Theorems of the form `g (f a b) c = f a (g b c)` (note the order! In most cases, we have f = g) | `Nat.add_sub_assoc` |
-| `distrib` | Theorems of the form `f (g a b) = g (f a) (f b)` | `Nat.add_left_distrib` |
-| `self` | May be used if a variable appears multiple times in the conclusion | `List.mem_cons_self` |
-| `inj` | Theorems of the form `f a = f b ↔ a = b`. | `Int.neg_inj`, `Nat.add_left_inj` |
-| `cancel` | Theorems which have one of the forms `f a = f b → a = b` or `g (f a) = a`, where `f` and `g` usually involve a binary operator | `Nat.add_sub_cancel` |
-| `cancel_iff` | Same as `inj`, but with different conventions for left and right (see below) | `Nat.add_right_cancel_iff` |
-| `ext` | Theorems of the form `f a = f b → a = b`, where `f` usually involves some kind of projection | `List.ext_getElem`
-| `mono` | Theorems of the form `a R b → f a R f b`, where `R` is a transitive relation | `List.countP_mono_left`
-
-### Left and right
-
-The keywords left and right are useful to disambiguate symmetric variants of theorems.
-
-```lean
-theorem imp_congr_left (h : a ↔ b) : (a → c) ↔ (b → c) := sorry
-theorem imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) := sorry
-```
-
-It is not always obvious which version of a theorem should be “left” and which should be “right”.
-Heuristically, the theorem should name the side which is “more variable”, but there are exceptions. For some of the special keywords discussed in this section, there are conventions which should be followed, as laid out in the following examples:
-
-```lean
-theorem Nat.left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := sorry
-theorem Nat.right_distrib (n m k : Nat) : (n + m) * k = n * k + m * k := sorry
-theorem Nat.add_left_cancel {n m k : Nat} : n + m = n + k → m = k := sorry
-theorem Nat.add_right_cancel {n m k : Nat} : n + m = k + m → n = k := sorry
-theorem Nat.add_left_cancel_iff {m k n : Nat} : n + m = n + k ↔ m = k := sorry
-theorem Nat.add_right_cancel_iff {m k n : Nat} : m + n = k + n ↔ m = k := sorry
-theorem Nat.add_left_inj {m k n : Nat} : m + n = k + n ↔ m = k := sorry
-theorem Nat.add_right_inj {m k n : Nat} : n + m = n + k ↔ m = k := sorry
-```
-
-Note in particular that the convention is opposite for `cancel_iff` and `inj`.
-
-```lean
-theorem Nat.add_sub_self_left (a b : Nat) : (a + b) - a = b := sorry
-theorem Nat.add_sub_self_right (a b : Nat) : (a + b) - b = a := sorry
-theorem Nat.add_sub_cancel (n m : Nat) : (n + m) - m = n := sorry
-```
-
-## Primed names
-
-Avoid disambiguating variants of a concept by appending the `'` character (e.g., introducing both `BitVec.sshiftRight` and `BitVec.sshiftRight'`), as it is impossible to tell the difference without looking at the type signature, the documentation or even the code, and even if you know what the two variants are there is no way to tell which is which. Prefer descriptive pairs `BitVec.sshiftRightNat`/`BitVec.sshiftRight`.
-
-## Acronyms
-
-For acronyms which are three letters or shorter, all letters should use the same case as dictated by the convention. For example, `IO` is a correct name for a type and the name `IO.Ref` may become `IORef` when used as part of a definition name and `ioRef` when used as part of a theorem name.
-
-For acronyms which are at least four letters long, switch to lower case starting from the second letter. For example, `Json` is a correct name for a type, as is `JsonRPC`.
-
-If an acronym is typically spelled using mixed case, this mixed spelling may be used in identifiers (for example `Std.Net.IPv4Addr`).
-
-## Simp sets
-
-Simp sets centered around a conversion function should be called `source_to_target`. For example, a simp set for the `BitVec.toNat` function, which goes from `BitVec` to
-`Nat`, should be called `bitvec_to_nat`.
-
-## Variable names
-
-We make the following recommendations for variable names, but without insisting on them:
-* Simple hypotheses should be named `h`, `h'`, or using a numerical sequence `h₁`, `h₂`, etc.
-* Another common name for a simple hypothesis is `w` (for "witness").
-* `List`s should be named `l`, `l'`, `l₁`, etc, or `as`, `bs`, etc.
-  (Use of `as`, `bs` is encouraged when the lists are of different types, e.g. `as : List α` and `bs : List β`.)
-  `xs`, `ys`, `zs` are allowed, but it is better if these are reserved for `Array` and `Vector`.
-  A list of lists may be named `L`.
-* `Array`s should be named `xs`, `ys`, `zs`, although `as`, `bs` are encouraged when the arrays are of different types, e.g. `as : Array α` and `bs : Array β`.
-  An array of arrays may be named `xss`.
-* `Vector`s should be named `xs`, `ys`, `zs`, although `as`, `bs` are encouraged when the vectors are of different types, e.g. `as : Vector α n` and `bs : Vector β n`.
-  A vector of vectors may be named `xss`.
-* A common exception for `List` / `Array` / `Vector` is to use `acc` for an accumulator in a recursive function.
-* `i`, `j`, `k` are preferred for numerical indices.
-  Descriptive names such as `start`, `stop`, `lo`, and `hi` are encouraged when they increase readability.
-* `n`, `m` are preferred for sizes, e.g. in `Vector α n` or `xs.size = n`.
-* `w` is preferred for the width of a `BitVec`.

doc/std/style.md

@@ -1,522 +0,0 @@
-# Standard library style
-
-Please take some time to familiarize yourself with the stylistic conventions of
-the project and the specific part of the library you are planning to contribute
-to. While the Lean compiler may not enforce strict formatting rules,
-consistently formatted code is much easier for others to read and maintain.
-Attention to formatting is more than a cosmetic concern—it reflects the same
-level of precision and care required to meet the deeper standards of the Lean 4
-standard library.
-
-Below we will give specific formatting prescriptions for various language constructs. Note that this style guide only applies to the Lean standard library, even though some examples in the guide are taken from other parts of the Lean code base.
-
-## Basic whitespace rules
-
-Syntactic elements (like `:`, `:=`, `|`, `::`) are surrounded by single spaces, with the exception of `,` and `;`, which are followed by a space but not preceded by one. Delimiters (like `()`, `{}`) do not have spaces on the inside, with the exceptions of subtype notation and structure instance notation.
-
-Examples of correctly formatted function parameters:
-
-* `{α : Type u}`
-* `[BEq α]`
-* `(cmp : α → α → Ordering)`
-* `(hab : a = b)`
-* `{d : { l : List ((n : Nat) × Vector Nat n) // l.length % 2 = 0 }}`
-
-Examples of correctly formatted terms:
-
-* `1 :: [2, 3]`
-* `letI : Ord α := ⟨cmp⟩; True`
-* `(⟨2, 3⟩ : Nat × Nat)`
-* `((2, 3) : Nat × Nat)`
-* `{ x with fst := f (4 + f 0), snd := 4, .. }`
-* `match 1 with | 0 => 0 | _ => 0`
-* `fun ⟨a, b⟩ _ _ => by cases hab <;> apply id; rw [hbc]`
-
-Configure your editor to remove trailing whitespace. If you have set up Visual Studio Code for Lean development in the recommended way then the correct setting is applied automatically.
-
-## Splitting terms across multiple lines
-
-When splitting a term across multiple lines, increase indentation by two spaces starting from the second line. When splitting a function application, try to split at argument boundaries. If an argument itself needs to be split, increase indentation further as appropriate.
-
-When splitting at an infix operator, the operator goes at the end of the first line, not at the beginning of the second line. When splitting at an infix operator, you may or may not increase indentation depth, depending on what is more readable.
-
-When splitting an `if`-`then`-`else` expression, the `then` keyword wants to stay with the condition and the `else` keyword wants to stay with the alternative term. Otherwise, indent as if the `if` and `else` keywords were arguments to the same function.
-
-When splitting a comma-separated bracketed sequence (i.e., anonymous constructor application, list/array/vector literal, tuple) it is allowed to indent subsequent lines for alignment, but indenting by two spaces is also allowed.
-
-Do not orphan parentheses.
-
-Correct:
-```lean
-def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=
-  v₁.name.isPrefixOf v₂.name &&
-  v₁.scopes == v₂.scopes &&
-  v₁.mainModule == v₂.mainModule &&
-  v₁.imported == v₂.imported
-```
-
-Correct:
-```lean
-theorem eraseP_eq_iff {p} {l : List α} :
-    l.eraseP p = l' ↔
-      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
-        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧
-          l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ :=
-  sorry
-```
-
-Correct:
-```lean
-example : Nat :=
-  functionWithAVeryLongNameSoThatSomeArgumentsWillNotFit firstArgument secondArgument
-    (firstArgumentWithAnEquallyLongNameAndThatFunctionDoesHaveMoreArguments firstArgument
-      secondArgument)
-    secondArgument
-```
-
-Correct:
-```lean
-theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
-    (m.alter k f).size =
-      if m.contains k && (f (m.get? k)).isNone then
-        m.size - 1
-      else if !m.contains k && (f (m.get? k)).isSome then
-        m.size + 1
-      else
-        m.size := by
- simp_to_raw using Raw₀.size_alter
-```
-
-Correct:
-```lean
-theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
-    (m.alter k f).get? k' =
-      if h : k == k' then
-        cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k))
-      else m.get? k' := by
- simp_to_raw using Raw₀.get?_alter
-```
-
-Correct:
-```lean
-example : Nat × Nat :=
-  ⟨imagineThisWasALongTerm,
-   imagineThisWasAnotherLongTerm⟩
-```
-
-Correct:
-```lean
-example : Nat × Nat :=
-  ⟨imagineThisWasALongTerm,
-    imagineThisWasAnotherLongTerm⟩
-```
-
-Correct:
-```lean
-example : Vector Nat :=
-  #v[imagineThisWasALongTerm,
-     imagineThisWasAnotherLongTerm]
-```
-
-## Basic file structure
-
-Every file should start with a copyright header, imports (in the standard library, this always includes a `prelude` declaration) and a module documentation string. There should not be a blank line between the copyright header and the imports. There should be a blank line between the imports and the module documentation string.
-
-If you explicitly declare universe variables, do so at the top of the file, after the module documentation.
-
-Correct:
-```lean
-/-
-Copyright (c) 2014 Parikshit Khanna. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro,
-  Yury Kudryashov
--/
-prelude
-import Init.Data.List.Pairwise
-import Init.Data.List.Find
-
-/-!
-**# Lemmas about `List.eraseP` and `List.erase`.**
--/
-
-universe u u'
-```
-
-Syntax that is not supposed to be user-facing must be scoped. New public syntax must always be discussed explicitly in an RFC.
-
-## Top-level commands and declarations
-
-All top-level commands are unindented. Sectioning commands like `section` and `namespace` do not increase the indentation level.
-
-Attributes may be placed on the same line as the rest of the command or on a separate line.
-
-Multi-line declaration headers are indented by four spaces starting from the second line. The colon that indicates the type of a declaration may not be placed at the start of a line or on its own line.
-
-Declaration bodies are indented by two spaces. Short declaration bodies may be placed on the same line as the declaration type.
-
-Correct:
-```lean
-theorem eraseP_eq_iff {p} {l : List α} :
-    l.eraseP p = l' ↔
-      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
-        ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧
-          l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ :=
-  sorry
-```
-
-Correct:
-```lean
-@[simp] theorem eraseP_nil : [].eraseP p = [] := rfl
-```
-
-Correct:
-```lean
-@[simp]
-theorem eraseP_nil : [].eraseP p = [] := rfl
-```
-
-### Documentation comments
-
-Note to external contributors: this is a section where the Lean style and the mathlib style are different.
-
-Declarations should be documented as required by the `docBlame` linter, which may be activated in a file using
-`set_option linter.missingDocs true` (we allow these to stay in the file).
-
-Single-line documentation comments should go on the same line as `/--`/`-/`, while multi-line documentation strings
-should have these delimiters on their own line, with the documentation comment itself unindented.
-
-Documentation comments must be written in the indicative mood. Use American orthography.
-
-Correct:
-```lean
-/-- Carries out a monadic action on each mapping in the hash map in some order. -/
-@[inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit :=
-  b.buckets.forM (AssocList.forM f)
-```
-
-Correct:
-```lean
-/--
-Monadically computes a value by folding the given function over the mappings in the hash
-map in some order.
--/
-@[inline] def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (b : Raw α β) : m δ :=
-  b.buckets.foldlM (fun acc l => l.foldlM f acc) init
-```
-
-### Where clauses
-
-The `where` keyword should be unindented, and all declarations bound by it should be indented with two spaces.
-
-Blank lines before and after `where` and between declarations bound by `where` are optional and should be chosen
-to maximize readability.
-
-Correct:
-```lean
-@[simp] theorem partition_eq_filter_filter (p : α → Bool) (l : List α) :
-    partition p l = (filter p l, filter (not ∘ p) l) := by
-  simp [partition, aux]
-where
-  aux (l) {as bs} : partition.loop p l (as, bs) =
-      (as.reverse ++ filter p l, bs.reverse ++ filter (not ∘ p) l) :=
-    match l with
-    | [] => by simp [partition.loop, filter]
-    | a :: l => by cases pa : p a <;> simp [partition.loop, pa, aux, filter, append_assoc]
-```
-
-### Termination arguments
-
-The `termination_by`, `decreasing_by`, `partial_fixpoint` keywords should be unindented. The associated terms should be indented like declaration bodies.
-
-Correct:
-```lean
-@[inline] def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do
-  let rec loop (p : String.Pos) := do
-    if h : opt.atEnd p then
-      return
-    else
-      handle (opt.get' p h)
-      loop (opt.next' p h)
-  termination_by opt.utf8ByteSize - p.byteIdx
-  decreasing_by
-    simp [String.atEnd] at h
-    apply Nat.sub_lt_sub_left h
-    simp [String.lt_next opt p]
-  loop ⟨1⟩
-```
-
-Correct:
-```lean
-def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) : Bool :=
-  off1.byteIdx + sz ≤ s1.endPos.byteIdx && off2.byteIdx + sz ≤ s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
-where
-  loop (off1 off2 stop1 : Pos) :=
-    if _h : off1.byteIdx < stop1.byteIdx then
-      let c₁ := s1.get off1
-      let c₂ := s2.get off2
-      c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
-    else true
-  termination_by stop1.1 - off1.1
-  decreasing_by
-    have := Nat.sub_lt_sub_left _h (Nat.add_lt_add_left c₁.utf8Size_pos off1.1)
-    decreasing_tactic
-```
-
-Correct:
-```lean
-theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
-  rw [div_eq, mod_eq]
-  have h : Decidable (0 < n ∧ n ≤ m) := inferInstance
-  cases h with
-  | isFalse h => simp [h]
-  | isTrue h =>
-    simp [h]
-    have ih := div_add_mod (m - n) n
-    rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
-decreasing_by apply div_rec_lemma; assumption
-```
-
-### Deriving
-
-The `deriving` clause should be unindented.
-
-Correct:
-```lean
-structure Iterator where
-  array : ByteArray
-  idx : Nat
-deriving Inhabited
-```
-
-## Notation and Unicode
-
-We generally prefer to use notation as available. We usually prefer the Unicode versions of notations over non-Unicode alternatives.
-
-There are some rules and exceptions regarding specific notations which are listed below:
-
-* Sigma types: use `(a : α) × β a` instead of `Σ a, β a` or `Sigma β`.
-* Function arrows: use `fun a => f x` instead of `fun x ↦ f x` or `λ x => f x` or any other variant.
-
-## Language constructs
-
-### Pattern matching, induction etc.
-
-Match arms are indented at the indentation level that the match statement would have if it was on its own line. If the match is implicit, then the arms should be indented as if the match was explicitly given. The content of match arms is indented two spaces, so that it appears on the same level as the match pattern.
-
-Correct:
-```lean
-def alter [BEq α] {β : Type v} (a : α) (f : Option β → Option β) :
-    AssocList α (fun _ => β) → AssocList α (fun _ => β)
-  | nil => match f none with
-    | none => nil
-    | some b => AssocList.cons a b nil
-  | cons k v l =>
-    if k == a then
-      match f v with
-      | none => l
-      | some b => cons a b l
-    else
-      cons k v (alter a f l)
-```
-
-Correct:
-```lean
-theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
-    ∃ as bs, xs = as ++ a :: bs ∧ a ∉ as := by
-  induction xs with
-  | nil => cases h
-  | cons x xs ih =>
-    simp at h
-    cases h with
-    | inl h => exact ⟨[], xs, by simp_all⟩
-    | inr h =>
-      by_cases h' : a = x
-      · subst h'
-        exact ⟨[], xs, by simp⟩
-      · obtain ⟨as, bs, rfl, h⟩ := ih h
-        exact ⟨x :: as, bs, rfl, by simp_all⟩
-```
-
-Aligning match arms is allowed, but not required.
-
-Correct:
-```lean
-def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
-  match h₁?, h₂? with
-  | none, none       => return none
-  | none, some h     => return h
-  | some h, none     => return h
-  | some h₁, some h₂ => mkEqTrans h₁ h₂
-```
-
-Correct:
-```lean
-def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
-  match h₁?, h₂? with
-  | none, none => return none
-  | none, some h => return h
-  | some h, none => return h
-  | some h₁, some h₂ => mkEqTrans h₁ h₂
-```
-
-Correct:
-```lean
-def mkEqTrans? (h₁? h₂? : Option Expr) : MetaM (Option Expr) :=
-  match h₁?, h₂? with
-  | none,    none    => return none
-  | none,    some h  => return h
-  | some h,  none    => return h
-  | some h₁, some h₂ => mkEqTrans h₁ h₂
-```
-
-### Structures
-
-Note to external contributors: this is a section where the Lean style and the mathlib style are different.
-
-When using structure instance syntax over multiple lines, the opening brace should go on the preceding line, while the closing brace should go on its own line. The rest of the syntax should be indented by one level. During structure updates, the `with` clause goes on the same line as the opening brace. Aligning at the assignment symbol is allowed but not required.
-
-Correct:
-```lean
-def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (reportExts := true) :
-    IO AddConstAsyncResult := do
-  let sigPromise ← IO.Promise.new
-  let infoPromise ← IO.Promise.new
-  let extensionsPromise ← IO.Promise.new
-  let checkedEnvPromise ← IO.Promise.new
-  let asyncConst := {
-    constInfo := {
-      name := constName
-      kind
-      sig := sigPromise.result
-      constInfo := infoPromise.result
-    }
-    exts? := guard reportExts *> some extensionsPromise.result
-  }
-  return {
-    constName, kind
-    mainEnv := { env with
-      asyncConsts := env.asyncConsts.add asyncConst
-      checked := checkedEnvPromise.result }
-    asyncEnv := { env with
-      asyncCtx? := some { declPrefix := privateToUserName constName.eraseMacroScopes }
-    }
-    sigPromise, infoPromise, extensionsPromise, checkedEnvPromise
-  }
-```
-
-Correct:
-```lean
-instance [Inhabited α] : Inhabited (Descr α β σ) where
-  default := {
-    name         := default
-    mkInitial    := default
-    ofOLeanEntry := default
-    toOLeanEntry := default
-    addEntry     := fun s _ => s
-  }
-```
-
-### Declaring structures
-
-When defining structure types, do not parenthesize structure fields.
-
-When declaring a structure type with a custom constructor name, put the custom name on its own line, indented like the
-structure fields, and add a documentation comment.
-
-Correct:
-
-```lean
-/--
-A bitvector of the specified width.
-
-This is represented as the underlying `Nat` number in both the runtime
-and the kernel, inheriting all the special support for `Nat`.
--/
-structure BitVec (w : Nat) where
-  /--
-  Constructs a `BitVec w` from a number less than `2^w`.
-  O(1), because we use `Fin` as the internal representation of a bitvector.
-  -/
-  ofFin ::
-  /--
-  Interprets a bitvector as a number less than `2^w`.
-  O(1), because we use `Fin` as the internal representation of a bitvector.
-  -/
-  toFin : Fin (2 ^ w)
-```
-
-## Tactic proofs
-
-Tactic proofs are the most common thing to break during any kind of upgrade, so it is important to write them in a way that minimizes the likelihood of proofs breaking and that makes it easy to debug breakages if they do occur.
-
-If there are multiple goals, either use a tactic combinator (like `all_goals`) to operate on all of them or a clearly specified subset, or use focus dots to work on goals one at a time. Using structured proofs (e.g., `induction … with`) is encouraged but not mandatory.
-
-Squeeze non-terminal `simp`s (i.e., calls to `simp` which do not close the goal). Squeezing terminal `simp`s is generally discouraged, although there are exceptions (for example if squeezing yields a noticeable performance improvement).
-
-Do not over-golf proofs in ways that are likely to lead to hard-to-debug breakage. Examples of things to avoid include complex multi-goal manipulation using lots of tactic combinators, complex uses of the substitution operator (`▸`) and clever point-free expressions (possibly involving anonymous function notation for multiple arguments).
-
-Do not under-golf proofs: for routine tasks, use the most powerful tactics available.
-
-Do not use `erw`. Avoid using `rfl` after `simp` or `rw`, as this usually indicates a missing lemma that should be used instead of `rfl`.
-
-Use `(d)simp` or `rw` instead of `delta` or `unfold`. Use `refine` instead of `refine’`. Use `haveI` and `letI` only if they are actually required.
-
-Prefer highly automated tactics (like `grind` and `omega`) over low-level proofs, unless the automated tactic requires unacceptable additional imports or has bad performance. If you decide against using a highly automated tactic, leave a comment explaining the decision.
-
-## `do` notation
-
-The `do` keyword goes on the same line as the corresponding `:=` (or `=>`, or similar). `Id.run do` should be treated as if it was a bare `do`.
-
-Use early `return` statements to reduce nesting depth and make the non-exceptional control flow of a function easier to see.
-
-Alternatives for `let` matches may be placed in the same line or in the next line, indented by two spaces. If the term that is
-being matched on is itself more than one line and there is an alternative present, consider breaking immediately after `←` and indent
-as far as necessary to ensure readability.
-
-Correct:
-```lean
-def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
-  let some decl ← findFunDecl? fvarId | throwError "unknown local function {fvarId.name}"
-  return decl
-```
-
-Correct:
-```lean
-def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
-  let some decl ←
-        findFunDecl? fvarId
-    | throwError "unknown local function {fvarId.name}"
-  return decl
-```
-
-Correct:
-```lean
-def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
-  let some decl ← findFunDecl?
-      fvarId
-    | throwError "unknown local function {fvarId.name}"
-  return decl
-```
-
-Correct:
-```lean
-def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do
-  let mctx ← getMCtx
-  let mut numAnonymous := 0
-  for g in newGoals do
-    if mctx.isAnonymousMVar g then
-      numAnonymous := numAnonymous + 1
-  modifyMCtx fun mctx => Id.run do
-    let mut mctx := mctx
-    let mut idx  := 1
-    for g in newGoals do
-      if mctx.isAnonymousMVar g then
-        if numAnonymous == 1 then
-          mctx := mctx.setMVarUserName g parentTag
-        else
-          mctx := mctx.setMVarUserName g (parentTag ++ newSuffix.appendIndexAfter idx)
-        idx := idx + 1
-    pure mctx
-```
-

doc/std/vision.md

@@ -1,98 +0,0 @@
-# The Lean 4 standard library
-
-Maintainer team (in alphabetical order): Henrik Böving, Markus Himmel
-(community contact & external contribution coordinator), Kim Morrison, Paul
-Reichert, Sofia Rodrigues.
-
-The Lean 4 standard library is a core part of the Lean distribution, providing
-essential building blocks for functional programming, verified software
-development, and software verification. Unlike the standard libraries of most
-other languages, many of its components are formally verified and can be used
-as part of verified applications.
-
-The standard library is a public API that contains the components listed in the
-standard library outline below. Not all public APIs in the Lean distribution
-are part of the standard library, and the standard library does not correspond
-to a certain directory within the Lean source repository (like `Std`). For
-example, the metaprogramming framework is not part of the standard library, but
-basic types like `True` and `Nat` are.
-
-The standard library is under active development. Our guiding principles are:
-
-* Provide comprehensive, verified building blocks for real-world software.
-* Build a public API of the highest quality with excellent internal consistency.
-* Carefully optimize components that may be used in performance-critical software.
-* Ensure smooth adoption and maintenance for users.
-* Offer excellent documentation, example projects, and guides.
-* Provide a reliable and extensible basis that libraries for software
-  development, software verification and mathematics can build on.
-
-The standard library is principally developed by the Lean FRO. Community
-contributions are welcome. If you would like to contribute, please refer to the
-call for contributions below.
-
-### Standard library outline
-
-1. Core types and operations
-   1. Basic types
-   2. Numeric types, including floating point numbers
-   3. Containers
-   4. Strings and formatting
-2. Language constructs
-   1. Ranges and iterators
-   2. Comparison, ordering, hashing and related type classes
-   3. Basic monad infrastructure
-3. Libraries
-   1. Random numbers
-   2. Dates and times
-4. Operating system abstractions
-   1. Concurrency and parallelism primitives
-   2. Asynchronous I/O
-   3. FFI helpers
-   4. Environment, file system, processes
-   5. Locales
-
-The material covered in the first three sections (core types and operations,
-language constructs and libraries) will be verified, with the exception of
-floating point numbers and the parts of the libraries that interface with the
-operating system (e.g., sources of operating system randomness or time zone
-database access).
-
-### Call for contributions
-
-Thank you for taking interest in contributing to the Lean standard library\!
-There are two main ways for community members to contribute to the Lean
-standard library: by contributing experience reports or by contributing code
-and lemmas.
-
-**If you are using Lean for software verification or verified software
-development:** hearing about your experiences using Lean and its standard
-library for software verification is extremely valuable to us. We are committed
-to building a standard library suitable for real-world applications and your
-input will directly influence the continued evolution of the Lean standard
-library. Please reach out to the standard library maintainer team via Zulip
-(either in a public thread in the \#lean4 channel or via direct message). Even
-just a link to your code helps. Thanks\!
-
-**If you have code that you believe could enhance the Lean 4 standard
-library:** we encourage you to initiate a discussion in the \#lean4 channel on
-Zulip. This is the most effective way to receive preliminary feedback on your
-contribution. The Lean standard library has a very precise scope and it has
-very high quality standards, so at the moment we are mostly interested in
-contributions that expand upon existing material rather than introducing novel
-concepts.
-
-**If you would like to contribute code to the standard library but don’t know
-what to work on:** we are always excited to meet motivated community members
-who would like to contribute, and there is always impactful work that is
-suitable for new contributors. Please reach out to Markus Himmel on Zulip to
-discuss possible contributions.
-
-As laid out in the [project-wide External Contribution
-Guidelines](../../CONTRIBUTING.md),
-PRs are much more likely to be merged if they are preceded by an RFC or if you
-discussed your planned contribution with a member of the standard library
-maintainer team. When in doubt, introducing yourself is always a good idea.
-
-All code in the standard library is expected to strictly adhere to the
-[standard library coding conventions](./style.md).

script/benchReelabRss.lean

@@ -8,12 +8,12 @@ open Lean.JsonRpc
 Tests language server memory use by repeatedly re-elaborate a given file.
 
 NOTE: only works on Linux for now.
+ot to touch the imports for usual files.
 -/
 
 def main (args : List String) : IO Unit := do
   let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
-  let file ← IO.FS.realPath file
-  let uri := s!"file://{file}"
+  let uri := s!"file:///{file}"
   Ipc.runWith leanCmd (#["--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
   -- for use with heaptrack:
   --Ipc.runWith "heaptrack" (#[leanCmd, "--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do

src/CMakeLists.txt

@@ -689,7 +689,7 @@ add_custom_target(make_stdlib ALL
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
   # for a parallelized nested build, but CMake doesn't let us do that.
   # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean Leanc
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
   VERBATIM)
 
 # if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
@@ -768,7 +768,7 @@ if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean AND NOT ${CMAKE_S
   add_custom_target(leanc ALL
     WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
     DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanc
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanc
     VERBATIM)
 endif()
 
@@ -823,6 +823,7 @@ endif()
 
 # Escape for `make`. Yes, twice.
 string(REPLACE "$" "\\\$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
+string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
 configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
 
 # hacky

src/Init/BinderNameHint.lean

@@ -40,5 +40,5 @@ This gadget is supported by
 It is ineffective in other positions (hyptheses of rewrite rules) or when used by other tactics
 (e.g. `apply`).
 -/
-@[simp ↓, expose]
+@[simp ↓]
 def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e

src/Init/Classical.lean

@@ -107,8 +107,8 @@ noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
   (strongIndefiniteDescription p h).property
 
-theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α hex.nonempty p) :=
-  epsilon_spec_aux hex.nonempty p hex
+theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
+  epsilon_spec_aux (nonempty_of_exists hex) p hex
 
 theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
   @epsilon_spec α (fun y => y = x) ⟨x, rfl⟩

src/Init/Control/Except.lean

@@ -127,7 +127,7 @@ end Except
 /--
 Adds exceptions of type `ε` to a monad `m`.
 -/
-@[expose] def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
+def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
   m (Except ε α)
 
 /--

src/Init/Control/ExceptCps.lean

@@ -18,7 +18,7 @@ Adds exceptions of type `ε` to a monad `m`.
 Instead of using `Except ε` to model exceptions, this implementation uses continuation passing
 style. This has different performance characteristics from `ExceptT ε`.
 -/
-@[expose] def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
+def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
 
 namespace ExceptCpsT
 

src/Init/Control/Id.lean

@@ -34,7 +34,7 @@ def containsFive (xs : List Nat) : Bool := Id.run do
 true
 ```
 -/
-@[expose] def Id (type : Type u) : Type u := type
+def Id (type : Type u) : Type u := type
 
 namespace Id
 
@@ -56,7 +56,7 @@ Runs a computation in the identity monad.
 This function is the identity function. Because its parameter has type `Id α`, it causes
 `do`-notation in its arguments to use the `Monad Id` instance.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def run (x : Id α) : α := x
 
 instance [OfNat α n] : OfNat (Id α) n :=

src/Init/Control/Lawful/Instances.lean

@@ -7,8 +7,7 @@ module
 
 prelude
 import Init.Control.Lawful.Basic
-import all Init.Control.Except
-import all Init.Control.State
+import Init.Control.Except
 import Init.Control.StateRef
 import Init.Ext
 
@@ -99,7 +98,7 @@ end ExceptT
 
 instance : LawfulMonad (Except ε) := LawfulMonad.mk'
   (id_map := fun x => by cases x <;> rfl)
-  (pure_bind := fun _ _ => by rfl)
+  (pure_bind := fun _ _ => rfl)
   (bind_assoc := fun a _ _ => by cases a <;> rfl)
 
 instance : LawfulApplicative (Except ε) := inferInstance
@@ -248,7 +247,7 @@ instance : LawfulMonad (EStateM ε σ) := .mk'
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
-  (pure_bind := fun _ _ => by rfl)
+  (pure_bind := fun _ _ => rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
     dsimp only [EStateM.instMonad, EStateM.bind]
     match x s with

src/Init/Control/Option.lean

@@ -20,7 +20,7 @@ instance : ToBool (Option α) := ⟨Option.isSome⟩
 Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a
 failure occurred.
 -/
-@[expose] def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
+def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
   m (Option α)
 
 /--

src/Init/Control/State.lean

@@ -22,7 +22,7 @@ Adds a mutable state of type `σ` to a monad.
 Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple
 of a value and a state.
 -/
-@[expose] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)
 
 /--
@@ -47,7 +47,7 @@ A tuple-based state monad.
 Actions in `StateM σ` are functions that take an initial state and return a value paired with a
 final state.
 -/
-@[expose, reducible]
+@[reducible]
 def StateM (σ α : Type u) : Type u := StateT σ Id α
 
 instance {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α) where

src/Init/Control/StateCps.lean

@@ -18,7 +18,7 @@ The State monad transformer using CPS style.
 An alternative implementation of a state monad transformer that internally uses continuation passing
 style instead of tuples.
 -/
-@[expose] def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
+def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
 
 namespace StateCpsT
 

src/Init/Control/StateRef.lean

@@ -17,7 +17,7 @@ A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref ω σ`
 
 The macro `StateRefT σ m α` infers `ω` from `m`. It should normally be used instead.
 -/
-@[expose] def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
+def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 
 /-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/
 

src/Init/Core.lean

@@ -12,8 +12,6 @@ import Init.Prelude
 import Init.SizeOf
 set_option linter.missingDocs true -- keep it documented
 
-@[expose] section
-
 universe u v w
 
 /--
@@ -1212,7 +1210,10 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
 instance : Inhabited Prop where
   default := True
 
-deriving instance Inhabited for NonScalar, PNonScalar, True
+deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep
+
+theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
+  | ⟨w, _⟩ => ⟨w⟩
 
 /-! # Subsingleton -/
 
@@ -1386,7 +1387,16 @@ instance Sum.nonemptyLeft [h : Nonempty α] : Nonempty (Sum α β) :=
 instance Sum.nonemptyRight [h : Nonempty β] : Nonempty (Sum α β) :=
   Nonempty.elim h (fun b => ⟨Sum.inr b⟩)
 
-deriving instance DecidableEq for Sum
+instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
+  match a, b with
+  | Sum.inl a, Sum.inl b =>
+    if h : a = b then isTrue (h ▸ rfl)
+    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
+  | Sum.inr a, Sum.inr b =>
+    if h : a = b then isTrue (h ▸ rfl)
+    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
+  | Sum.inr _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
+  | Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h
 
 end
 

src/Init/Data/Array/Attach.lean

@@ -9,7 +9,7 @@ prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Count
-import all Init.Data.List.Attach
+import Init.Data.List.Attach
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Basic.lean

@@ -13,8 +13,8 @@ import Init.Data.UInt.BasicAux
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
-import all Init.Data.List.ToArrayImpl
-import all Init.Data.Array.Set
+import Init.Data.List.ToArrayImpl
+import Init.Data.Array.Set
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/BasicAux.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Array.Basic
+import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.NotationExtra
 

src/Init/Data/Array/Bootstrap.lean

@@ -8,7 +8,6 @@ module
 
 prelude
 import Init.Data.List.TakeDrop
-import all Init.Data.Array.Basic
 
 /-!
 ## Bootstrapping theorems about arrays
@@ -53,8 +52,8 @@ theorem foldlM_toList.aux [Monad m]
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_toList.aux (j := j+1) H]
     rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
-    simp
-  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; simp
+    rfl
+  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
 @[simp, grind =] theorem foldlM_toList [Monad m]
     {f : β → α → m β} {init : β} {xs : Array α} :
@@ -70,14 +69,14 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (xs.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f xs 0 i h init := by
   unfold foldrM.fold
   match i with
-  | 0 => simp
+  | 0 => simp [List.foldlM, List.take]
   | i+1 => rw [← List.take_concat_get h]; simp [← aux]
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
     xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by
   have : xs = #[] ∨ 0 < xs.size :=
     match xs with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
-  match xs, this with | _, .inl rfl => simp [foldrM] | xs, .inr h => ?_
+  match xs, this with | _, .inl rfl => rfl | xs, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
 @[simp, grind =] theorem foldrM_toList [Monad m]

src/Init/Data/Array/Count.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Count
 

src/Init/Data/Array/DecidableEq.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Array.Basic
+import Init.Data.Array.Basic
 import Init.Data.BEq
 import Init.Data.List.Nat.BEq
 import Init.ByCases

src/Init/Data/Array/Erase.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Nat.Basic

src/Init/Data/Array/Find.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 import Init.Data.List.Nat.Find
-import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.Array.Range

src/Init/Data/Array/GetLit.lean

@@ -27,13 +27,11 @@ theorem extLit {n : Nat}
     (h : (i : Nat) → (hi : i < n) → xs.getLit i hsz₁ hi = ys.getLit i hsz₂ hi) : xs = ys :=
   Array.ext (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
 
--- has to be expose for array literal support
-@[expose] def toListLitAux (xs : Array α) (n : Nat) (hsz : xs.size = n) : ∀ (i : Nat), i ≤ xs.size → List α → List α
+def toListLitAux (xs : Array α) (n : Nat) (hsz : xs.size = n) : ∀ (i : Nat), i ≤ xs.size → List α → List α
   | 0,     _,  acc => acc
   | (i+1), hi, acc => toListLitAux xs n hsz i (Nat.le_of_succ_le hi) (xs.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
 
--- has to be expose for array literal support
-@[expose] def toArrayLit (xs : Array α) (n : Nat) (hsz : xs.size = n) : Array α :=
+def toArrayLit (xs : Array α) (n : Nat) (hsz : xs.size = n) : Array α :=
   List.toArray <| toListLitAux xs n hsz n (hsz ▸ Nat.le_refl _) []
 
 theorem toArrayLit_eq (xs : Array α) (n : Nat) (hsz : xs.size = n) : xs = toArrayLit xs n hsz := by

src/Init/Data/Array/Lemmas.lean

@@ -8,13 +8,11 @@ module
 prelude
 import Init.Data.Nat.Lemmas
 import Init.Data.List.Range
-import all Init.Data.List.Control
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
 import Init.Data.List.Nat.Basic
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
-import all Init.Data.Array.Bootstrap
 import Init.Data.Array.Mem
 import Init.Data.Array.DecidableEq
 import Init.Data.Array.Lex.Basic
@@ -854,7 +852,7 @@ abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
     elem a xs = xs.contains a := by
   simp [elem]
 
-@[grind] theorem contains_empty [BEq α] : (#[] : Array α).contains a = false := by simp
+@[grind] theorem contains_empty [BEq α] : (#[] : Array α).contains a = false := rfl
 
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     elem a xs = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
@@ -871,8 +869,8 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
 @[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     xs.contains a = decide (a ∈ xs) := by rw [← elem_eq_contains, elem_eq_mem]
 
-@[simp, grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := by simp
-@[simp, grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp
+@[simp, grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := rfl
+@[simp, grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := rfl
 
 /-- Variant of `any_push` with a side condition on `stop`. -/
 @[simp, grind] theorem any_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
@@ -4154,7 +4152,7 @@ theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
 section replace
 variable [BEq α]
 
-@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by simp [replace]
+@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by rfl
 
 @[simp, grind] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
   simp only [replace, List.finIdxOf?_toArray, List.finIdxOf?]

src/Init/Data/Array/Lex/Lemmas.lean

@@ -6,7 +6,6 @@ Author: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Lex.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Lex
 
@@ -23,9 +22,9 @@ namespace Array
 @[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
 @[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
-protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
-    ¬ xs ≤ ys ↔ ys < xs :=
+protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
+    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
   Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by

src/Init/Data/Array/MapIdx.lean

@@ -6,11 +6,10 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.Array.OfFn
-import all Init.Data.List.MapIdx
+import Init.Data.List.MapIdx
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Monadic.lean

@@ -6,8 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.List.Control
-import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.List.Monadic

src/Init/Data/Array/OfFn.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.OfFn
 
@@ -26,11 +25,12 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩) := by
   ext i h₁ h₂
   · simp
-  · simp only [getElem_ofFn, getElem_push, size_ofFn, Fin.castSucc_mk, left_eq_dite_iff,
-      Nat.not_lt]
-    simp only [size_ofFn] at h₁
-    intro h₃
-    simp only [show i = n by omega]
+  · simp [getElem_push]
+    split <;> rename_i h₃
+    · rfl
+    · congr
+      simp at h₁ h₂
+      omega
 
 @[simp] theorem _root_.List.toArray_ofFn {f : Fin n → α} : (List.ofFn f).toArray = Array.ofFn f := by
   ext <;> simp

src/Init/Data/Array/Perm.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 import Init.Data.List.Nat.Perm
-import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.

src/Init/Data/Array/Range.lean

@@ -7,8 +7,7 @@ module
 
 prelude
 import Init.Data.Array.Lemmas
-import all Init.Data.Array.Basic
-import all Init.Data.Array.OfFn
+import Init.Data.Array.OfFn
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Zip
 import Init.Data.List.Nat.Range
@@ -81,7 +80,7 @@ theorem range'_append {s m n step : Nat} :
     range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)
 
 theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ #[s + step * n] := by
-  simp [← range'_append]
+  simpa using range'_append.symm
 
 theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ #[s + n] := by
   simp [range'_concat]

src/Init/Data/Array/Subarray/Split.lean

@@ -8,7 +8,7 @@ module
 
 prelude
 import Init.Data.Array.Basic
-import all Init.Data.Array.Subarray
+import Init.Data.Array.Subarray
 import Init.Omega
 
 /-

src/Init/Data/Array/TakeDrop.lean

@@ -6,7 +6,6 @@ Authors: Markus Himmel
 module
 
 prelude
-import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.TakeDrop
 

src/Init/Data/Array/Zip.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
 import Init.Data.Array.TakeDrop
 import Init.Data.List.Zip
 

src/Init/Data/BitVec/BasicAux.lean

@@ -22,7 +22,7 @@ section Nat
 /--
 The bitvector with value `i mod 2^n`.
 -/
-@[expose, match_pattern]
+@[match_pattern]
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
   toFin := Fin.ofNat' (2^n) i
 

src/Init/Data/BitVec/Bitblast.lean

@@ -7,11 +7,9 @@ module
 
 prelude
 import Init.Data.BitVec.Folds
-import all Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Mod
-import all Init.Data.Int.DivMod
 import Init.Data.Int.LemmasAux
-import all Init.Data.BitVec.Lemmas
+import Init.Data.BitVec.Lemmas
 
 /-!
 # Bit blasting of bitvectors

src/Init/Data/BitVec/Folds.lean

@@ -6,7 +6,6 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
-import all Init.Data.BitVec.Basic
 import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate

src/Init/Data/BitVec/Lemmas.lean

@@ -8,8 +8,7 @@ module
 
 prelude
 import Init.Data.Bool
-import all Init.Data.BitVec.Basic
-import all Init.Data.BitVec.BasicAux
+import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Div.Lemmas
@@ -344,7 +343,7 @@ theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
   cases b <;> rfl
 
 @[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by
-  cases b <;> simp
+  cases b <;> rfl
 
 @[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by
   cases b <;> rfl
@@ -1973,7 +1972,7 @@ theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
 /-! ### shiftLeft reductions from BitVec to Nat -/
 
 @[simp]
-theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := rfl
+theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := by rfl
 
 theorem shiftLeft_zero' {x : BitVec w₁} : x <<< 0#w₂ = x := by simp
 
@@ -2133,7 +2132,7 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
 
 @[simp]
 theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) :
-    x >>> y = x >>> y.toNat := rfl
+    x >>> y = x >>> y.toNat := by rfl
 
 theorem ushiftRight_ofNat_eq {x : BitVec w} {k : Nat} : x >>> (BitVec.ofNat w k) = x >>> (k % 2^w) := rfl
 
@@ -2261,7 +2260,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
-  simp only [getElem_sshiftRight, Nat.add_assoc, msb_sshiftRight, dite_eq_ite]
+  simp [getElem_sshiftRight, getLsbD_sshiftRight, Nat.add_assoc]
   by_cases h₂ : n + i < w
   · simp [h₂]
   · simp only [h₂, ↓reduceIte]
@@ -3373,7 +3372,7 @@ theorem add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b := by
 
 /-! ### sub/neg -/
 
-theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := rfl
+theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
 
 @[simp] theorem toNat_sub {n} (x y : BitVec n) :
     (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
@@ -3684,7 +3683,7 @@ theorem fill_false {w : Nat} : fill w false = 0#w := by
 
 /-! ### mul -/
 
-theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := rfl
+theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
 
 @[simp, bitvec_to_nat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
 @[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
@@ -3732,10 +3731,6 @@ theorem mul_add {x y z : BitVec w} :
   rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
     ← Nat.mul_mod, Nat.mul_add]
 
-theorem add_mul {x y z : BitVec w} :
-    (x + y) * z = x * z + y * z := by
-  rw [BitVec.mul_comm, mul_add, BitVec.mul_comm z, BitVec.mul_comm z]
-
 theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add]
 theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]
 
@@ -4167,7 +4162,7 @@ theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
   have hy : y = 0#1 ∨ y = 1#1 := by bv_omega
   rcases hx with rfl | rfl <;>
     rcases hy with rfl | rfl <;>
-      simp
+      rfl
 
 @[simp]
 theorem sdiv_self {x : BitVec w} :
@@ -5350,7 +5345,7 @@ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
 
 /-! ### abs -/
 
-theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := rfl
+theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
 
 @[simp, bitvec_to_nat]
 theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by

src/Init/Data/Bool.lean

@@ -432,7 +432,7 @@ theorem and_or_inj_left_iff :
 /--
 Converts `true` to `1` and `false` to `0`.
 -/
-@[expose] def toNat (b : Bool) : Nat := cond b 1 0
+def toNat (b : Bool) : Nat := cond b 1 0
 
 @[simp, bitvec_to_nat] theorem toNat_false : false.toNat = 0 := rfl
 
@@ -687,7 +687,7 @@ def boolPredToPred : Coe (α → Bool) (α  → Prop) where
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
-@[expose] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/

src/Init/Data/ByteArray/Basic.lean

@@ -9,7 +9,6 @@ prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.Subarray
 import Init.Data.UInt.Basic
-import all Init.Data.UInt.BasicAux
 import Init.Data.Option.Basic
 universe u
 

src/Init/Data/Cast.lean

@@ -64,7 +64,7 @@ class NatCast (R : Type u) where
 
 instance : NatCast Nat where natCast n := n
 
-@[coe, expose, reducible, match_pattern, inherit_doc NatCast]
+@[coe, reducible, match_pattern, inherit_doc NatCast]
 protected def Nat.cast {R : Type u} [NatCast R] : Nat → R :=
   NatCast.natCast
 

src/Init/Data/Char/Basic.lean

@@ -20,13 +20,13 @@ namespace Char
 /--
 One character is less than another if its code point is strictly less than the other's.
 -/
-@[expose] protected def lt (a b : Char) : Prop := a.val < b.val
+protected def lt (a b : Char) : Prop := a.val < b.val
 
 /--
 One character is less than or equal to another if its code point is less than or equal to the
 other's.
 -/
-@[expose] protected def le (a b : Char) : Prop := a.val ≤ b.val
+protected def le (a b : Char) : Prop := a.val ≤ b.val
 
 instance : LT Char := ⟨Char.lt⟩
 instance : LE Char := ⟨Char.le⟩

src/Init/Data/Char/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Char.Basic
+import Init.Data.Char.Basic
 import Init.Data.UInt.Lemmas
 
 namespace Char

src/Init/Data/Fin/Basic.lean

@@ -8,8 +8,6 @@ module
 prelude
 import Init.Data.Nat.Bitwise.Basic
 
-@[expose] section
-
 open Nat
 
 namespace Fin
@@ -46,7 +44,7 @@ Returns `a` modulo `n` as a `Fin n`.
 
 The assumption `NeZero n` ensures that `Fin n` is nonempty.
 -/
-@[expose] protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
+protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
 
 /--

src/Init/Data/Fin/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro, Leonardo de Moura
 module
 
 prelude
+import Init.Data.Fin.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Int.DivMod.Lemmas
 import Init.Ext

src/Init/Data/Float.lean

@@ -161,7 +161,8 @@ This function does not reduce in the kernel. It is compiled to the C inequality
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
-attribute [instance] Float.decLt Float.decLe
+instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
+instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
 
 /--
 Converts a floating-point number to a string.

src/Init/Data/Float32.lean

@@ -145,7 +145,7 @@ Compares two floating point numbers for strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLt", instance] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
+@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLt a b
 
@@ -154,10 +154,13 @@ Compares two floating point numbers for non-strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLe", instance] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
+@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLe a b
 
+instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
+instance float32DecLe (a b : Float32) : Decidable (a ≤ b) := Float32.decLe a b
+
 /--
 Converts a floating-point number to a string.
 

src/Init/Data/Function.lean

@@ -18,7 +18,7 @@ Examples:
  * `Function.curry (fun (x, y) => x + y) 3 5 = 8`
  * `Function.curry Prod.swap 3 "five" = ("five", 3)`
 -/
-@[inline, expose]
+@[inline]
 def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
 
 /--
@@ -28,7 +28,7 @@ Examples:
  * `Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]`
  * `[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]`
 -/
-@[inline, expose]
+@[inline]
 def uncurry : (α → β → φ) → α × β → φ := fun f a => f a.1 a.2
 
 @[simp]

src/Init/Data/Hashable.lean

@@ -57,6 +57,9 @@ instance : Hashable UInt64 where
 instance : Hashable USize where
   hash n := n.toUInt64
 
+instance : Hashable ByteArray where
+  hash as := as.foldl (fun r a => mixHash r (hash a)) 7
+
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64
 

src/Init/Data/Int/Basic.lean

@@ -11,8 +11,6 @@ prelude
 import Init.Data.Cast
 import Init.Data.Nat.Div.Basic
 
-@[expose] section
-
 set_option linter.missingDocs true -- keep it documented
 open Nat
 

src/Init/Data/Int/Bitwise/Lemmas.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.Nat.Bitwise.Lemmas
-import all Init.Data.Int.Bitwise.Basic
+import Init.Data.Int.Bitwise.Basic
 import Init.Data.Int.DivMod.Lemmas
 
 namespace Int

src/Init/Data/Int/Compare.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert
 module
 
 prelude
-import all Init.Data.Ord
+import Init.Data.Ord
 import Init.Data.Int.Order
 
 /-! # Basic lemmas about comparing integers

src/Init/Data/Int/DivMod/Basic.lean

@@ -8,8 +8,6 @@ module
 prelude
 import Init.Data.Int.Basic
 
-@[expose] section
-
 open Nat
 
 namespace Int

src/Init/Data/Int/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module
 
 prelude
+import Init.Data.Int.Basic
 import Init.Conv
 import Init.NotationExtra
 import Init.PropLemmas

src/Init/Data/Int/LemmasAux.lean

@@ -121,7 +121,7 @@ theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m :=
 /-! ### min and max -/
 
 @[simp] protected theorem min_assoc : ∀ (a b c : Int), min (min a b) c = min a (min b c) := by omega
-instance : Std.Associative (α := Int) min := ⟨Int.min_assoc⟩
+instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 
 @[simp] protected theorem min_self_assoc {m n : Int} : min m (min m n) = min m n := by
   rw [← Int.min_assoc, Int.min_self]
@@ -130,7 +130,7 @@ instance : Std.Associative (α := Int) min := ⟨Int.min_assoc⟩
   rw [Int.min_comm m n, ← Int.min_assoc, Int.min_self]
 
 @[simp] protected theorem max_assoc (a b c : Int) : max (max a b) c = max a (max b c) := by omega
-instance : Std.Associative (α := Int) max := ⟨Int.max_assoc⟩
+instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
 @[simp] protected theorem max_self_assoc {m n : Int} : max m (max m n) = max m n := by
   rw [← Int.max_assoc, Int.max_self]

src/Init/Data/Int/Linear.lean

@@ -12,9 +12,9 @@ import Init.Data.Int.Lemmas
 import Init.Data.Int.LemmasAux
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.Cooper
-import all Init.Data.Int.Gcd
+import Init.Data.Int.Gcd
 import Init.Data.RArray
-import all Init.Data.AC
+import Init.Data.AC
 
 namespace Int.Linear
 

src/Init/Data/List/Attach.lean

@@ -6,7 +6,6 @@ Authors: Mario Carneiro
 module
 
 prelude
-import all Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
 import Init.Data.List.Count
 import Init.Data.Subtype
 import Init.BinderNameHint
@@ -243,8 +242,9 @@ theorem getElem?_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} (h
   | nil => simp
   | cons hd tl hl =>
     rcases i with ⟨i⟩
-    · simp
-    · simp only [pmap, getElem?_cons_succ, hl]
+    · simp only [Option.pmap]
+      split <;> simp_all
+    · simp only [pmap, getElem?_cons_succ, hl, Option.pmap]
 
 set_option linter.deprecated false in
 @[deprecated List.getElem?_pmap (since := "2025-02-12")]

src/Init/Data/List/Basic.lean

@@ -10,8 +10,6 @@ import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.List.Notation
 
-@[expose] section
-
 /-!
 # Basic operations on `List`.
 

src/Init/Data/List/Control.lean

@@ -9,6 +9,7 @@ prelude
 import Init.Control.Basic
 import Init.Control.Id
 import Init.Control.Lawful
+import Init.Data.List.Basic
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -340,9 +341,9 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
 theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
     findM? (m := m) (pure <| p ·) as = pure (as.find? p) := by
   induction as with
-  | nil => simp [findM?, find?_nil]
+  | nil => rfl
   | cons a as ih =>
-    simp only [findM?, find?_cons]
+    simp only [findM?, find?]
     cases p a with
     | true  => simp
     | false => simp [ih]

src/Init/Data/List/FinRange.lean

@@ -29,7 +29,7 @@ def finRange (n : Nat) : List (Fin n) := ofFn fun i => i
     (finRange n)[i] = Fin.cast length_finRange ⟨i, h⟩ := by
   simp [List.finRange]
 
-@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange]
+@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn]
 
 theorem finRange_succ {n} : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
   apply List.ext_getElem; simp; intro i; cases i <;> simp

src/Init/Data/List/Find.lean

@@ -11,7 +11,6 @@ import Init.Data.List.Lemmas
 import Init.Data.List.Sublist
 import Init.Data.List.Range
 import Init.Data.List.Impl
-import all Init.Data.List.Attach
 import Init.Data.Fin.Lemmas
 
 /-!
@@ -95,7 +94,7 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
   induction l with
   | nil => simp
   | cons x xs ih =>
-    simp [findSome?, find?]
+    simp [guard, findSome?, find?]
     split <;> rename_i h
     · simp only [Option.guard_eq_some_iff] at h
       obtain ⟨rfl, h⟩ := h
@@ -1003,8 +1002,9 @@ theorem isNone_findFinIdx? {l : List α} {p : α → Bool} :
 @[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
+  unfold unattach
   induction l with
-  | nil => simp [unattach]
+  | nil => simp
   | cons a l ih =>
     simp [hf, findFinIdx?_cons]
     split <;> simp [ih, Function.comp_def]

src/Init/Data/List/Lemmas.lean

@@ -9,8 +9,8 @@ module
 prelude
 import Init.Data.Bool
 import Init.Data.Option.Lemmas
-import all Init.Data.List.BasicAux
-import all Init.Data.List.Control
+import Init.Data.List.BasicAux
+import Init.Data.List.Control
 import Init.Control.Lawful.Basic
 import Init.BinderPredicates
 
@@ -1745,7 +1745,7 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
   rw [head_append, dif_pos (by simp_all)]
 
 @[simp, grind] theorem head?_append {l : List α} : (l ++ l').head? = l.head?.or l'.head? := by
-  cases l <;> simp
+  cases l <;> rfl
 
 -- Note:
 -- `getLast_append_of_ne_nil`, `getLast_append` and `getLast?_append`
@@ -2052,7 +2052,7 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
 
 /-! ### flatMap -/
 
-theorem flatMap_def {l : List α} {f : α → List β} : l.flatMap f = flatten (map f l) := rfl
+theorem flatMap_def {l : List α} {f : α → List β} : l.flatMap f = flatten (map f l) := by rfl
 
 @[simp] theorem flatMap_id {L : List (List α)} : L.flatMap id = L.flatten := by simp [flatMap_def]
 
@@ -3054,7 +3054,7 @@ theorem head?_dropLast {xs : List α} : xs.dropLast.head? = if 1 < xs.length the
 
 theorem getLast_dropLast {xs : List α} (h) :
    xs.dropLast.getLast h =
-     xs[xs.length - 2]'(by match xs, h with | (_ :: _ :: _), _ => exact Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _)) := by
+     xs[xs.length - 2]'(match xs, h with | (_ :: _ :: _), _ => Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _)) := by
   rw [getLast_eq_getElem, getElem_dropLast]
   congr 1
   simp; rfl

src/Init/Data/List/Monadic.lean

@@ -8,7 +8,6 @@ module
 prelude
 import Init.Data.List.TakeDrop
 import Init.Data.List.Attach
-import all Init.Data.List.Control
 
 /-!
 # Lemmas about `List.mapM` and `List.forM`.
@@ -438,6 +437,7 @@ and simplifies these to the function directly taking the value.
     {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
     (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
     l.foldlM f x = l.unattach.foldlM g x := by
+  unfold unattach
   induction l generalizing x with
   | nil => simp
   | cons a l ih => simp [ih, hf]
@@ -460,6 +460,7 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
     (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
     l.foldrM f x = l.unattach.foldrM g x := by
+  unfold unattach
   induction l generalizing x with
   | nil => simp
   | cons a l ih =>
@@ -485,6 +486,7 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem mapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m β} {g : α → m β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.mapM f = l.unattach.mapM g := by
+  unfold unattach
   simp [← List.mapM'_eq_mapM]
   induction l with
   | nil => simp
@@ -502,6 +504,7 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m (Option β)} {g : α → m (Option β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.filterMapM f = l.unattach.filterMapM g := by
+  unfold unattach
   induction l with
   | nil => simp
   | cons a l ih => simp [ih, hf, filterMapM_cons]
@@ -520,9 +523,10 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m (List β)} {g : α → m (List β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (l.flatMapM f) = l.unattach.flatMapM g := by
+  unfold unattach
   induction l with
-  | nil => simp [flatMapM_nil]
-  | cons a l ih => simp only [flatMapM_cons, hf, ih, bind_pure_comp, unattach_cons]
+  | nil => simp
+  | cons a l ih => simp [ih, hf]
 
 @[wf_preprocess] theorem flatMapM_wfParam [Monad m] [LawfulMonad m]
     {xs : List α} {f : α → m (List β)} :

src/Init/Data/List/Nat/Modify.lean

@@ -148,7 +148,7 @@ theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (i : Nat) (
     (a :: l).modify 0 f = f a :: l := rfl
 
 @[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (i) :
-    (a :: l).modify (i + 1) f = a :: l.modify i f := rfl
+    (a :: l).modify (i + 1) f = a :: l.modify i f := by rfl
 
 theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
     l.modifyHead f = l.modify 0 f := by cases l <;> simp

src/Init/Data/List/Pairwise.lean

@@ -254,7 +254,7 @@ theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h
   | nil => simp
   | cons a l ihl =>
     obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h
-    simp only [pmap_cons, pairwise_cons, mem_pmap, forall_exists_index, ihl hl, and_congr_left_iff]
+    simp only [ihl hl, pairwise_cons, exists₂_imp, pmap, and_congr_left_iff, mem_pmap]
     refine fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, ?_⟩
     rintro H _ b hb rfl
     exact H b hb _ _

src/Init/Data/List/Perm.lean

@@ -9,7 +9,6 @@ prelude
 import Init.Data.List.Pairwise
 import Init.Data.List.Erase
 import Init.Data.List.Find
-import all Init.Data.List.Attach
 
 /-!
 # List Permutations

src/Init/Data/List/Sort/Impl.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.List.Sort.Basic
 import Init.Data.List.Sort.Lemmas
 
 /-!

src/Init/Data/List/Sort/Lemmas.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.List.Perm
-import all Init.Data.List.Sort.Basic
+import Init.Data.List.Sort.Basic
 import Init.Data.List.Nat.Range
 import Init.Data.Bool
 

src/Init/Data/List/TakeDrop.lean

@@ -6,7 +6,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module
 
 prelude
-import all Init.Data.List.Basic
 import Init.Data.List.Lemmas
 
 /-!
@@ -242,7 +241,7 @@ theorem dropLast_eq_take {l : List α} : l.dropLast = l.take (l.length - 1) := b
     ∀ {l : List α} {i : Nat}, (l.take i).map f = (l.map f).take i
   | [], i => by simp
   | _, 0 => by simp
-  | _ :: tl, n + 1 => by simp [map_take]
+  | _ :: tl, n + 1 => by dsimp; rw [map_take]
 
 @[simp] theorem map_drop {f : α → β} :
     ∀ {l : List α} {i : Nat}, (l.drop i).map f = (l.map f).drop i

src/Init/Data/List/ToArray.lean

@@ -6,14 +6,11 @@ Authors: Mario Carneiro
 module
 
 prelude
-import all Init.Data.List.Control
 import Init.Data.List.Impl
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
 import Init.Data.List.Nat.InsertIdx
 import Init.Data.Array.Lex.Basic
-import all Init.Data.Array.Basic
-import all Init.Data.Array.Set
 
 /-! ### Lemmas about `List.toArray`.
 

src/Init/Data/Nat/Basic.lean

@@ -57,7 +57,7 @@ Examples:
 * `Nat.repeat f 3 a = f <| f <| f <| a`
 * `Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"`
 -/
-@[specialize, expose] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α
+@[specialize] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α
   | 0,      a => a
   | succ n, a => f (repeat f n a)
 
@@ -89,7 +89,7 @@ Examples:
  * `Nat.blt 5 2 = false`
  * `Nat.blt 5 5 = false`
 -/
-@[expose] def blt (a b : Nat) : Bool :=
+def blt (a b : Nat) : Bool :=
   ble a.succ b
 
 attribute [simp] Nat.zero_le

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -9,7 +9,7 @@ module
 prelude
 import Init.Data.Bool
 import Init.Data.Int.Pow
-import all Init.Data.Nat.Bitwise.Basic
+import Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Simproc
 import Init.TacticsExtra

src/Init/Data/Nat/Compare.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 module
 
 prelude
-import all Init.Data.Ord
+import Init.Data.Ord
 
 /-! # Basic lemmas about comparing natural numbers
 

src/Init/Data/Nat/Div/Basic.lean

@@ -10,8 +10,6 @@ import Init.WF
 import Init.WFTactics
 import Init.Data.Nat.Basic
 
-@[expose] section
-
 namespace Nat
 
 /--

src/Init/Data/Nat/Lemmas.lean

@@ -6,9 +6,8 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Floris van Doorn
 module
 
 prelude
-import all Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.MinMax
-import all Init.Data.Nat.Log2
+import Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
 import Init.Data.Nat.Mod
 

src/Init/Data/Nat/Linear.lean

@@ -10,8 +10,6 @@ import Init.ByCases
 import Init.Data.Prod
 import Init.Data.RArray
 
-@[expose] section
-
 namespace Nat.Linear
 
 /-!
@@ -257,8 +255,15 @@ theorem Poly.denote_cons (ctx : Context) (k : Nat) (v : Var) (p : Poly) : denote
 
 attribute [local simp] Poly.denote_cons
 
+theorem Poly.denote_reverseAux (ctx : Context) (p q : Poly) : denote ctx (List.reverseAux p q) = denote ctx (p ++ q) := by
+  match p with
+  | [] => simp [List.reverseAux]
+  | (k, v) :: p => simp [List.reverseAux, denote_reverseAux]
+
+attribute [local simp] Poly.denote_reverseAux
+
 theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.reverse p) = denote ctx p := by
-  induction p <;> simp [*]
+  simp [List.reverse]
 
 attribute [local simp] Poly.denote_reverse
 

src/Init/Data/Option/Array.lean

@@ -8,37 +8,9 @@ module
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Option.List
-import all Init.Data.Option.Instances
 
 namespace Option
 
-@[simp, grind] theorem mem_toArray {a : α} {o : Option α} : a ∈ o.toArray ↔ o = some a := by
-  cases o <;> simp [eq_comm]
-
-@[simp, grind] theorem forIn'_toArray [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toArray → β → m (ForInStep β)) :
-    forIn' o.toArray b f = forIn' o b fun a m b => f a (by simpa using m) b := by
-  cases o <;> simp <;> rfl
-
-@[simp, grind] theorem forIn_toArray [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn o.toArray b f = forIn o b f := by
-  cases o <;> simp <;> rfl
-
-@[simp, grind] theorem foldlM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : α → β → m α) :
-    o.toArray.foldlM f a = o.elim (pure a) (fun b => f a b) := by
-  cases o <;> simp
-
-@[simp, grind] theorem foldrM_toArray [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
-    o.toArray.foldrM f a = o.elim (pure a) (fun b => f b a) := by
-  cases o <;> simp
-
-@[simp, grind] theorem foldl_toArray (o : Option β) (a : α) (f : α → β → α) :
-    o.toArray.foldl f a = o.elim a (fun b => f a b) := by
-  cases o <;> simp
-
-@[simp, grind] theorem foldr_toArray (o : Option β) (a : α) (f : β → α → α) :
-    o.toArray.foldr f a = o.elim a (fun b => f b a) := by
-  cases o <;> simp
-
 @[simp]
 theorem toList_toArray {o : Option α} : o.toArray.toList = o.toList := by
   cases o <;> simp
@@ -51,47 +23,4 @@ theorem toArray_filter {o : Option α} {p : α → Bool} :
     (o.filter p).toArray = o.toArray.filter p := by
   rw [← toArray_toList, toList_filter, ← List.filter_toArray, toArray_toList]
 
-theorem toArray_bind {o : Option α} {f : α → Option β} :
-    (o.bind f).toArray = o.toArray.flatMap (Option.toArray ∘ f) := by
-  cases o <;> simp
-
-theorem toArray_join {o : Option (Option α)} : o.join.toArray = o.toArray.flatMap Option.toArray := by
-  simp [toArray_bind, ← bind_id_eq_join]
-
-theorem toArray_map {o : Option α} {f : α → β} : (o.map f).toArray = o.toArray.map f := by
-  cases o <;> simp
-
-theorem toArray_min [Min α] {o o' : Option α} :
-    (min o o').toArray = o.toArray.zipWith min o'.toArray := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem size_toArray_le {o : Option α} : o.toArray.size ≤ 1 := by
-  cases o <;> simp
-
-theorem size_toArray_eq_ite {o : Option α} :
-    o.toArray.size = if o.isSome then 1 else 0 := by
-  cases o <;> simp
-
-@[simp]
-theorem toArray_eq_empty_iff {o : Option α} : o.toArray = #[] ↔ o = none := by
-  cases o <;> simp
-
-@[simp]
-theorem toArray_eq_singleton_iff {o : Option α} : o.toArray = #[a] ↔ o = some a := by
-  cases o <;> simp
-
-@[simp]
-theorem size_toArray_eq_zero_iff {o : Option α} :
-    o.toArray.size = 0 ↔ o = none := by
-  cases o <;> simp
-
-@[simp]
-theorem size_toArray_eq_one_iff {o : Option α} :
-    o.toArray.size = 1 ↔ o.isSome := by
-  cases o <;> simp
-
-theorem size_toArray_choice_eq_one [Nonempty α] : (choice α).toArray.size = 1 := by
-  simp
-
 end Option

src/Init/Data/Option/Attach.lean

@@ -8,16 +8,11 @@ module
 prelude
 import Init.Data.Option.Basic
 import Init.Data.Option.List
-import Init.Data.Option.Array
-import Init.Data.Array.Attach
 import Init.Data.List.Attach
 import Init.BinderPredicates
 
 namespace Option
 
-instance {o : Option α} : Subsingleton { x // o = some x } where
-  allEq a b := Subtype.ext (Option.some.inj (a.property.symm.trans b.property))
-
 /--
 Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
 `Option {x // P x}` is the same as the input `Option α`.
@@ -91,7 +86,7 @@ theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a,
     (o.attachWith p H).map Subtype.val = o :=
   (attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
 
-theorem attach_eq_some : ∀ (o : Option α) (x : {x // o = some x}), o.attach = some x
+theorem attach_eq_some : ∀ (o : Option a) (x : {x // o = some x}), o.attach = some x
   | none, ⟨x, h⟩ => by simp at h
   | some a, ⟨x, h⟩ => by simpa using h
 
@@ -128,45 +123,24 @@ theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach
   cases o <;> cases x <;> simp
 
 @[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
-    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ :=
-  Subsingleton.elim _ _
-
-@[simp] theorem getD_attach {o : Option α} {fallback} :
-    o.attach.getD fallback = fallback :=
-  Subsingleton.elim _ _
-
-@[simp] theorem get!_attach {o : Option α} [Inhabited { x // o = some x }] :
-    o.attach.get! = default :=
-  Subsingleton.elim _ _
+    o.attach.get h = ⟨o.get (by simpa using h), by simp⟩ := by
+  cases o
+  · simp at h
+  · simp [get_some]
 
 @[simp] theorem get_attachWith {p : α → Prop} {o : Option α} (H : ∀ a, o = some a → p a) (h : (o.attachWith p H).isSome) :
     (o.attachWith p H).get h = ⟨o.get (by simpa using h), H _ (by simp)⟩ := by
-  cases o <;> simp
-
-@[simp] theorem getD_attachWith {p : α → Prop} {o : Option α} {h} {fallback} :
-    (o.attachWith p h).getD fallback =
-      ⟨o.getD fallback.1, by cases o <;> (try exact fallback.2) <;> exact h _ (by simp)⟩ := by
-  cases o <;> simp
+  cases o
+  · simp at h
+  · simp [get_some]
 
 theorem toList_attach (o : Option α) :
-    o.attach.toList = o.toList.attach.map fun x => ⟨x.1, by simpa using x.2⟩ := by
-  cases o <;> simp
-
-theorem toList_attachWith {p : α → Prop} {o : Option α} {h} :
-    (o.attachWith p h).toList = o.toList.attach.map fun x => ⟨x.1, h _ (by simpa using x.2)⟩ := by
-  cases o <;> simp
-
-theorem toArray_attach (o : Option α) :
-    o.attach.toArray = o.toArray.attach.map fun x => ⟨x.1, by simpa using x.2⟩ := by
-  cases o <;> simp
-
-theorem toArray_attachWith {p : α → Prop} {o : Option α} {h} :
-    (o.attachWith p h).toArray = o.toArray.attach.map fun x => ⟨x.1, h _ (by simpa using x.2)⟩ := by
+    o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases o <;> simp
 
 @[simp, grind =] theorem attach_toList (o : Option α) :
     o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by
-  cases o <;> simp [toList]
+  cases o <;> simp
 
 theorem attach_map {o : Option α} (f : α → β) :
     (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some_iff.2 ⟨_, h, rfl⟩⟩) := by
@@ -219,7 +193,7 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
   cases o with
   | none => simp
   | some a =>
-    simp only [Option.filter, attach_some]
+    simp only [filter_some, attach_some]
     ext
     simp only [attach_eq_some_iff, ite_none_right_eq_some, some.injEq, bind_some,
       dite_none_right_eq_some]
@@ -229,11 +203,6 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
     · rintro ⟨h, rfl⟩
       simp [h]
 
-theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
-    (o.attachWith P h).filter q =
-      (o.filter q).attachWith P (fun _ h' => h _ (eq_some_of_filter_eq_some h')) := by
-  cases o <;> simp [filter_some] <;> split <;> simp
-
 theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
     o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
   cases o <;> simp [filter_some]
@@ -242,64 +211,6 @@ theorem toList_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
     (o.pbind f).toList = o.attach.toList.flatMap (fun ⟨x, h⟩ => (f x h).toList) := by
   cases o <;> simp
 
-theorem toArray_pbind {o : Option α} {f : (a : α) → o = some a → Option β} :
-    (o.pbind f).toArray = o.attach.toArray.flatMap (fun ⟨x, h⟩ => (f x h).toArray) := by
-  cases o <;> simp
-
-theorem toList_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
-    (o.pfilter p).toList = (o.toList.attach.filter (fun x => p x.1 (by simpa using x.2))).unattach := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [pfilter_some, toList_some, List.attach_cons, List.attach_nil, List.map_nil]
-    split <;> rename_i h
-    · rw [List.filter_cons_of_pos h]; simp
-    · rw [List.filter_cons_of_neg h]; simp
-
-theorem toArray_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
-    (o.pfilter p).toArray = (o.toArray.attach.filter (fun x => p x.1 (by simpa using x.2))).unattach := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [pfilter_some, toArray_some, List.attach_toArray, List.attachWith_mem_toArray,
-      List.attach_cons, List.attach_nil, List.map_nil, List.map_cons, List.size_toArray,
-      List.length_cons, List.length_nil, Nat.zero_add, List.filter_toArray', List.unattach_toArray]
-    split <;> rename_i h
-    · rw [List.filter_cons_of_pos h]; simp
-    · rw [List.filter_cons_of_neg h]; simp
-
-theorem toList_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a → β}
-    (h : ∀ a, o = some a → p a) :
-    (o.pmap f h).toList = o.attach.toList.map (fun x => f x.1 (h _ x.2)) := by
-  cases o <;> simp
-
-theorem toArray_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a → β}
-    (h : ∀ a, o = some a → p a) :
-    (o.pmap f h).toArray = o.attach.toArray.map (fun x => f x.1 (h _ x.2)) := by
-  cases o <;> simp
-
-theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
-    (o.pfilter p).attach =
-      o.attach.pbind fun x h => if h' : p x (by simp_all) then
-        some ⟨x.1, by simpa [pfilter_eq_some_iff] using ⟨_, h'⟩⟩ else none := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [attach_some, eq_mp_eq_cast, id_eq, pbind_some]
-    rw [attach_congr pfilter_some]
-    split <;> simp [*]
-
-theorem attach_guard {p : α → Bool} {x : α} :
-    (guard p x).attach = if h : p x then some ⟨x, by simp_all⟩ else none := by
-  simp only [guard_eq_ite]
-  split <;> simp [*]
-
-theorem attachWith_guard {q : α → Bool} {x : α} {P : α → Prop}
-    {h : ∀ a, guard q x = some a → P a} :
-    (guard q x).attachWith P h = if h' : q x then some ⟨x, h _ (by simp_all)⟩ else none := by
-  simp only [guard_eq_ite]
-  split <;> simp [*]
-
 /-! ## unattach
 
 `Option.unattach` is the (one-sided) inverse of `Option.attach`. It is a synonym for `Option.map Subtype.val`.
@@ -344,29 +255,6 @@ def unattach {α : Type _} {p : α → Prop} (o : Option { x // p x }) := o.map
     (o.attachWith p H).unattach = o := by
   cases o <;> simp
 
-theorem unattach_eq_some_iff {p : α → Prop} {o : Option { x // p x }} {x : α} :
-    o.unattach = some x ↔ ∃ h, o = some ⟨x, h⟩ :=
-  match o with
-  | none => by simp
-  | some ⟨y, h⟩ => by simpa using fun h' => h' ▸ h
-
-@[simp]
-theorem unattach_eq_none_iff {p : α → Prop} {o : Option { x // p x }} :
-    o.unattach = none ↔ o = none := by
-  cases o <;> simp
-
-theorem get_unattach {p : α → Prop} {o : Option { x // p x }} {h} :
-    o.unattach.get h = (o.get (by simpa using h)).1 := by
-  cases o <;> simp
-
-theorem toList_unattach {p : α → Prop} {o : Option { x // p x }} :
-    o.unattach.toList = o.toList.unattach := by
-  cases o <;> simp
-
-theorem toArray_unattach {p : α → Prop} {o : Option { x // p x }} :
-    o.unattach.toArray = o.toArray.unattach := by
-  cases o <;> simp
-
 /-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
 
 /--
@@ -391,51 +279,4 @@ and simplifies these to the function directly taking the value.
   · simp only [filter_some, hf, unattach_some]
     split <;> simp
 
-@[simp] theorem unattach_guard {p : α → Prop} {q : { x // p x } → Bool} {r : α → Bool}
-    (hq : ∀ x h, q ⟨x, h⟩ = r x) {x : { x // p x }} :
-    (guard q x).unattach = guard r x.1 := by
-  simp only [guard]
-  split <;> simp_all
-
-@[simp] theorem unattach_pfilter {p : α → Prop} {o : Option { x // p x }}
-    {f : (a : { x // p x }) → o = some a → Bool}
-    {g : (a : α) → o.unattach = some a → Bool} (hf : ∀ x h h', f ⟨x, h⟩ h' = g x (by simp_all)) :
-    (o.pfilter f).unattach = o.unattach.pfilter g := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [hf, pfilter_some, unattach_some]
-    split <;> simp
-
-@[simp] theorem unattach_merge {p : α → Prop} {f : { x // p x } → { x // p x } → { x // p x }}
-    {g : α → α → α} (hf : ∀ x h y h', (f ⟨x, h⟩ ⟨y, h'⟩).1 = g x y) {o o' : Option { x // p x }} :
-    (o.merge f o').unattach = o.unattach.merge g o'.unattach := by
-  cases o <;> cases o' <;> simp [*]
-
-theorem any_attach {p : α → Bool} {o : Option α} {q : { x // o = some x } → Bool}
-    (h : ∀ x h, q ⟨x, h⟩ = p x) : o.attach.any q = o.any p := by
-  cases o <;> simp [*]
-
-theorem any_attachWith {p : α → Bool} {o : Option α} {r : α → Prop} (hr : ∀ x, o = some x → r x)
-    {q : { x // r x } → Bool}
-    (h : ∀ x h, q ⟨x, h⟩ = p x) : (o.attachWith r hr).any q = o.any p := by
-  cases o <;> simp [*]
-
-theorem any_unattach {p : α → Prop} {o : Option { x // p x }} {q : α → Bool} :
-    o.unattach.any q = o.any (q ∘ Subtype.val) := by
-  cases o <;> simp
-
-theorem all_attach {p : α → Bool} {o : Option α} {q : { x // o = some x } → Bool}
-    (h : ∀ x h, q ⟨x, h⟩ = p x) : o.attach.all q = o.all p := by
-  cases o <;> simp [*]
-
-theorem all_attachWith {p : α → Bool} {o : Option α} {r : α → Prop} (hr : ∀ x, o = some x → r x)
-    {q : { x // r x } → Bool}
-    (h : ∀ x h, q ⟨x, h⟩ = p x) : (o.attachWith r hr).all q = o.all p := by
-  cases o <;> simp [*]
-
-theorem all_unattach {p : α → Prop} {o : Option { x // p x }} {q : α → Bool} :
-    o.unattach.all q = o.all (q ∘ Subtype.val) := by
-  cases o <;> simp
-
 end Option

src/Init/Data/Option/Basic.lean

@@ -8,8 +8,6 @@ module
 prelude
 import Init.Control.Basic
 
-@[expose] section
-
 namespace Option
 
 deriving instance DecidableEq for Option
@@ -102,9 +100,11 @@ From the perspective of `Option` as a collection with at most one element, the m
 is applied to the element if present, and the final result is empty if either the initial or the
 resulting collections are empty.
 -/
-@[inline] protected def bindM [Pure m] (f : α → m (Option β)) : Option α → m (Option β)
-  | none => pure none
-  | some a => f a
+@[inline] protected def bindM [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β) := do
+  if let some a := o then
+    return (← f a)
+  else
+    return none
 
 /--
 Applies a function in some applicative functor to an optional value, returning `none` with no

src/Init/Data/Option/Lemmas.lean

@@ -6,16 +6,14 @@ Authors: Mario Carneiro
 module
 
 prelude
-import all Init.Data.Option.BasicAux
-import all Init.Data.Option.Instances
+import Init.Data.Option.BasicAux
+import Init.Data.Option.Instances
 import Init.Data.BEq
 import Init.Classical
 import Init.Ext
 
 namespace Option
 
-theorem default_eq_none : (default : Option α) = none := rfl
-
 @[deprecated mem_def (since := "2025-04-07")]
 theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl
 
@@ -151,22 +149,6 @@ theorem not_isSome_iff_eq_none : ¬o.isSome ↔ o = none := by
 
 theorem ne_none_iff_isSome : o ≠ none ↔ o.isSome := by cases o <;> simp
 
-@[simp]
-theorem any_true {o : Option α} : o.any (fun _ => true) = o.isSome := by
-  cases o <;> simp
-
-@[simp]
-theorem any_false {o : Option α} : o.any (fun _ => false) = false := by
-  cases o <;> simp
-
-@[simp]
-theorem all_true {o : Option α} : o.all (fun _ => true) = true := by
-  cases o <;> simp
-
-@[simp]
-theorem all_false {o : Option α} : o.all (fun _ => false) = o.isNone := by
-  cases o <;> simp
-
 theorem ne_none_iff_exists : o ≠ none ↔ ∃ x, some x = o := by cases o <;> simp
 
 theorem ne_none_iff_exists' : o ≠ none ↔ ∃ x, o = some x :=
@@ -194,6 +176,8 @@ abbrev ball_ne_none := @forall_ne_none
 
 @[simp, grind] theorem bind_eq_bind : bind = @Option.bind α β := rfl
 
+@[simp, grind] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
+
 @[simp, grind] theorem bind_fun_some (x : Option α) : x.bind some = x := by cases x <;> rfl
 
 @[simp] theorem bind_fun_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
@@ -254,18 +238,10 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α →
       (isSome_apply_of_isSome_bind h) := by
   cases x <;> trivial
 
-theorem any_bind {p : β → Bool} {f : α → Option β} {o : Option α} :
-    (o.bind f).any p = o.any (Option.any p ∘ f) := by
-  cases o <;> simp
-
-theorem all_bind {p : β → Bool} {f : α → Option β} {o : Option α} :
-    (o.bind f).all p = o.all (Option.all p ∘ f) := by
-  cases o <;> simp
-
-@[grind] theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
+theorem join_eq_bind_id {x : Option (Option α)} : x.join = x.bind id := rfl
 
 theorem join_eq_some_iff : x.join = some a ↔ x = some (some a) := by
-  simp [← bind_id_eq_join, bind_eq_some_iff]
+  simp [join_eq_bind_id, bind_eq_some_iff]
 
 @[deprecated join_eq_some_iff (since := "2025-04-10")]
 abbrev join_eq_some := @join_eq_some_iff
@@ -277,14 +253,12 @@ theorem join_ne_none' : ¬x.join = none ↔ ∃ z, x = some (some z) :=
   join_ne_none
 
 theorem join_eq_none_iff : o.join = none ↔ o = none ∨ o = some none :=
-  match o with | none | some none | some (some _) => by simp [bind_id_eq_join]
+  match o with | none | some none | some (some _) => by simp [join_eq_bind_id]
 
 @[deprecated join_eq_none_iff (since := "2025-04-10")]
 abbrev join_eq_none := @join_eq_none_iff
 
-theorem bind_join {f : α → Option β} {o : Option (Option α)} :
-    o.join.bind f = o.bind (·.bind f) := by
-  cases o <;> simp
+@[grind] theorem bind_id_eq_join {x : Option (Option α)} : x.bind id = x.join := rfl
 
 @[simp, grind] theorem map_eq_map : Functor.map f = Option.map f := rfl
 
@@ -421,15 +395,9 @@ theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
     a ∈ o.filter p ↔ a ∈ o ∧ p a := by
   simp
 
-@[grind]
-theorem bind_guard (x : Option α) (p : α → Bool) :
-    x.bind (Option.guard p) = x.filter p := by
-  cases x <;> rfl
-
-@[deprecated bind_guard (since := "2025-05-15")]
 theorem filter_eq_bind (x : Option α) (p : α → Bool) :
-    x.filter p = x.bind (Option.guard p) :=
-  (bind_guard x p).symm
+    x.filter p = x.bind (Option.guard p) := by
+  cases x <;> rfl
 
 @[simp] theorem any_filter : (o : Option α) →
     (Option.filter p o).any q = Option.any (fun a => p a && q a) o
@@ -531,10 +499,6 @@ theorem any_eq_false_iff_get (p : α → Bool) (x : Option α) :
 theorem isSome_of_any {x : Option α} {p : α → Bool} (h : x.any p) : x.isSome := by
   cases x <;> trivial
 
-theorem get_of_any_eq_true (p : α → Bool) (x : Option α) (h : x.any p = true) :
-    p (x.get (isSome_of_any h)) :=
-  any_eq_true_iff_get p x |>.1 h |>.2
-
 @[grind]
 theorem any_map {α β : Type _} {x : Option α} {f : α → β} {p : β → Bool} :
     (x.map f).any p = x.any (fun a => p (f a)) := by
@@ -563,39 +527,29 @@ theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
 theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a ∈ x.join) : some a ∈ x :=
   h.symm ▸ join_eq_some_iff.1 h
 
-theorem any_join {p : α → Bool} {x : Option (Option α)} :
-    x.join.any p = x.any (Option.any p) := by
+@[deprecated orElse_some (since := "2025-05-03")]
+theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
+
+@[deprecated orElse_none (since := "2025-05-03")]
+theorem none_orElse (f : Unit → Option α) : none.orElse f = f () := rfl
+
+@[simp] theorem orElse_fun_none (x : Option α) : x.orElse (fun _ => none) = x := by cases x <;> rfl
+
+@[simp] theorem orElse_fun_some (x : Option α) (a : α) :
+    x.orElse (fun _ => some a) = some (x.getD a) := by
   cases x <;> simp
 
-theorem all_join {p : α → Bool} {x : Option (Option α)} :
-    x.join.all p = x.all (Option.all p) := by
+theorem orElse_eq_some_iff (o : Option α) (f) (x : α) :
+    (o.orElse f) = some x ↔ o = some x ∨ o = none ∧ f () = some x := by
+  cases o <;> simp
+
+theorem orElse_eq_none_iff (o : Option α) (f) : (o.orElse f) = none ↔ o = none ∧ f () = none := by
+  cases o <;> simp
+
+@[grind] theorem map_orElse {x : Option α} {y} :
+    (x.orElse y).map f = (x.map f).orElse (fun _ => (y ()).map f) := by
   cases x <;> simp
 
-theorem isNone_join {x : Option (Option α)} : x.join.isNone = x.all Option.isNone := by
-  cases x <;> simp
-
-theorem isSome_join {x : Option (Option α)} : x.join.isSome = x.any Option.isSome := by
-  cases x <;> simp
-
-theorem get_join {x : Option (Option α)} {h} : x.join.get h =
-    (x.get (Option.isSome_of_any (Option.isSome_join ▸ h))).get (get_of_any_eq_true _ _ (Option.isSome_join ▸ h)) := by
-  cases x with
-  | none => simp at h
-  | some _ => simp
-
-theorem join_eq_get {x : Option (Option α)} {h} : x.join = x.get h := by
-  cases x with
-  | none => simp at h
-  | some _ => simp
-
-theorem getD_join {x : Option (Option α)} {default : α} :
-    x.join.getD default = (x.getD (some default)).getD default := by
-  cases x <;> simp
-
-theorem get!_join [Inhabited α] {x : Option (Option α)} :
-    x.join.get! = x.get!.get! := by
-  cases x <;> simp [default_eq_none]
-
 @[simp] theorem guard_eq_some_iff : guard p a = some b ↔ a = b ∧ p a :=
   if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
 
@@ -608,9 +562,6 @@ abbrev guard_eq_some := @guard_eq_some_iff
 @[deprecated isSome_guard (since := "2025-03-18")]
 abbrev guard_isSome := @isSome_guard
 
-@[simp] theorem isNone_guard : (Option.guard p a).isNone = !p a := by
-  rw [← not_isSome, isSome_guard]
-
 @[simp] theorem guard_eq_none_iff : Option.guard p a = none ↔ p a = false :=
   if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
 
@@ -636,27 +587,19 @@ theorem guard_comp {p : α → Bool} {f : β → α} :
   ext1 b
   simp [guard]
 
-theorem get_none (a : α) {h} : none.get h = a := by
-  simp at h
+@[grind] theorem bind_guard (x : Option α) (p : α → Bool) :
+    x.bind (Option.guard p) = x.filter p := by
+  simp only [Option.filter_eq_bind, decide_eq_true_eq]
 
-@[simp]
-theorem get_none_eq_iff_true {h} : (none : Option α).get h = a ↔ True := by
-  simp at h
-
-theorem get_guard : (guard p a).get h = a := by
-  simp only [guard]
-  split <;> simp
-
-@[grind]
-theorem guard_def (p : α → Bool) :
-    Option.guard p = fun x => if p x then some x else none := rfl
-
-@[deprecated guard_def (since := "2025-05-15")]
 theorem guard_eq_map (p : α → Bool) :
     Option.guard p = fun x => Option.map (fun _ => x) (if p x then some x else none) := by
   funext x
   simp [Option.guard]
 
+@[grind]
+theorem guard_def (p : α → Bool) :
+    Option.guard p = fun x => if p x then some x else none := rfl
+
 theorem guard_eq_ite {p : α → Bool} {x : α} :
     Option.guard p x = if p x then some x else none := rfl
 
@@ -668,10 +611,6 @@ theorem guard_eq_filter {p : α → Bool} {x : α} :
   rw [guard_eq_ite]
   split <;> simp_all [filter_some, guard_eq_ite]
 
-theorem map_guard {p : α → Bool} {f : α → β} {x : α} :
-    (Option.guard p x).map f = if p x then some (f x) else none := by
-  simp [guard_eq_ite]
-
 theorem join_filter {p : Option α → Bool} : {o : Option (Option α)} →
     (o.filter p).join = o.join.filter (fun a => p (some a))
   | none => by simp
@@ -741,44 +680,6 @@ instance lawfulIdentity_merge (f : α → α → α) : Std.LawfulIdentity (merge
   left_id a := by cases a <;> simp [merge]
   right_id a := by cases a <;> simp [merge]
 
-theorem merge_join {o o' : Option (Option α)} {f : α → α → α} :
-    o.join.merge f o'.join = (o.merge (Option.merge f) o').join := by
-  cases o <;> cases o' <;> simp
-
-theorem merge_eq_some_iff {o o' : Option α} {f : α → α → α} {a : α} :
-    o.merge f o' = some a ↔ (o = some a ∧ o' = none) ∨ (o = none ∧ o' = some a) ∨
-      (∃ b c, o = some b ∧ o' = some c ∧ f b c = a) := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem merge_eq_none_iff {o o' : Option α} : o.merge f o' = none ↔ o = none ∧ o' = none := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem any_merge {p : α → Bool} {f : α → α → α} (hpf : ∀ a b, p (f a b) = (p a || p b))
-    {o o' : Option α} : (o.merge f o').any p = (o.any p || o'.any p) := by
-  cases o <;> cases o' <;> simp [*]
-
-@[simp]
-theorem all_merge {p : α → Bool} {f : α → α → α} (hpf : ∀ a b, p (f a b) = (p a && p b))
-    {o o' : Option α} : (o.merge f o').all p = (o.all p && o'.all p) := by
-  cases o <;> cases o' <;> simp [*]
-
-@[simp]
-theorem isSome_merge {o o' : Option α} {f : α → α → α} :
-    (o.merge f o').isSome = (o.isSome || o'.isSome) := by
-  simp [← any_true]
-
-@[simp]
-theorem isNone_merge {o o' : Option α} {f : α → α → α} :
-    (o.merge f o').isNone = (o.isNone && o'.isNone) := by
-  simp [← all_false]
-
-@[simp]
-theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.LawfulIdentity f i] {h} :
-    (o.merge f o').get h = f (o.getD i) (o'.getD i) := by
-  cases o <;> cases o' <;> simp [Std.LawfulLeftIdentity.left_id, Std.LawfulRightIdentity.right_id]
-
 @[simp, grind] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
 
 @[simp, grind] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
@@ -792,13 +693,6 @@ theorem elim_filter {o : Option α} {b : β} :
     | false => by simp [filter_some_neg h, h]
     | true => by simp [filter_some_pos, h]
 
-theorem elim_join {o : Option (Option α)} {b : β} {f : α → β} :
-    o.join.elim b f = o.elim b (·.elim b f) := by
-  cases o <;> simp
-
-theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by
-  cases h : p a <;> simp [*, guard]
-
 @[simp, grind] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl
 
@@ -833,29 +727,12 @@ theorem choice_eq_none_iff_not_nonempty : choice α = none ↔ ¬Nonempty α :=
 theorem isSome_choice_iff_nonempty : (choice α).isSome ↔ Nonempty α :=
   ⟨fun h => ⟨(choice α).get h⟩, fun h => by simp only [choice, dif_pos h, isSome_some]⟩
 
-@[simp]
-theorem isSome_choice [Nonempty α] : (choice α).isSome :=
-  isSome_choice_iff_nonempty.2 inferInstance
-
 @[deprecated isSome_choice_iff_nonempty (since := "2025-03-18")]
 abbrev choice_isSome_iff_nonempty := @isSome_choice_iff_nonempty
 
 theorem isNone_choice_iff_not_nonempty : (choice α).isNone ↔ ¬Nonempty α := by
   rw [isNone_iff_eq_none, choice_eq_none_iff_not_nonempty]
 
-@[simp]
-theorem isNone_choice_eq_false [Nonempty α] : (choice α).isNone = false := by
-  simp [← not_isSome]
-
-@[simp]
-theorem getD_choice {a} :
-    (choice α).getD a = (choice α).get (isSome_choice_iff_nonempty.2 ⟨a⟩) := by
-  rw [get_eq_getD]
-
-@[simp]
-theorem get!_choice [Inhabited α] : (choice α).get! = (choice α).get isSome_choice := by
-  rw [get_eq_get!]
-
 end choice
 
 @[simp, grind] theorem toList_some (a : α) : (some a).toList = [a] := rfl
@@ -919,6 +796,9 @@ theorem or_self : or o o = o := by
   cases o <;> rfl
 instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
 
+theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
+  cases o <;> rfl
+
 @[grind _=_] theorem map_or : (or o o').map f = (o.map f).or (o'.map f) := by
   cases o <;> rfl
 
@@ -938,54 +818,10 @@ theorem getD_or {o o' : Option α} {fallback : α} :
     (o.or o').getD fallback = o.getD (o'.getD fallback) := by
   cases o <;> simp
 
-@[simp]
-theorem get!_or {o o' : Option α} [Inhabited α] : (o.or o').get! = o.getD o'.get! := by
-  cases o <;> simp
-
 @[simp] theorem filter_or_filter {o o' : Option α} {f : α → Bool} :
     (o.or (o'.filter f)).filter f = (o.or o').filter f := by
   cases o <;> cases o' <;> simp
 
-theorem guard_or_guard : (guard p a).or (guard q a) = guard (fun x => p x || q x) a := by
-  simp only [guard]
-  split <;> simp_all
-
-/-! ### `orElse` -/
-
-/-- The `simp` normal form of `o <|> o'` is `o.or o'` via `orElse_eq_orElse` and `orElse_eq_or`. -/
-@[simp, grind] theorem orElse_eq_orElse : HOrElse.hOrElse = @Option.orElse α := rfl
-
-theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
-  cases o <;> rfl
-
-/-- The `simp` normal form of `o.orElse f` is o.or (f ())`. -/
-@[simp, grind] theorem orElse_eq_or {o : Option α} {f} : o.orElse f = o.or (f ()) := by
-  simp [or_eq_orElse]
-
-@[deprecated or_some (since := "2025-05-03")]
-theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
-
-@[deprecated or_none (since := "2025-05-03")]
-theorem none_orElse (f : Unit → Option α) : none.orElse f = f () := rfl
-
-@[deprecated or_none (since := "2025-05-13")]
-theorem orElse_fun_none (x : Option α) : x.orElse (fun _ => none) = x := by simp
-
-@[deprecated or_some (since := "2025-05-13")]
-theorem orElse_fun_some (x : Option α) (a : α) :
-    x.orElse (fun _ => some a) = some (x.getD a) := by simp
-
-@[deprecated or_eq_some_iff (since := "2025-05-13")]
-theorem orElse_eq_some_iff (o : Option α) (f) (x : α) :
-    (o.orElse f) = some x ↔ o = some x ∨ o = none ∧ f () = some x := by simp
-
-@[deprecated or_eq_none_iff (since := "2025-05-13")]
-theorem orElse_eq_none_iff (o : Option α) (f) : (o.orElse f) = none ↔ o = none ∧ f () = none := by simp
-
-@[deprecated map_or (since := "2025-05-13")]
-theorem map_orElse {x : Option α} {y} :
-    (x.orElse y).map f = (x.map f).orElse (fun _ => (y ()).map f) := by simp [map_or]
-
 /-! ### beq -/
 
 section beq
@@ -1024,42 +860,6 @@ variable [BEq α]
   · intro h
     infer_instance
 
-@[simp] theorem beq_none {o : Option α} : (o == none) = o.isNone := by cases o <;> simp
-
-@[simp]
-theorem filter_beq_self [ReflBEq α] {p : α → Bool} {o : Option α} : (o.filter p == o) = (o.all p) := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [*]
-
-@[simp]
-theorem self_beq_filter [ReflBEq α] {p : α → Bool} {o : Option α} : (o == o.filter p) = (o.all p) := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [*]
-
-theorem join_beq_some {o : Option (Option α)} {a : α} : (o.join == some a) = (o == some (some a)) := by
-  cases o <;> simp
-
-theorem join_beq_none {o : Option (Option α)} : (o.join == none) = (o == none || o == some none) := by
-  cases o <;> simp
-
-@[simp]
-theorem guard_beq_some [ReflBEq α] {x : α} {p : α → Bool} : (guard p x == some x) = p x := by
-  simp only [guard_eq_ite]
-  split <;> simp [*]
-
-theorem guard_beq_none {x : α} {p : α → Bool} : (guard p x == none) = !p x := by
-  simp
-
-theorem merge_beq_none {o o' : Option α} {f : α → α → α} :
-    (o.merge f o' == none) = (o == none && o' == none) := by
-  simp [beq_none]
-
 end beq
 
 /-! ### ite -/
@@ -1097,9 +897,6 @@ section ite
     some a = (if p then b else none) ↔ p ∧ some a = b := by
   split <;> simp_all
 
-theorem ite_some_none_eq_some {p : Prop} {_ : Decidable p} {a b : α} :
-    (if p then some a else none) = some b ↔ p ∧ a = b := by simp
-
 theorem mem_dite_none_left {x : α} {_ : Decidable p} {l : ¬ p → Option α} :
     (x ∈ if h : p then none else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
   simp
@@ -1191,10 +988,6 @@ theorem isSome_pbind_iff {o : Option α} {f : (a : α) → o = some a → Option
     (o.pbind f).isSome ↔ ∃ a h, (f a h).isSome := by
   cases o <;> simp
 
-theorem isNone_pbind_iff {o : Option α} {f : (a : α) → o = some a → Option β} :
-    (o.pbind f).isNone ↔ o = none ∨ ∃ a h, f a h = none := by
-  cases o <;> simp
-
 @[deprecated "isSome_pbind_iff" (since := "2025-04-01")]
 theorem pbind_isSome {o : Option α} {f : (a : α) → o = some a → Option β} :
     (o.pbind f).isSome = ∃ a h, (f a h).isSome := by
@@ -1204,25 +997,6 @@ theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → o = some a → Optio
     o.pbind f = some b ↔ ∃ a h, f a h = some b := by
   cases o <;> simp
 
-theorem pbind_join {o : Option (Option α)} {f : (a : α) → o.join = some a → Option β} :
-    o.join.pbind f = o.pbind (fun o' ho' => o'.pbind (fun a ha => f a (by simp_all))) := by
-  cases o <;> simp <;> congr
-
-theorem isSome_of_isSome_pbind {o : Option α} {f : (a : α) → o = some a → Option β} :
-    (o.pbind f).isSome → o.isSome := by
-  cases o <;> simp
-
-theorem isSome_get_of_isSome_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
-    (h : (o.pbind f).isSome) : (f (o.get (isSome_of_isSome_pbind h)) (by simp)).isSome := by
-  cases o with
-  | none => simp at h
-  | some a => simp [← h]
-
-@[simp]
-theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h} :
-    (o.pbind f).get h = (f (o.get (isSome_of_isSome_pbind h)) (by simp)).get (isSome_get_of_isSome_pbind h) := by
-  cases o <;> simp
-
 /-! ### pmap -/
 
 @[simp, grind] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
@@ -1273,8 +1047,8 @@ theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) :
 theorem pmap_or {p : α → Prop} {f : ∀ (a : α), p a → β} {o o' : Option α} {h} :
     (or o o').pmap f h =
       match o with
-      | none => o'.pmap f (fun a h' => h a (by simp [h']))
-      | some a => some (f a (h a (by simp))) := by
+      | none => o'.pmap f (fun a h' => h a h')
+      | some a => some (f a (h a rfl)) := by
   cases o <;> simp
 
 theorem pmap_pred_congr {α : Type u}
@@ -1299,18 +1073,6 @@ theorem pmap_congr {α : Type u} {β : Type v}
   · dsimp
     rw [hf]
 
-theorem pmap_guard {q : α → Bool} {p : α → Prop} (f : (x : α) → p x → β) {x : α}
-    (h : ∀ (a : α), guard q x = some a → p a) :
-    (guard q x).pmap f h = if h' : q x then some (f x (h _ (by simp_all))) else none := by
-  simp only [guard_eq_ite]
-  split <;> simp_all
-
-@[simp]
-theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
-    {h : ∀ a, o = some a → p a} {h'} :
-    (o.pmap f h).get h' = f (o.get (by simpa using h')) (h _ (by simp)) := by
-  cases o <;> simp
-
 /-! ### pelim -/
 
 @[simp, grind] theorem pelim_none : pelim none b f = b := rfl
@@ -1339,22 +1101,6 @@ theorem pelim_filter {o : Option α} {b : β} {f : (a : α) → a ∈ o.filter p
     | false => by simp [pelim_congr_left (filter_some_neg h), h]
     | true => by simp [pelim_congr_left (filter_some_pos h), h]
 
-theorem pelim_join {o : Option (Option α)} {b : β} {f : (a : α) → a ∈ o.join → β} :
-    o.join.pelim b f = o.pelim b (fun o' ho' => o'.pelim b (fun a ha => f a (by simp_all))) := by
-  cases o <;> simp <;> congr
-
-@[congr]
-theorem pelim_congr {o o' : Option α} {b b' : β}
-    {f : (a : α) → o = some a → β} {g : (a : α) → o' = some a → β}
-    (ho : o = o') (hb : b = b') (hf : ∀ a ha, f a (ho.trans ha) = g a ha) :
-    o.pelim b f = o'.pelim b' g := by
-  cases ho; cases hb; cases o <;> apply_assumption
-
-theorem pelim_guard {a : α} {f : (a' : α) → guard p a = some a' → β} :
-    (guard p a).pelim b f = if h : p a then f a (by simpa) else b := by
-  simp only [guard]
-  split <;> simp
-
 /-! ### pfilter -/
 
 @[congr]
@@ -1386,15 +1132,6 @@ theorem isSome_of_isSome_pfilter {α : Type _} {o : Option α} {p : (a : α) →
     (h : (o.pfilter p).isSome) : o.isSome :=
   (isSome_pfilter_iff_get.mp h).1
 
-theorem isNone_pfilter_iff {o : Option α} {p : (a : α) → o = some a → Bool} :
-    (o.pfilter p).isNone ↔ ∀ (a : α) (ha : o = some a), p a ha = false := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [pfilter_some, isNone_iff_eq_none, ite_eq_right_iff, reduceCtorEq, imp_false,
-      Bool.not_eq_true, some.injEq]
-    exact ⟨fun h _ h' => h' ▸ h, fun h => h _ rfl⟩
-
 @[simp, grind] theorem get_pfilter {α : Type _} {o : Option α} {p : (a : α) → o = some a → Bool}
     (h : (o.pfilter p).isSome) :
     (o.pfilter p).get h = o.get (isSome_of_isSome_pfilter h) := by
@@ -1468,53 +1205,6 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
   · rfl
   · simp only [Option.pfilter, Bool.cond_eq_ite, Option.pbind_some]
 
-theorem filter_pmap {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), o = some a → p a}
-    {q : β → Bool} : (o.pmap f h).filter q = (o.pfilter (fun a h' => q (f a (h _ h')))).pmap f
-      (fun _ h' => h _ (eq_some_of_pfilter_eq_some h')) := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [pmap_some, filter_some, pfilter_some]
-    split <;> simp
-
-theorem pfilter_join {o : Option (Option α)} {p : (a : α) → o.join = some a → Bool} :
-    o.join.pfilter p = (o.pfilter (fun o' h => o'.pelim false (fun a ha => p a (by simp_all)))).join := by
-  cases o with
-  | none => simp
-  | some o' =>
-    cases o' with
-    | none => simp
-    | some a =>
-      simp only [join_some, pfilter_some, pelim_some]
-      split <;> simp
-
-theorem join_pfilter {o : Option (Option α)} {p : (o' : Option α) → o = some o' → Bool} :
-    (o.pfilter p).join = o.pbind (fun o' ho' => if p o' ho' then o' else none) := by
-  cases o <;> simp <;> split <;> simp
-
-theorem elim_pfilter {o : Option α} {b : β} {f : α → β} {p : (a : α) → o = some a → Bool} :
-    (o.pfilter p).elim b f = o.pelim b (fun a ha => if p a ha then f a else b) := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [pfilter_some, pelim_some]
-    split <;> simp
-
-theorem pelim_pfilter {o : Option α} {b : β} {p : (a : α) → o = some a → Bool}
-    {f : (a : α) → o.pfilter p = some a → β} :
-    (o.pfilter p).pelim b f = o.pelim b
-      (fun a ha => if hp : p a ha then f a (pfilter_eq_some_iff.2 ⟨_, hp⟩) else b) := by
-  cases o with
-  | none => simp
-  | some a =>
-    simp only [pfilter_some, pelim_some]
-    split <;> simp
-
-theorem pfilter_guard {a : α} {p : α → Bool} {q : (a' : α) → guard p a = some a' → Bool} :
-    (guard p a).pfilter q = if ∃ (h : p a), q a (by simp [h]) then some a else none := by
-  simp only [guard]
-  split <;> simp_all
-
 /-! ### LT and LE -/
 
 @[simp, grind] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]
@@ -1527,112 +1217,6 @@ theorem pfilter_guard {a : α} {p : α → Bool} {q : (a' : α) → guard p a =
 @[simp] theorem le_none [LE α] {a : Option α} : a ≤ none ↔ a = none := by cases a <;> simp
 @[simp, grind] theorem some_le_some [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b := by simp [LE.le, Option.le]
 
-@[simp]
-theorem filter_le [LE α] (le_refl : ∀ x : α, x ≤ x) {o : Option α} {p : α → Bool} : o.filter p ≤ o := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [le_refl]
-
-@[simp]
-theorem filter_lt [LT α] (lt_irrefl : ∀ x : α, ¬x < x) {o : Option α} {p : α → Bool} : o.filter p < o ↔ o.any (fun a => !p a) := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [*]
-
-@[simp]
-theorem le_filter [LE α] (le_refl : ∀ x : α, x ≤ x) {o : Option α} {p : α → Bool} : o ≤ o.filter p ↔ o.all p := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [*]
-
-@[simp]
-theorem not_lt_filter [LT α] (lt_irrefl : ∀ x : α, ¬x < x) {o : Option α} {p : α → Bool} : ¬o < o.filter p := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [lt_irrefl]
-
-@[simp]
-theorem pfilter_le [LE α] (le_refl : ∀ x : α, x ≤ x) {o : Option α} {p : (a : α) → o = some a → Bool} :
-    o.pfilter p ≤ o := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [pfilter_some]
-    split <;> simp [*]
-
-@[simp]
-theorem not_lt_pfilter [LT α] (lt_irrefl : ∀ x : α, ¬x < x) {o : Option α}
-    {p : (a : α) → o = some a → Bool} : ¬o < o.pfilter p := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [pfilter_some]
-    split <;> simp [lt_irrefl]
-
-theorem join_le [LE α] {o : Option (Option α)} {o' : Option α} : o.join ≤ o' ↔ o ≤ some o' := by
-  cases o <;> simp
-
-@[simp]
-theorem guard_le_some [LE α] (le_refl : ∀ x : α, x ≤ x) {x : α} {p : α → Bool} : guard p x ≤ some x := by
-  simp only [guard_eq_ite]
-  split <;> simp [le_refl]
-
-@[simp]
-theorem guard_lt_some [LT α] (lt_irrefl : ∀ x : α, ¬x < x) {x : α} {p : α → Bool} :
-    guard p x < some x ↔ p x = false := by
-  simp only [guard_eq_ite]
-  split <;> simp [*]
-
-theorem left_le_of_merge_le [LE α] {f : α → α → α} (hf : ∀ a b c, f a b ≤ c → a ≤ c)
-    {o₁ o₂ o₃ : Option α} : o₁.merge f o₂ ≤ o₃ → o₁ ≤ o₃ := by
-  cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
-  simpa using hf _ _ _
-
-theorem right_le_of_merge_le [LE α] {f : α → α → α} (hf : ∀ a b c, f a b ≤ c → b ≤ c)
-    {o₁ o₂ o₃ : Option α} : o₁.merge f o₂ ≤ o₃ → o₂ ≤ o₃ := by
-  cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
-  simpa using hf _ _ _
-
-theorem merge_le [LE α] {f : α → α → α} {o₁ o₂ o₃ : Option α}
-    (hf : ∀ a b c, a ≤ c → b ≤ c → f a b ≤ c) : o₁ ≤ o₃ → o₂ ≤ o₃ → o₁.merge f o₂ ≤ o₃ := by
-  cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
-  simpa using hf _ _ _
-
-@[simp]
-theorem merge_le_iff [LE α] {f : α → α → α} {o₁ o₂ o₃ : Option α}
-    (hf : ∀ a b c, f a b ≤ c ↔ a ≤ c ∧ b ≤ c) :
-    o₁.merge f o₂ ≤ o₃ ↔ o₁ ≤ o₃ ∧ o₂ ≤ o₃ := by
-  cases o₁ <;> cases o₂ <;> cases o₃ <;> simp [*]
-
-theorem left_lt_of_merge_lt [LT α] {f : α → α → α} (hf : ∀ a b c, f a b < c → a < c)
-    {o₁ o₂ o₃ : Option α} : o₁.merge f o₂ < o₃ → o₁ < o₃ := by
-  cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
-  simpa using hf _ _ _
-
-theorem right_lt_of_merge_lt [LT α] {f : α → α → α} (hf : ∀ a b c, f a b < c → b < c)
-    {o₁ o₂ o₃ : Option α} : o₁.merge f o₂ < o₃ → o₂ < o₃ := by
-  cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
-  simpa using hf _ _ _
-
-theorem merge_lt [LT α] {f : α → α → α} {o₁ o₂ o₃ : Option α}
-    (hf : ∀ a b c, a < c → b < c → f a b < c) : o₁ < o₃ → o₂ < o₃ → o₁.merge f o₂ < o₃ := by
-  cases o₁ <;> cases o₂ <;> cases o₃ <;> try (simp; done)
-  simpa using hf _ _ _
-
-@[simp]
-theorem merge_lt_iff [LT α] {f : α → α → α} {o₁ o₂ o₃ : Option α}
-    (hf : ∀ a b c, f a b < c ↔ a < c ∧ b < c) :
-    o₁.merge f o₂ < o₃ ↔ o₁ < o₃ ∧ o₂ < o₃ := by
-  cases o₁ <;> cases o₂ <;> cases o₃ <;> simp [*]
-
 /-! ### Rel -/
 
 @[simp] theorem rel_some_some {r : α → β → Prop} : Rel r (some a) (some b) ↔ r a b :=
@@ -1714,192 +1298,4 @@ theorem merge_max [Max α] : merge (α := α) max = max := by
 instance [Max α] : Std.LawfulIdentity (α := Option α) max none := by
   rw [← merge_max]; infer_instance
 
-instance [Max α] [Std.IdempotentOp (α := α) max] : Std.IdempotentOp (α := Option α) max where
-  idempotent o := by cases o <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem max_filter_left [Max α] [Std.IdempotentOp (α := α) max] {p : α → Bool} {o : Option α} :
-    max (o.filter p) o = o := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem max_filter_right [Max α] [Std.IdempotentOp (α := α) max] {p : α → Bool} {o : Option α} :
-    max o (o.filter p) = o := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem min_filter_left [Min α] [Std.IdempotentOp (α := α) min] {p : α → Bool} {o : Option α} :
-    min (o.filter p) o = o.filter p := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem min_filter_right [Min α] [Std.IdempotentOp (α := α) min] {p : α → Bool} {o : Option α} :
-    min o (o.filter p) = o.filter p := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [filter_some]
-    split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem max_pfilter_left [Max α] [Std.IdempotentOp (α := α) max] {o : Option α} {p : (a : α) → o = some a → Bool} :
-    max (o.pfilter p) o = o := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [pfilter_some]
-    split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem max_pfilter_right [Max α] [Std.IdempotentOp (α := α) max] {o : Option α} {p : (a : α) → o = some a → Bool} :
-    max o (o.pfilter p) = o := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [pfilter_some]
-    split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem min_pfilter_left [Min α] [Std.IdempotentOp (α := α) min] {o : Option α} {p : (a : α) → o = some a → Bool} :
-    min (o.pfilter p) o = o.pfilter p := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [pfilter_some]
-    split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem min_pfilter_right [Min α] [Std.IdempotentOp (α := α) min] {o : Option α} {p : (a : α) → o = some a → Bool} :
-    min o (o.pfilter p) = o.pfilter p := by
-  cases o with
-  | none => simp
-  | some _ =>
-    simp only [pfilter_some]
-    split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem isSome_max [Max α] {o o' : Option α} : (max o o').isSome = (o.isSome || o'.isSome) := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem isNone_max [Max α] {o o' : Option α} : (max o o').isNone = (o.isNone && o'.isNone) := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem isSome_min [Min α] {o o' : Option α} : (min o o').isSome = (o.isSome && o'.isSome) := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem isNone_min [Min α] {o o' : Option α} : (min o o').isNone = (o.isNone || o'.isNone) := by
-  cases o <;> cases o' <;> simp
-
-theorem max_join_left [Max α] {o : Option (Option α)} {o' : Option α} :
-    max o.join o' = (max o (some o')).get (by simp) := by
-  cases o <;> simp
-
-theorem max_join_right [Max α] {o : Option α} {o' : Option (Option α)} :
-    max o o'.join = (max (some o) o').get (by simp) := by
-  cases o' <;> simp
-
-theorem join_max [Max α] {o o' : Option (Option α)} :
-    (max o o').join = max o.join o'.join := by
-  cases o <;> cases o' <;> simp
-
-theorem min_join_left [Min α] {o : Option (Option α)} {o' : Option α} :
-    min o.join o' = (min o (some o')).join := by
-  cases o <;> simp
-
-theorem min_join_right [Min α] {o : Option α} {o' : Option (Option α)} :
-    min o o'.join = (min (some o) o').join := by
-  cases o' <;> simp
-
-theorem join_min [Min α] {o o' : Option (Option α)} :
-    (min o o').join = min o.join o'.join := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem min_guard_some [Min α] [Std.IdempotentOp (α := α) min] {x : α} {p : α → Bool} :
-    min (guard p x) (some x) = guard p x := by
-  simp only [guard_eq_ite]
-  split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem min_some_guard [Min α] [Std.IdempotentOp (α := α) min] {x : α} {p : α → Bool} :
-    min (some x) (guard p x) = guard p x := by
-  simp only [guard_eq_ite]
-  split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem max_guard_some [Max α] [Std.IdempotentOp (α := α) max] {x : α} {p : α → Bool} :
-    max (guard p x) (some x) = some x := by
-  simp only [guard_eq_ite]
-  split <;> simp [Std.IdempotentOp.idempotent]
-
-@[simp]
-theorem max_some_guard [Max α] [Std.IdempotentOp (α := α) max] {x : α} {p : α → Bool} :
-    max (some x) (guard p x) = some x := by
-  simp only [guard_eq_ite]
-  split <;> simp [Std.IdempotentOp.idempotent]
-
-theorem max_eq_some_iff [Max α] {o o' : Option α} {a : α} :
-    max o o' = some a ↔ (o = some a ∧ o' = none) ∨ (o = none ∧ o' = some a) ∨
-      (∃ b c, o = some b ∧ o' = some c ∧ max b c = a) := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem max_eq_none_iff [Max α] {o o' : Option α} :
-    max o o' = none ↔ o = none ∧ o' = none := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem min_eq_some_iff [Min α] {o o' : Option α} {a : α} :
-    min o o' = some a ↔ ∃ b c, o = some b ∧ o' = some c ∧ min b c = a := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem min_eq_none_iff [Min α] {o o' : Option α} :
-    min o o' = none ↔ o = none ∨ o' = none := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem any_max [Max α] {o o' : Option α} {p : α → Bool} (hp : ∀ a b, p (max a b) = (p a || p b)) :
-    (max o o').any p = (o.any p || o'.any p) := by
-  cases o <;> cases o' <;> simp [hp]
-
-@[simp]
-theorem all_min [Min α] {o o' : Option α} {p : α → Bool} (hp : ∀ a b, p (min a b) = (p a || p b)) :
-    (min o o').all p = (o.all p || o'.all p) := by
-  cases o <;> cases o' <;> simp [hp]
-
-theorem isSome_left_of_isSome_min [Min α] {o o' : Option α} : (min o o').isSome → o.isSome := by
-  cases o <;> simp
-
-theorem isSome_right_of_isSome_min [Min α] {o o' : Option α} : (min o o').isSome → o'.isSome := by
-  cases o' <;> simp
-
-@[simp]
-theorem get_min [Min α] {o o' : Option α} {h} :
-    (min o o').get h = min (o.get (isSome_left_of_isSome_min h)) (o'.get (isSome_right_of_isSome_min h)) := by
-  cases o <;> cases o' <;> simp
-
-theorem map_max [Max α] [Max β] {o o' : Option α} {f : α → β} (hf : ∀ x y, f (max x y) = max (f x) (f y)) :
-    (max o o').map f = max (o.map f) (o'.map f) := by
-  cases o <;> cases o' <;> simp [*]
-
-theorem map_min [Min α] [Min β] {o o' : Option α} {f : α → β} (hf : ∀ x y, f (min x y) = min (f x) (f y)) :
-    (min o o').map f = min (o.map f) (o'.map f) := by
-  cases o <;> cases o' <;> simp [*]
-
 end Option

src/Init/Data/Option/List.lean

@@ -7,8 +7,6 @@ module
 
 prelude
 import Init.Data.List.Lemmas
-import all Init.Data.List.Control
-import all Init.Data.Option.Instances
 
 namespace Option
 
@@ -60,42 +58,6 @@ theorem toList_bind {o : Option α} {f : α → Option β} :
   cases o <;> simp
 
 theorem toList_join {o : Option (Option α)} : o.join.toList = o.toList.flatMap Option.toList := by
-  simp [toList_bind, ← bind_id_eq_join]
-
-theorem toList_map {o : Option α} {f : α → β} : (o.map f).toList = o.toList.map f := by
-  cases o <;> simp
-
-theorem toList_min [Min α] {o o' : Option α} :
-    (min o o').toList = o.toList.zipWith min o'.toList := by
-  cases o <;> cases o' <;> simp
-
-@[simp]
-theorem length_toList_le {o : Option α} : o.toList.length ≤ 1 := by
-  cases o <;> simp
-
-theorem length_toList_eq_ite {o : Option α} :
-    o.toList.length = if o.isSome then 1 else 0 := by
-  cases o <;> simp
-
-@[simp]
-theorem toList_eq_nil_iff {o : Option α} : o.toList = [] ↔ o = none := by
-  cases o <;> simp
-
-@[simp]
-theorem toList_eq_singleton_iff {o : Option α} : o.toList = [a] ↔ o = some a := by
-  cases o <;> simp
-
-@[simp]
-theorem length_toList_eq_zero_iff {o : Option α} :
-    o.toList.length = 0 ↔ o = none := by
-  cases o <;> simp
-
-@[simp]
-theorem length_toList_eq_one_iff {o : Option α} :
-    o.toList.length = 1 ↔ o.isSome := by
-  cases o <;> simp
-
-theorem length_toList_choice_eq_one [Nonempty α] : (choice α).toList.length = 1 := by
-  simp
+  simp [toList_bind, join_eq_bind_id]
 
 end Option

src/Init/Data/Option/Monadic.lean

@@ -7,14 +7,13 @@ module
 
 prelude
 
-import all Init.Data.Option.Instances
 import Init.Data.Option.Attach
 import Init.Control.Lawful.Basic
 
 namespace Option
 
-@[simp, grind] theorem bindM_none [Pure m] (f : α → m (Option β)) : none.bindM f = pure none := rfl
-@[simp, grind] theorem bindM_some [Pure m] (a) (f : α → m (Option β)) : (some a).bindM f = f a := by
+@[simp, grind] theorem bindM_none [Monad m] (f : α → m (Option β)) : none.bindM f = pure none := rfl
+@[simp, grind] theorem bindM_some [Monad m] [LawfulMonad m] (a) (f : α → m (Option β)) : (some a).bindM f = f a := by
   simp [Option.bindM]
 
 -- We simplify `Option.forM` to `forM`.
@@ -30,10 +29,6 @@ namespace Option
     forM (o.map g) f = forM o (fun a => f (g a)) := by
   cases o <;> simp
 
-theorem forM_join [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α → m PUnit) :
-    forM o.join f = forM o (forM · f) := by
-  cases o <;> simp
-
 @[simp, grind] theorem forIn'_none [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) :
     forIn' none b f = pure b := by
   rfl
@@ -44,7 +39,7 @@ theorem forM_join [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α →
   rw [map_eq_pure_bind]
   congr
   funext x
-  split <;> simp
+  split <;> rfl
 
 @[simp, grind] theorem forIn_none [Monad m] (b : β) (f : α → β → m (ForInStep β)) :
     forIn none b f = pure b := by
@@ -56,7 +51,7 @@ theorem forM_join [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α →
   rw [map_eq_pure_bind]
   congr
   funext x
-  split <;> simp
+  split <;> rfl
 
 @[congr] theorem forIn'_congr [Monad m] [LawfulMonad m] {as bs : Option α} (w : as = bs)
     {b b' : β} (hb : b = b')
@@ -101,13 +96,6 @@ theorem forIn'_eq_pelim [Monad m] [LawfulMonad m]
     forIn' (o.map g) init f = forIn' o init fun a h y => f (g a) (mem_map_of_mem g h) y := by
   cases o <;> simp
 
-theorem forIn'_join [Monad m] [LawfulMonad m] (b : β) (o : Option (Option α))
-    (f : (a : α) → a ∈ o.join → β → m (ForInStep β)) :
-    forIn' o.join b f = forIn' o b (fun o' ho' b => ForInStep.yield <$> forIn' o' b (fun a ha b' => f a (by simp_all [join_eq_some_iff]) b')) := by
-  cases o with
-  | none => simp
-  | some a => simpa using forIn'_congr rfl rfl (by simp)
-
 theorem forIn_eq_elim [Monad m] [LawfulMonad m]
     (o : Option α) (f : (a : α) → β → m (ForInStep β)) (b : β) :
     forIn o b f =
@@ -137,11 +125,6 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
     forIn (o.map g) init f = forIn o init fun a y => f (g a) y := by
   cases o <;> simp
 
-theorem forIn_join [Monad m] [LawfulMonad m]
-    (o : Option (Option α)) (f : α → β → m (ForInStep β)) :
-    forIn o.join init f = forIn o init (fun o' b => ForInStep.yield <$> forIn o' b f) := by
-  cases o <;> simp
-
 @[simp] theorem elimM_pure [Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α → m β) :
     Option.elimM (pure x : m (Option α)) y z = x.elim y z := by
   simp [Option.elimM]
@@ -154,8 +137,11 @@ theorem forIn_join [Monad m] [LawfulMonad m]
     (y : m γ) (z : β → m γ) : Option.elimM (f <$> x) y z = (do Option.elim (f (← x)) y z) := by
   simp [Option.elimM]
 
-@[simp] theorem tryCatch_eq_or (o : Option α) (alternative : Unit → Option α) :
-    tryCatch o alternative = o.or (alternative ()) := by cases o <;> rfl
+@[simp] theorem tryCatch_none (alternative : Unit → Option α) :
+  (tryCatch none alternative) = alternative () := rfl
+
+@[simp] theorem tryCatch_some (a : α) (alternative : Unit → Option α) :
+  (tryCatch (some a) alternative) = some a := rfl
 
 @[simp] theorem throw_eq_none : throw () = (none : Option α) := rfl
 
@@ -164,21 +150,4 @@ theorem forIn_join [Monad m] [LawfulMonad m]
 theorem filterM_some [Applicative m] (p : α → m Bool) (a : α) :
     (some a).filterM p = (fun b => if b then some a else none) <$> p a := rfl
 
-theorem sequence_join [Applicative m] [LawfulApplicative m] {o : Option (Option (m α))} :
-    o.join.sequence = join <$> sequence (o.map sequence) := by
-  cases o <;> simp
-
-theorem bindM_join [Pure m] {f : α → m (Option β)} {o : Option (Option α)} :
-    o.join.bindM f = o.bindM (·.bindM f) := by
-  cases o <;> simp
-
-theorem mapM_join [Applicative m] [LawfulApplicative m] {f : α → m β} {o : Option (Option α)} :
-    o.join.mapM f = join <$> o.mapM (Option.mapM f) := by
-  cases o <;> simp
-
-theorem mapM_guard [Applicative m] {x : α} {p : α → Bool} {f : α → m β} :
-    (guard p x).mapM f = if p x then some <$> f x else pure none := by
-  simp only [guard_eq_ite]
-  split <;> simp
-
 end Option

src/Init/Data/Ord.lean

@@ -10,7 +10,7 @@ prelude
 import Init.Data.String.Basic
 import Init.Data.Array.Basic
 import Init.Data.SInt.Basic
-import all Init.Data.Vector.Basic
+import Init.Data.Vector.Basic
 
 /--
 The result of a comparison according to a total order.
@@ -88,7 +88,7 @@ Ordering.gt
 Ordering.lt
 ```
 -/
-@[macro_inline, expose] def «then» (a b : Ordering) : Ordering :=
+@[macro_inline] def «then» (a b : Ordering) : Ordering :=
   match a with
   | .eq => b
   | a => a
@@ -768,7 +768,7 @@ def lexOrd [Ord α] [Ord β] : Ord (α × β) where
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.lt`.
 -/
-@[expose] def ltOfOrd [Ord α] : LT α where
+def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
 instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
@@ -778,7 +778,7 @@ instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
 satisfies `Ordering.isLE`.
 -/
-@[expose] def leOfOrd [Ord α] : LE α where
+def leOfOrd [Ord α] : LE α where
   le a b := (compare a b).isLE
 
 instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
@@ -795,7 +795,7 @@ protected def toBEq (ord : Ord α) : BEq α where
 /--
 Constructs an `LT` instance from an `Ord` instance.
 -/
-@[expose] protected def toLT (ord : Ord α) : LT α :=
+protected def toLT (ord : Ord α) : LT α :=
   ltOfOrd
 
 instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
@@ -804,7 +804,7 @@ instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
 /--
 Constructs an `LE` instance from an `Ord` instance.
 -/
-@[expose] protected def toLE (ord : Ord α) : LE α :=
+protected def toLE (ord : Ord α) : LE α :=
   leOfOrd
 
 instance [i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i)) :=
@@ -849,4 +849,13 @@ comparisons.
 protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
+/--
+Constructs an order which compares elements of an `Array` in lexicographic order.
+-/
+protected def arrayOrd [a : Ord α] : Ord (Array α) where
+  compare x y :=
+    let _ : LT α := a.toLT
+    let _ : BEq α := a.toBEq
+    if List.lex x.toList y.toList then .lt else if x == y then .eq else .gt
+
 end Ord

src/Init/Data/RArray.lean

@@ -9,8 +9,6 @@ module
 prelude
 import Init.PropLemmas
 
-@[expose] section
-
 namespace Lean
 
 /--

src/Init/Data/Range/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Range.Basic
+import Init.Data.Range.Basic
 import Init.Data.List.Range
 import Init.Data.List.Monadic
 import Init.Data.Nat.Div.Lemmas

src/Init/Data/Repr.lean

@@ -211,7 +211,7 @@ private def reprArray : Array String := Id.run do
   List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
-  if h : n < Nat.reprArray.size then Nat.reprArray.getInternal n h else
+  if h : n < 128 then Nat.reprArray.getInternal n h else
   if h : n < USize.size then (USize.ofNatLT n h).repr
   else (toDigits 10 n).asString
 

src/Init/Data/SInt/Basic.lean

@@ -429,8 +429,8 @@ Examples:
 def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-attribute [instance] Int8.decLt Int8.decLe
-
+instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
+instance (a b : Int8) : Decidable (a ≤ b) := Int8.decLe a b
 instance : Max Int8 := maxOfLe
 instance : Min Int8 := minOfLe
 
@@ -800,8 +800,8 @@ Examples:
 def Int16.decLe (a b : Int16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-attribute [instance] Int16.decLt Int16.decLe
-
+instance (a b : Int16) : Decidable (a < b) := Int16.decLt a b
+instance (a b : Int16) : Decidable (a ≤ b) := Int16.decLe a b
 instance : Max Int16 := maxOfLe
 instance : Min Int16 := minOfLe
 
@@ -1187,8 +1187,8 @@ Examples:
 def Int32.decLe (a b : Int32) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-attribute [instance] Int32.decLt Int32.decLe
-
+instance (a b : Int32) : Decidable (a < b) := Int32.decLt a b
+instance (a b : Int32) : Decidable (a ≤ b) := Int32.decLe a b
 instance : Max Int32 := maxOfLe
 instance : Min Int32 := minOfLe
 
@@ -1593,8 +1593,8 @@ Examples:
 def Int64.decLe (a b : Int64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-attribute [instance] Int64.decLt Int64.decLe
-
+instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
+instance (a b : Int64) : Decidable (a ≤ b) := Int64.decLe a b
 instance : Max Int64 := maxOfLe
 instance : Min Int64 := minOfLe
 
@@ -1986,7 +1986,7 @@ Examples:
 def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-attribute [instance] ISize.decLt ISize.decLe
-
+instance (a b : ISize) : Decidable (a < b) := ISize.decLt a b
+instance (a b : ISize) : Decidable (a ≤ b) := ISize.decLe a b
 instance : Max ISize := maxOfLe
 instance : Min ISize := minOfLe

src/Init/Data/SInt/Bitwise.lean

@@ -6,11 +6,7 @@ Authors: Markus Himmel
 module
 
 prelude
-import all Init.Data.UInt.Basic
 import Init.Data.UInt.Bitwise
-import all Init.Data.BitVec.Basic
-import all Init.Data.BitVec.Lemmas
-import all Init.Data.SInt.Basic
 import Init.Data.SInt.Lemmas
 
 set_option hygiene false in

src/Init/Data/SInt/Lemmas.lean

@@ -6,13 +6,9 @@ Authors: Markus Himmel
 module
 
 prelude
-import all Init.Data.Nat.Bitwise.Basic
-import all Init.Data.SInt.Basic
-import all Init.Data.BitVec.Basic
+import Init.Data.SInt.Basic
 import Init.Data.BitVec.Bitblast
-import all Init.Data.BitVec.Lemmas
 import Init.Data.Int.LemmasAux
-import all Init.Data.UInt.Basic
 import Init.Data.UInt.Lemmas
 import Init.System.Platform
 
@@ -1459,16 +1455,16 @@ theorem ISize.toInt64_ofIntLE {n : Int} (h₁ h₂) :
   ISize.toInt64_ofNat' (by rw [toInt_maxValue]; cases System.Platform.numBits_eq <;> simp_all <;> omega)
 
 @[simp] theorem Int8.ofIntLE_bitVecToInt (n : BitVec 8) :
-    Int8.ofIntLE n.toInt (by exact n.le_toInt) (by exact n.toInt_le) = Int8.ofBitVec n :=
+    Int8.ofIntLE n.toInt n.le_toInt n.toInt_le = Int8.ofBitVec n :=
   Int8.toBitVec.inj (by simp)
 @[simp] theorem Int16.ofIntLE_bitVecToInt (n : BitVec 16) :
-    Int16.ofIntLE n.toInt (by exact n.le_toInt) (by exact n.toInt_le) = Int16.ofBitVec n :=
+    Int16.ofIntLE n.toInt n.le_toInt n.toInt_le = Int16.ofBitVec n :=
   Int16.toBitVec.inj (by simp)
 @[simp] theorem Int32.ofIntLE_bitVecToInt (n : BitVec 32) :
-    Int32.ofIntLE n.toInt (by exact n.le_toInt) (by exact n.toInt_le) = Int32.ofBitVec n :=
+    Int32.ofIntLE n.toInt n.le_toInt n.toInt_le = Int32.ofBitVec n :=
   Int32.toBitVec.inj (by simp)
 @[simp] theorem Int64.ofIntLE_bitVecToInt (n : BitVec 64) :
-    Int64.ofIntLE n.toInt (by exact n.le_toInt) (by exact n.toInt_le) = Int64.ofBitVec n :=
+    Int64.ofIntLE n.toInt n.le_toInt n.toInt_le = Int64.ofBitVec n :=
   Int64.toBitVec.inj (by simp)
 @[simp] theorem ISize.ofIntLE_bitVecToInt (n : BitVec System.Platform.numBits) :
     ISize.ofIntLE n.toInt (toInt_minValue ▸ n.le_toInt)

src/Init/Data/String/Basic.lean

@@ -41,7 +41,7 @@ Non-strict inequality on strings, typically used via the `≤` operator.
 
 `a ≤ b` is defined to mean `¬ b < a`.
 -/
-@[expose, reducible] protected def le (a b : String) : Prop := ¬ b < a
+@[reducible] protected def le (a b : String) : Prop := ¬ b < a
 
 instance : LE String :=
   ⟨String.le⟩

src/Init/Data/String/Extra.lean

@@ -6,8 +6,7 @@ Author: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.ByteArray.Basic
-import all Init.Data.String.Basic
+import Init.Data.ByteArray
 import Init.Data.UInt.Lemmas
 
 namespace String

src/Init/Data/String/Lemmas.lean

@@ -32,4 +32,22 @@ protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
   have := String.lt_irrefl a
   intro h; subst h; contradiction
 
+instance ltIrrefl : Std.Irrefl (· < · : Char → Char → Prop) where
+  irrefl := Char.lt_irrefl
+
+instance leRefl : Std.Refl (· ≤ · : Char → Char → Prop) where
+  refl := Char.le_refl
+
+instance leTrans : Trans (· ≤ · : Char → Char → Prop) (· ≤ ·) (· ≤ ·) where
+  trans := Char.le_trans
+
+instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
+  antisymm _ _ := Char.le_antisymm
+
+instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
+  asymm _ _ := Char.lt_asymm
+
+instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
+  total := Char.le_total
+
 end String

src/Init/Data/Sum/Basic.lean

@@ -44,6 +44,7 @@ universe signature in consequence. The `Prop` version is `Or`.
 
 namespace Sum
 
+deriving instance DecidableEq for Sum
 deriving instance BEq for Sum
 
 section get

src/Init/Data/Sum/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro, Yury G. Kudryashov
 module
 
 prelude
-import all Init.Data.Sum.Basic
+import Init.Data.Sum.Basic
 import Init.Ext
 
 /-!

src/Init/Data/UInt/Basic.lean

@@ -222,8 +222,8 @@ Examples:
 def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
-attribute [instance] UInt8.decLt UInt8.decLe
-
+instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
+instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
 instance : Max UInt8 := maxOfLe
 instance : Min UInt8 := minOfLe
 
@@ -438,8 +438,8 @@ Examples:
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
-attribute [instance] UInt16.decLt UInt16.decLe
-
+instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
+instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
 instance : Max UInt16 := maxOfLe
 instance : Min UInt16 := minOfLe
 
@@ -567,14 +567,12 @@ protected def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (UI
 Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
 natural numbers. Usually accessed via the `<` operator.
 -/
--- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping puproses and
--- they should be defeq
-@[expose] protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
+protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
 /--
 Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
 natural numbers. Usually accessed via the `≤` operator.
 -/
-@[expose] protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
+protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
@@ -586,7 +584,8 @@ set_option linter.deprecated false in
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
 
 instance : Div UInt32       := ⟨UInt32.div⟩
--- `LT` and `LE` are already defined in `Init.Prelude`
+instance : LT UInt32        := ⟨UInt32.lt⟩
+instance : LE UInt32        := ⟨UInt32.le⟩
 
 /--
 Bitwise complement, also known as bitwise negation, for 32-bit unsigned integers. Usually accessed
@@ -831,8 +830,8 @@ Examples:
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
-attribute [instance] UInt64.decLt UInt64.decLe
-
+instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
+instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 instance : Max UInt64 := maxOfLe
 instance : Min UInt64 := minOfLe
 

src/Init/Data/UInt/BasicAux.lean

@@ -9,8 +9,6 @@ prelude
 import Init.Data.Fin.Basic
 import Init.Data.BitVec.BasicAux
 
-@[expose] section
-
 set_option linter.missingDocs true
 
 /-!
@@ -437,4 +435,5 @@ Examples:
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
-attribute [instance] USize.decLt USize.decLe
+instance (a b : USize) : Decidable (a < b) := USize.decLt a b
+instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b

src/Init/Data/UInt/Bitwise.lean

@@ -6,8 +6,6 @@ Authors: Markus Himmel, Mac Malone
 module
 
 prelude
-import all Init.Data.BitVec.Basic
-import all Init.Data.UInt.Basic
 import Init.Data.UInt.Lemmas
 import Init.Data.Fin.Bitwise