feat(*): bump to lean 3.46.0 (#15994)

The only relevant change is that `is_strict_total_order` had a redundant assumption removed, and is now exactly the same as `is_strict_total_order'`. This old assumption is proved in `order/rel_classes.lean`, which has to be added as an import to a file, leading to two non-terminal `simp`s breaking.

Of course, the idea is to remove `is_strict_total_order'` in a follow-up PR.

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.45.0"
+lean_version = "leanprover-community/lean:3.46.0"
 path = "src"
 
 [dependencies]

src/data/rbmap/default.lean

@@ -70,7 +70,7 @@ lemma eq_some_of_to_value_eq_some {e : option (α × β)} {v : β} :
   to_value e = some v → ∃ k, e = some (k, v) :=
 begin
   cases e with val; simp [to_value, false_implies_iff],
-  { cases val, simp, intro h, subst v, constructor, refl }
+  { cases val, simp }
 end
 
 lemma eq_none_of_to_value_eq_none {e : option (α × β)} : to_value e = none → e = none :=

src/data/rbtree/main.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import data.rbtree.find
 import data.rbtree.insert
 import data.rbtree.min_max
+import order.rel_classes
 
 universes u
 
@@ -65,8 +66,8 @@ variables [decidable_rel lt]
 
 lemma insert_ne_mk_rbtree (t : rbtree α lt) (a : α) : t.insert a ≠ mk_rbtree α lt :=
 begin
-  cases t with n p, simp [insert, mk_rbtree], intro h, injection h with h',
-  apply rbnode.insert_ne_leaf lt n a h'
+  cases t with n p,
+  simpa [insert, mk_rbtree] using rbnode.insert_ne_leaf lt n a
 end
 
 lemma find_correct [is_strict_weak_order α lt] (a : α) (t : rbtree α lt) :

src/order/rel_classes.lean

@@ -147,6 +147,7 @@ See note [reducible non-instances]. -/
 
 /-- This is basically the same as `is_strict_total_order`, but that definition has a redundant
 assumption `is_incomp_trans α lt`. -/
+-- TODO: This is now exactly the same as `is_strict_total_order`, remove.
 @[algebra] class is_strict_total_order' (α : Type u) (lt : α → α → Prop)
   extends is_trichotomous α lt, is_strict_order α lt : Prop.
 
@@ -200,7 +201,17 @@ instance is_order_connected_of_is_strict_total_order'
 @[priority 100] -- see Note [lower instance priority]
 instance is_strict_total_order_of_is_strict_total_order'
   [is_strict_total_order' α r] : is_strict_total_order α r :=
-{..is_strict_weak_order_of_is_order_connected}
+{ }
+
+@[priority 100] -- see Note [lower instance priority]
+instance is_strict_weak_order_of_is_strict_total_order'
+  [is_strict_total_order' α r] : is_strict_weak_order α r :=
+{ ..is_strict_weak_order_of_is_order_connected }
+
+@[priority 100] -- see Note [lower instance priority]
+instance is_strict_weak_order_of_is_strict_total_order
+  [is_strict_total_order α r] : is_strict_weak_order α r :=
+by { haveI : is_strict_total_order' α r := {}, apply_instance }
 
 /-! ### Well-order -/