chore(*): upgrade to Lean 3.33.0c (#9165)

My main goal is to fix various diamonds with `sup`/`inf`, see leanprover-community/lean#609. I use lean-master + 1 fixup commit leanprover-community/lean#615.



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Author: 3 people

leanpkg.toml

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

src/algebra/ordered_monoid.lean

@@ -176,14 +176,14 @@ linear_order.lift coe units.ext
 @[simp, norm_cast, to_additive]
 theorem max_coe [monoid α] [linear_order α] {a b : units α} :
   (↑(max a b) : α) = max a b :=
-by by_cases b ≤ a; simp [max, h]
+by by_cases b ≤ a; simp [max_def, h]
 
 attribute [norm_cast] add_units.max_coe
 
 @[simp, norm_cast, to_additive]
 theorem min_coe [monoid α] [linear_order α] {a b : units α} :
   (↑(min a b) : α) = min a b :=
-by by_cases a ≤ b; simp [min, h]
+by by_cases a ≤ b; simp [min_def, h]
 
 attribute [norm_cast] add_units.min_coe
 

src/data/bool.lean

@@ -150,8 +150,6 @@ lemma bxor_iff_ne : ∀ {x y : bool}, bxor x y = tt ↔ x ≠ y := dec_trivial
 
 lemma bnot_inj : ∀ {a b : bool}, !a = !b → a = b := dec_trivial
 
-end bool
-
 instance : linear_order bool :=
 { le := λ a b, a = ff ∨ b = tt,
   le_refl := dec_trivial,
@@ -160,9 +158,11 @@ instance : linear_order bool :=
   le_total := dec_trivial,
   decidable_le := infer_instance,
   decidable_eq := infer_instance,
-  decidable_lt := infer_instance }
-
-namespace bool
+  decidable_lt := infer_instance,
+  max := bor,
+  max_def := by { funext x y, revert x y, exact dec_trivial },
+  min := band,
+  min_def := by { funext x y, revert x y, exact dec_trivial } }
 
 @[simp] lemma ff_le {x : bool} : ff ≤ x := or.intro_left _ rfl
 

src/data/finsupp/lattice.lean

@@ -37,10 +37,7 @@ lemma support_inf {f g : α →₀ γ} : (f ⊓ g).support = f.support ∩ g.sup
 begin
   ext, simp only [inf_apply, mem_support_iff,  ne.def,
     finset.mem_union, finset.mem_filter, finset.mem_inter],
-  rw [← decidable.not_or_iff_and_not, ← not_congr],
-  rw inf_eq_min, unfold min, split_ifs;
-  { try {apply or_iff_left_of_imp}, try {apply or_iff_right_of_imp}, intro con, rw con at h,
-    revert h, simp, }
+  simp only [inf_eq_min, ← nonpos_iff_eq_zero, min_le_iff, not_or_distrib]
 end
 
 instance [semilattice_sup β] : semilattice_sup (α →₀ β) :=

src/data/list/func.lean

@@ -83,7 +83,7 @@ def sub {α : Type u} [has_zero α] [has_sub α] : list α → list α → list
 /- set -/
 
 lemma length_set : ∀ {m : ℕ} {as : list α},
-  (as {m ↦ a}).length = _root_.max as.length (m+1)
+  (as {m ↦ a}).length = max as.length (m+1)
 | 0 []          := rfl
 | 0 (a::as)     := by {rw max_eq_left, refl, simp [nat.le_add_right]}
 | (m+1) []      := by simp only [set, nat.zero_max, length, @length_set m]
@@ -278,7 +278,7 @@ lemma get_pointwise [inhabited γ] {f : α → β → γ} (h1 : f (default α) (
 
 lemma length_pointwise {f : α → β → γ} :
   ∀ {as : list α} {bs : list β},
-  (pointwise f as bs).length = _root_.max as.length bs.length
+  (pointwise f as bs).length = max as.length bs.length
 | []      []      := rfl
 | []      (b::bs) :=
   by simp only [pointwise, length, length_map,
@@ -301,7 +301,7 @@ by {apply get_pointwise, apply zero_add}
 
 @[simp] lemma length_add {α : Type u}
   [has_zero α] [has_add α] {xs ys : list α} :
-  (add xs ys).length = _root_.max xs.length ys.length :=
+  (add xs ys).length = max xs.length ys.length :=
 @length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
 
 @[simp] lemma nil_add {α : Type u} [add_monoid α]
@@ -349,7 +349,7 @@ end
 by {apply get_pointwise, apply sub_zero}
 
 @[simp] lemma length_sub [has_zero α] [has_sub α] {xs ys : list α} :
-  (sub xs ys).length = _root_.max xs.length ys.length :=
+  (sub xs ys).length = max xs.length ys.length :=
 @length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
 
 @[simp] lemma nil_sub {α : Type} [add_group α]

src/data/list/intervals.lean

@@ -160,7 +160,7 @@ begin
   { rw [eq_nil_of_le hml, filter_le_of_top_le hml] }
 end
 
-@[simp] lemma filter_le (n m l : ℕ) : (Ico n m).filter (λ x, l ≤ x) = Ico (_root_.max n l) m :=
+@[simp] lemma filter_le (n m l : ℕ) : (Ico n m).filter (λ x, l ≤ x) = Ico (max n l) m :=
 begin
   cases le_total n l with hnl hln,
   { rw [max_eq_right hnl, filter_le_of_le hnl] },

src/data/list/min_max.lean

@@ -242,7 +242,7 @@ begin
   { rw [max_eq_left], refl, exact bot_le },
   change (coe : α → with_bot α) with some,
   rw [max_comm],
-  simp [max]
+  simp [max_def]
 end
 
 theorem minimum_concat (a : α) (l : list α) : minimum (l ++ [a]) = min (minimum l) a :=

src/data/nat/cast.lean

@@ -204,11 +204,11 @@ end
 
 @[simp, norm_cast] theorem cast_min [linear_ordered_semiring α] {a b : ℕ} :
   (↑(min a b) : α) = min a b :=
-by by_cases a ≤ b; simp [h, min]
+(@mono_cast α _).map_min
 
 @[simp, norm_cast] theorem cast_max [linear_ordered_semiring α] {a b : ℕ} :
   (↑(max a b) : α) = max a b :=
-by by_cases a ≤ b; simp [h, max]
+(@mono_cast α _).map_max
 
 @[simp, norm_cast] theorem abs_cast [linear_ordered_ring α] (a : ℕ) :
   abs (a : α) = a :=

src/data/polynomial/degree/definitions.lean

@@ -442,9 +442,8 @@ lemma degree_le_zero_iff : degree p ≤ 0 ↔ p = C (coeff p 0) :=
 
 lemma degree_add_le (p q : polynomial R) : degree (p + q) ≤ max (degree p) (degree q) :=
 calc degree (p + q) = ((p + q).support).sup some : rfl
-  ... ≤ (p.support ∪ q.support).sup some : by convert sup_mono support_add
-  ... = p.support.sup some ⊔ q.support.sup some : by convert sup_union
-  ... = _ : with_bot.sup_eq_max _ _
+  ... ≤ (p.support ∪ q.support).sup some : sup_mono support_add
+  ... = p.support.sup some ⊔ q.support.sup some : sup_union
 
 lemma nat_degree_add_le (p q : polynomial R) :
   nat_degree (p + q) ≤ max (nat_degree p) (nat_degree q) :=
@@ -525,7 +524,7 @@ finset.induction_on s (by simp only [sum_empty, sup_empty, degree_zero, le_refl]
   assume a s has ih,
   calc degree (∑ i in insert a s, f i) ≤ max (degree (f a)) (degree (∑ i in s, f i)) :
     by rw sum_insert has; exact degree_add_le _ _
-  ... ≤ _ : by rw [sup_insert, with_bot.sup_eq_max]; exact max_le_max (le_refl _) ih
+  ... ≤ _ : by rw [sup_insert, sup_eq_max]; exact max_le_max le_rfl ih
 
 lemma degree_mul_le (p q : polynomial R) : degree (p * q) ≤ degree p + degree q :=
 calc degree (p * q) ≤ (p.support).sup (λi, degree (sum q (λj a, C (coeff p i * a) * X ^ (i + j)))) :
@@ -851,8 +850,7 @@ begin
   haveI : is_associative (with_bot ℕ) max := ⟨max_assoc⟩,
   calc  (∑ i, C (f i) * X ^ (i : ℕ)).degree
       ≤ finset.univ.fold (⊔) ⊥ (λ i, (C (f i) * X ^ (i : ℕ)).degree) : degree_sum_le _ _
-  ... = finset.univ.fold max ⊥ (λ i, (C (f i) * X ^ (i : ℕ)).degree) :
-    (@finset.fold_hom _ _ _ (⊔) _ _ _ ⊥ finset.univ _ _ _ id (with_bot.sup_eq_max)).symm
+  ... = finset.univ.fold max ⊥ (λ i, (C (f i) * X ^ (i : ℕ)).degree) : rfl
   ... < n : (finset.fold_max_lt (n : with_bot ℕ)).mpr ⟨with_bot.bot_lt_coe _, _⟩,
 
   rintros ⟨i, hi⟩ -,

src/data/rat/cast.lean

@@ -230,11 +230,11 @@ by rw [← cast_zero, cast_lt]
 
 @[simp, norm_cast] theorem cast_min [linear_ordered_field α] {a b : ℚ} :
   (↑(min a b) : α) = min a b :=
-by by_cases a ≤ b; simp [h, min]
+by by_cases a ≤ b; simp [h, min_def]
 
 @[simp, norm_cast] theorem cast_max [linear_ordered_field α] {a b : ℚ} :
   (↑(max a b) : α) = max a b :=
-by by_cases b ≤ a; simp [h, max]
+by by_cases b ≤ a; simp [h, max_def]
 
 @[simp, norm_cast] theorem cast_abs [linear_ordered_field α] {q : ℚ} :
   ((abs q : ℚ) : α) = abs q :=