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>

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) :

src/meta/expr.lean

@@ -436,16 +436,6 @@ meta def dsimp (t : expr)
 do (s, to_unfold) ← mk_simp_set no_defaults attr_names hs,
    s.dsimplify to_unfold t cfg
 
-/-- Auxilliary definition for `expr.pi_arity` -/
-meta def pi_arity_aux : ℕ → expr → ℕ
-| n (pi _ _ _ b) := pi_arity_aux (n + 1) b
-| n e            := n
-
-/-- The arity of a pi-type. Does not perform any reduction of the expression.
-  In one application this was ~30 times quicker than `tactic.get_pi_arity`. -/
-meta def pi_arity : expr → ℕ :=
-pi_arity_aux 0
-
 /-- Get the names of the bound variables by a sequence of pis or lambdas. -/
 meta def binding_names : expr → list name
 | (pi n _ _ e)  := n :: e.binding_names

src/order/filter/filter_product.lean

@@ -133,9 +133,9 @@ lemma max_def [K : decidable_linear_order β] (U : is_ultrafilter φ) (x y : β*
 quotient.induction_on₂' x y $ λ a b, by unfold max;
 begin
   split_ifs,
-  exact quotient.sound'(by filter_upwards [h] λ i hi, (max_eq_right hi).symm),
+  exact quotient.sound'(by filter_upwards [h] λ i hi, (max_eq_left hi).symm),
   exact quotient.sound'(by filter_upwards [@le_of_not_le _ (germ.linear_order U) _ _ h]
-    λ i hi, (max_eq_left hi).symm),
+    λ i hi, (max_eq_right hi).symm),
 end
 
 lemma min_def [K : decidable_linear_order β] (U : is_ultrafilter φ) (x y : β*) :

src/ring_theory/algebra_tower.lean

@@ -64,7 +64,7 @@ by simp_rw [algebra.smul_def, ← mul_assoc, algebra_map_apply R S A,
     ← (algebra_map S A).map_mul, mul_comm s]
 
 @[ext] lemma algebra.ext {S : Type u} {A : Type v} [comm_semiring S] [semiring A]
-  (h1 h2 : algebra S A) (h : ∀ {r : S} {x : A}, (by clear h2; exact r • x) = r • x) : h1 = h2 :=
+  (h1 h2 : algebra S A) (h : ∀ {r : S} {x : A}, (by haveI := h1; exact r • x) = r • x) : h1 = h2 :=
 begin
   unfreezingI { cases h1 with f1 g1 h11 h12, cases h2 with f2 g2 h21 h22,
   cases f1, cases f2, congr', { ext r x, exact h },

src/set_theory/ordinal.lean

@@ -495,7 +495,7 @@ theorem type_eq {α β} {r : α → α → Prop} {s : β → β → Prop}
 by { refine eq.trans _ (by rw [←quotient.out_eq o]), cases quotient.out o, refl }
 
 @[elab_as_eliminator] theorem induction_on {C : ordinal → Prop}
-  (o : ordinal) (H : ∀ α r [is_well_order α r], C (type r)) : C o :=
+  (o : ordinal) (H : ∀ α r [is_well_order α r], by exactI C (type r)) : C o :=
 quot.induction_on o $ λ ⟨α, r, wo⟩, @H α r wo
 
 /-! ### The order on ordinals -/

src/tactic/core.lean

@@ -10,7 +10,6 @@ import meta.rb_map
 import data.bool
 import tactic.lean_core_docs
 import tactic.interactive_expr
-import tactic.fix_by_cases
 
 universe variable u
 

src/tactic/interval_cases.lean

@@ -117,7 +117,7 @@ meta def combine_lower_bounds : option expr → option expr → tactic (option e
 | (some prf) none := return $ some prf
 | none (some prf) := return $ some prf
 | (some prf₁) (some prf₂) :=
-  do option.some <$> to_expr ``(max_le %%prf₁ %%prf₂)
+  do option.some <$> to_expr ``(max_le %%prf₂ %%prf₁)
 
 /-- Inspect a given expression, using it to update a set of upper and lower bounds on `n`. -/
 meta def update_bounds (n : expr) (bounds : option expr × option expr) (e : expr) :

src/topology/algebra/ordered.lean

@@ -513,14 +513,13 @@ lemma frontier_lt_subset_eq : frontier {b | f b < g b} ⊆ {b | f b = g b} :=
 by rw ← frontier_compl;
    convert frontier_le_subset_eq hg hf; simp [ext_iff, eq_comm]
 
-@[continuity] lemma continuous.max : continuous (λb, max (f b) (g b)) :=
-have ∀b∈frontier {b | f b ≤ g b}, g b = f b, from assume b hb, (frontier_le_subset_eq hf hg hb).symm,
-continuous_if this hg hf
-
 @[continuity] lemma continuous.min : continuous (λb, min (f b) (g b)) :=
 have ∀b∈frontier {b | f b ≤ g b}, f b = g b, from assume b hb, frontier_le_subset_eq hf hg hb,
 continuous_if this hf hg
 
+@[continuity] lemma continuous.max : continuous (λb, max (f b) (g b)) :=
+@continuous.min (order_dual α) _ _ _ _ _ _ _ hf hg
+
 end
 
 lemma tendsto.max {b : filter β} {a₁ a₂ : α} (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) :