chore(*): bump to Lean 3.18.4 (#3610)

* Remove `pi_arity` and the `vm_override` for `by_cases`, which have moved to core
* Fix fallout from the change to the definition of `max`
* Fix a small number of errors caused by changes to instance caching
* Remove `min_add`, which is generalized by `min_add_add_right`  and make `to_additive` generate some lemmas



Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

Author: robertylewis

leanpkg.toml

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

src/algebra/order_functions.lean

@@ -97,7 +97,7 @@ theorem min_choice (a b : α) : min a b = a ∨ min a b = b :=
 by by_cases h : a ≤ b; simp [min, h]
 
 theorem max_choice (a b : α) : max a b = a ∨ max a b = b :=
-by by_cases h : a ≤ b; simp [max, h]
+by by_cases h : b ≤ a; simp [max, h]
 
 lemma le_of_max_le_left {a b c : α} (h : max a b ≤ c) : a ≤ c :=
 le_trans (le_max_left _ _) h
@@ -107,34 +107,18 @@ le_trans (le_max_right _ _) h
 
 end
 
-lemma min_add {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
-      min a b + c = min (a + c) (b + c) :=
-if hle : a ≤ b then
-  have a - c ≤ b - c, from sub_le_sub hle (le_refl _),
-  by simp * at *
-else
-  have b - c ≤ a - c, from sub_le_sub (le_of_lt (lt_of_not_ge hle)) (le_refl _),
-  by simp * at *
-
 lemma min_sub {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
       min a b - c = min (a - c) (b - c) :=
-by simp [min_add, sub_eq_add_neg]
-
+by simp only [min_add_add_right, sub_eq_add_neg]
 
 /- Some lemmas about types that have an ordering and a binary operation, with no
   rules relating them. -/
-lemma fn_min_add_fn_max [decidable_linear_order α] [add_comm_semigroup β] (f : α → β) (n m : α) :
-  f (min n m) + f (max n m) = f n + f m :=
-by { cases le_total n m with h h; simp [h, add_comm] }
-
-lemma min_add_max [decidable_linear_order α] [add_comm_semigroup α] (n m : α) :
-  min n m + max n m = n + m :=
-fn_min_add_fn_max id n m
-
+@[to_additive]
 lemma fn_min_mul_fn_max [decidable_linear_order α] [comm_semigroup β] (f : α → β) (n m : α) :
   f (min n m) * f (max n m) = f n * f m :=
 by { cases le_total n m with h h; simp [h, mul_comm] }
 
+@[to_additive]
 lemma min_mul_max [decidable_linear_order α] [comm_semigroup α] (n m : α) :
   min n m * max n m = n * m :=
 fn_min_mul_fn_max id n m
@@ -219,18 +203,9 @@ end
 
 lemma abs_max_sub_max_le_abs (a b c : α) : abs (max a c - max b c) ≤ abs (a - b) :=
 begin
-  simp only [max],
-  split_ifs,
-  { rw [sub_self, abs_zero], exact abs_nonneg _ },
-  { calc abs (c - b) = - (c - b) : abs_of_neg (sub_neg_of_lt (lt_of_not_ge h_1))
-      ... = b - c : neg_sub _ _
-      ... ≤ b - a : by { rw sub_le_sub_iff_left, exact h }
-      ... = - (a - b) : by rw neg_sub
-      ... ≤ abs (a - b) : neg_le_abs_self _ },
-  { calc abs (a - c) = a - c : abs_of_pos (sub_pos_of_lt (lt_of_not_ge h))
-      ... ≤ a - b : by { rw sub_le_sub_iff_left, exact h_1 }
-      ... ≤ abs (a - b) : le_abs_self _ },
-  { refl }
+  simp_rw [abs_le, le_sub_iff_add_le, sub_le_iff_le_add, ← max_add_add_left],
+  split; apply max_le_max; simp only [← le_sub_iff_add_le, ← sub_le_iff_le_add, sub_self, neg_le,
+    neg_le_abs_self, neg_zero, abs_nonneg, le_abs_self]
 end
 
 lemma max_sub_min_eq_abs' (a b : α) : max a b - min a b = abs (a - b) :=

src/algebra/ordered_group.lean

@@ -231,7 +231,7 @@ decidable_linear_order.lift coe units.ext
 @[simp, to_additive, norm_cast]
 theorem max_coe [monoid α] [decidable_linear_order α] {a b : units α} :
   (↑(max a b) : α) = max a b :=
-by by_cases a ≤ b; simp [max, h]
+by by_cases b ≤ a; simp [max, h]
 
 @[simp, to_additive, norm_cast]
 theorem min_coe [monoid α] [decidable_linear_order α] {a b : units α} :

src/computability/primrec.lean

@@ -581,7 +581,7 @@ theorem nat_le : primrec_rel ((≤) : ℕ → ℕ → Prop) :=
 end
 
 theorem nat_min : primrec₂ (@min ℕ _) := ite nat_le fst snd
-theorem nat_max : primrec₂ (@max ℕ _) := ite nat_le snd fst
+theorem nat_max : primrec₂ (@max ℕ _) := ite (nat_le.comp primrec.snd primrec.fst) fst snd
 
 theorem dom_bool (f : bool → α) : primrec f :=
 (cond primrec.id (const (f tt)) (const (f ff))).of_eq $

src/control/traversable/equiv.lean

@@ -109,7 +109,8 @@ protected def is_lawful_traversable' [_i : traversable t']
          map f = equiv.map eqv f)
   (h₁ : ∀ {α β} (f : β),
          map_const f = (equiv.map eqv ∘ function.const α) f)
-  (h₂ : ∀ {F : Type u → Type u} [applicative F] [is_lawful_applicative F]
+  (h₂ : ∀ {F : Type u → Type u} [applicative F],
+        by exactI ∀ [is_lawful_applicative F]
           {α β} (f : α → F β),
          traverse f = equiv.traverse eqv f) :
   _root_.is_lawful_traversable t' :=

src/data/int/cast.lean

@@ -151,7 +151,7 @@ by by_cases a ≤ b; simp [h, min]
 
 @[simp, norm_cast] theorem cast_max [decidable_linear_ordered_comm_ring α] {a b : ℤ} :
   (↑(max a b) : α) = max a b :=
-by by_cases a ≤ b; simp [h, max]
+by by_cases b ≤ a; simp [h, max]
 
 @[simp, norm_cast] theorem cast_abs [decidable_linear_ordered_comm_ring α] {q : ℤ} :
   ((abs q : ℤ) : α) = abs q :=

src/data/list/min_max.lean

@@ -237,22 +237,23 @@ theorem le_minimum_of_mem' {a : α} {l : list α} (ha : a ∈ l) : minimum l ≤
 theorem maximum_concat (a : α) (l : list α) : maximum (l ++ [a]) = max (maximum l) a :=
 begin
   rw max_comm,
-  simp only [maximum, argmax_concat, id, max],
+  simp only [maximum, argmax_concat, id],
   cases h : argmax id l,
-  { rw [if_neg], refl, exact not_le_of_gt (with_bot.bot_lt_some _) },
+  { rw [max_eq_left], refl, exact bot_le },
   change (coe : α → with_bot α) with some,
-  simp
+  rw [max_comm],
+  simp [max]
 end
 
 theorem minimum_concat (a : α) (l : list α) : minimum (l ++ [a]) = min (minimum l) a :=
-by simp only [min_comm _ (a : with_top α)]; exact @maximum_concat (order_dual α) _ _ _
+@maximum_concat (order_dual α) _ _ _
 
 theorem maximum_cons (a : α) (l : list α) : maximum (a :: l) = max a (maximum l) :=
 list.reverse_rec_on l (by simp [@max_eq_left (with_bot α) _ _ _ bot_le])
   (λ tl hd ih, by rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc])
 
 theorem minimum_cons (a : α) (l : list α) : minimum (a :: l) = min a (minimum l) :=
-min_comm (minimum l) a ▸ @maximum_cons (order_dual α) _ _ _
+@maximum_cons (order_dual α) _ _ _
 
 theorem maximum_eq_coe_iff {m : α} {l : list α} :
   maximum l = m ↔ m ∈ l ∧ (∀ a ∈ l, a ≤ m) :=

src/data/polynomial/monic.lean

@@ -160,7 +160,8 @@ begin
   { rw nontrivial_iff at h, push_neg at h, apply h, },
   haveI := h, clear h,
   have := monic.nat_degree_mul hp hq,
-  dsimp [next_coeff], rw this, simp [hp, hq], clear this,
+  dsimp only [next_coeff], rw this,
+  simp only [hp, hq, degree_eq_zero_iff_eq_one, add_eq_zero_iff], clear this,
   split_ifs; try { tauto <|> simp [h_1, h_2] },
   rename h_1 hp0, rename h_2 hq0, clear h,
   rw ← degree_eq_zero_iff_eq_one at hp0 hq0, assumption',
@@ -170,19 +171,21 @@ begin
   have : {(dp, dq - 1), (dp - 1, dq)} ⊆ nat.antidiagonal (dp + dq - 1),
   { rw insert_subset, split,
     work_on_goal 0 { rw [nat.mem_antidiagonal, nat.add_sub_assoc] },
-    work_on_goal 1 { simp only [singleton_subset_iff, nat.mem_antidiagonal], apply nat.sub_add_eq_add_sub },
+    work_on_goal 1 { simp only [singleton_subset_iff, nat.mem_antidiagonal],
+      apply nat.sub_add_eq_add_sub },
     all_goals { apply nat.succ_le_of_lt, apply nat.pos_of_ne_zero, assumption } },
   rw ← sum_subset this,
   { rw [sum_insert, sum_singleton], iterate 2 { rw coeff_nat_degree }, ring, assumption',
     suffices : dp ≠ dp - 1, { rw mem_singleton, simp [this] }, omega }, clear this,
-  intros x hx hx1, simp only [nat.mem_antidiagonal] at hx, simp only [mem_insert, mem_singleton] at hx1,
+  intros x hx hx1,
+  simp only [nat.mem_antidiagonal] at hx, simp only [mem_insert, mem_singleton] at hx1,
   suffices : p.coeff x.fst = 0 ∨ q.coeff x.snd = 0, cases this; simp [this],
   suffices : dp < x.fst ∨ dq < x.snd, cases this,
   { left,  apply coeff_eq_zero_of_nat_degree_lt, assumption },
   { right, apply coeff_eq_zero_of_nat_degree_lt, assumption },
-  by_cases h : dp < x.fst, { tauto }, push_neg at h, right,
-  have : x.fst ≠ dp - 1, { contrapose! hx1, right, ext, assumption, dsimp, omega },
-  have : x.fst ≠ dp,     { contrapose! hx1, left,  ext, assumption, dsimp, omega },
+  by_cases h : dp < x.fst, { left, exact h }, push_neg at h, right,
+  have : x.fst ≠ dp - 1, { contrapose! hx1, right, ext, assumption, dsimp only, omega },
+  have : x.fst ≠ dp,     { contrapose! hx1, left,  ext, assumption, dsimp only, omega },
   omega,
 end
 

src/data/rat/cast.lean

@@ -233,7 +233,7 @@ by by_cases a ≤ b; simp [h, min]
 
 @[simp, norm_cast] theorem cast_max [discrete_linear_ordered_field α] {a b : ℚ} :
   (↑(max a b) : α) = max a b :=
-by by_cases a ≤ b; simp [h, max]
+by by_cases b ≤ a; simp [h, max]
 
 @[simp, norm_cast] theorem cast_abs [discrete_linear_ordered_field α] {q : ℚ} :
   ((abs q : ℚ) : α) = abs q :=

src/measure_theory/borel_space.lean

@@ -333,7 +333,7 @@ hf.prod_mk hg is_measurable_le'
 lemma measurable.max [decidable_linear_order α] [order_closed_topology α] [second_countable_topology α]
   {f g : δ → α} (hf : measurable f) (hg : measurable g) :
   measurable (λa, max (f a) (g a)) :=
-hg.piecewise (is_measurable_le hf hg) hf
+hf.piecewise (is_measurable_le hg hf) hg
 
 lemma measurable.min [decidable_linear_order α] [order_closed_topology α] [second_countable_topology α]
   {f g : δ → α} (hf : measurable f) (hg : measurable g) :