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>

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

src/data/real/nnreal.lean

@@ -397,11 +397,11 @@ by simp only [div_eq_inv_mul, mul_finset_sup]
 
 @[simp, norm_cast] lemma coe_max (x y : ℝ≥0) :
   ((max x y : ℝ≥0) : ℝ) = max (x : ℝ) (y : ℝ) :=
-by { delta max, split_ifs; refl }
+nnreal.coe_mono.map_max
 
 @[simp, norm_cast] lemma coe_min (x y : ℝ≥0) :
   ((min x y : ℝ≥0) : ℝ) = min (x : ℝ) (y : ℝ) :=
-by { delta min, split_ifs; refl }
+nnreal.coe_mono.map_min
 
 @[simp] lemma zero_le_coe {q : ℝ≥0} : 0 ≤ (q : ℝ) := q.2
 

src/data/string/basic.lean

@@ -92,13 +92,15 @@ begin
 end
 
 instance : linear_order string :=
-by refine_struct {
-    lt := (<), le := (≤),
-    decidable_lt := by apply_instance,
-    decidable_le := string.decidable_le,
-    decidable_eq := by apply_instance, .. };
-  { simp only [le_iff_to_list_le, lt_iff_to_list_lt, ← to_list_inj], introv,
-    apply_field }
+{ lt := (<), le := (≤),
+  decidable_lt := by apply_instance,
+  decidable_le := string.decidable_le,
+  decidable_eq := by apply_instance,
+  le_refl := λ a, le_iff_to_list_le.2 le_rfl,
+  le_trans := λ a b c, by { simp only [le_iff_to_list_le], exact λ h₁ h₂, h₁.trans h₂ },
+  le_total := λ a b, by { simp only [le_iff_to_list_le], exact le_total _ _ },
+  le_antisymm := λ a b, by { simp only [le_iff_to_list_le, ← to_list_inj], apply le_antisymm },
+  lt_iff_le_not_le := λ a b, by simp only [le_iff_to_list_le, lt_iff_to_list_lt, lt_iff_le_not_le] }
 
 end string
 

src/field_theory/separable.lean

@@ -445,7 +445,7 @@ lemma separable_prod_X_sub_C_iff' {ι : Sort*} {f : ι → F} {s : finset ι} :
 
 lemma separable_prod_X_sub_C_iff {ι : Sort*} [fintype ι] {f : ι → F} :
   (∏ i, (X - C (f i))).separable ↔ function.injective f :=
-separable_prod_X_sub_C_iff'.trans $ by simp_rw [mem_univ, true_implies_iff]
+separable_prod_X_sub_C_iff'.trans $ by simp_rw [mem_univ, true_implies_iff, function.injective]
 
 section splits
 

src/group_theory/order_of_element.lean

@@ -475,7 +475,8 @@ lemma exists_pow_eq_one (x : G) : is_of_fin_order x :=
 begin
   refine (is_of_fin_order_iff_pow_eq_one _).mpr _,
   obtain ⟨i, j, a_eq, ne⟩ : ∃(i j : ℕ), x ^ i = x ^ j ∧ i ≠ j :=
-    by simpa only [not_forall, exists_prop] using (not_injective_infinite_fintype (λi:ℕ, x^i)),
+    by simpa only [not_forall, exists_prop, injective]
+      using (not_injective_infinite_fintype (λi:ℕ, x^i)),
   wlog h'' : j ≤ i,
   refine ⟨i - j, nat.sub_pos_of_lt (lt_of_le_of_ne h'' ne.symm), mul_right_injective (x^j) _⟩,
   rw [mul_one, ← pow_add, ← a_eq, nat.add_sub_cancel' h''],

src/measure_theory/constructions/borel_space.lean

@@ -434,7 +434,7 @@ variables [second_countable_topology α]
 @[measurability]
 lemma measurable.max {f g : δ → α} (hf : measurable f) (hg : measurable g) :
   measurable (λ a, max (f a) (g a)) :=
-hf.piecewise (measurable_set_le hg hf) hg
+by simpa only [max_def] using hf.piecewise (measurable_set_le hg hf) hg
 
 @[measurability]
 lemma ae_measurable.max {f g : δ → α} {μ : measure δ}
@@ -445,7 +445,7 @@ lemma ae_measurable.max {f g : δ → α} {μ : measure δ}
 @[measurability]
 lemma measurable.min {f g : δ → α} (hf : measurable f) (hg : measurable g) :
   measurable (λ a, min (f a) (g a)) :=
-hf.piecewise (measurable_set_le hf hg) hg
+by simpa only [min_def] using hf.piecewise (measurable_set_le hf hg) hg
 
 @[measurability]
 lemma ae_measurable.min {f g : δ → α} {μ : measure δ}

src/measure_theory/measure/lebesgue.lean

@@ -313,16 +313,16 @@ begin
   have h₁ : (λ y, ennreal.of_real ((g - f) y))
           =ᵐ[μ.restrict s]
               λ y, ennreal.of_real ((ae_measurable.mk g hg - ae_measurable.mk f hf) y) :=
-    eventually_eq.fun_comp (eventually_eq.sub hg.ae_eq_mk hf.ae_eq_mk) _,
+    (hg.ae_eq_mk.sub hf.ae_eq_mk).fun_comp _,
   have h₂ : (μ.restrict s).prod volume (region_between f g s) =
     (μ.restrict s).prod volume (region_between (ae_measurable.mk f hf) (ae_measurable.mk g hg) s),
   { apply measure_congr,
-    apply eventually_eq.inter, { refl },
-    exact eventually_eq.inter
-            (eventually_eq.comp₂ (ae_eq_comp' measurable_fst hf.ae_eq_mk
-              measure.prod_fst_absolutely_continuous) _ eventually_eq.rfl)
-            (eventually_eq.comp₂ eventually_eq.rfl _
-              (ae_eq_comp' measurable_fst hg.ae_eq_mk measure.prod_fst_absolutely_continuous)) },
+    apply eventually_eq.rfl.inter,
+    exact
+      ((ae_eq_comp' measurable_fst hf.ae_eq_mk measure.prod_fst_absolutely_continuous).comp₂ _
+        eventually_eq.rfl).inter
+      (eventually_eq.rfl.comp₂ _
+        (ae_eq_comp' measurable_fst hg.ae_eq_mk measure.prod_fst_absolutely_continuous)) },
   rw [lintegral_congr_ae h₁,
       ← volume_region_between_eq_lintegral' hf.measurable_mk hg.measurable_mk hs],
   convert h₂ using 1,
@@ -341,11 +341,7 @@ theorem volume_region_between_eq_integral' [sigma_finite μ]
   μ.prod volume (region_between f g s) = ennreal.of_real (∫ y in s, (g - f) y ∂μ) :=
 begin
   have h : g - f =ᵐ[μ.restrict s] (λ x, real.to_nnreal (g x - f x)),
-  { apply hfg.mono,
-    simp only [real.to_nnreal, max, sub_nonneg, pi.sub_apply],
-    intros x hx,
-    split_ifs,
-    refl },
+    from hfg.mono (λ x hx, (real.coe_to_nnreal _ $ sub_nonneg.2 hx).symm),
   rw [volume_region_between_eq_lintegral f_int.ae_measurable g_int.ae_measurable hs,
     integral_congr_ae h, lintegral_congr_ae,
     lintegral_coe_eq_integral _ ((integrable_congr h).mp (g_int.sub f_int))],

src/number_theory/pell.lean

@@ -706,7 +706,7 @@ k = 0 ∧ m = 1 ∨ 0 < k ∧
   refine (nat.eq_zero_or_pos n).elim
     (λn0, by rw [n0, zero_pow kpos]; exact or.inl ⟨rfl, rfl⟩)
     (λnpos, or.inr ⟨npos, _⟩); exact
-  let w := _root_.max n k in
+  let w := max n k in
   have nw : n ≤ w, from le_max_left _ _,
   have kw : k ≤ w, from le_max_right _ _,
   have wpos : 0 < w, from lt_of_lt_of_le npos nw,

src/order/basic.lean

@@ -85,7 +85,15 @@ lemma partial_order.to_preorder_injective {α : Type*} :
 @[ext]
 lemma linear_order.to_partial_order_injective {α : Type*} :
   function.injective (@linear_order.to_partial_order α) :=
-λ A B h, by { cases A, cases B, injection h, congr' }
+begin
+  intros A B h,
+  cases A, cases B, injection h,
+  obtain rfl : A_le = B_le := ‹_›, obtain rfl : A_lt = B_lt := ‹_›,
+  obtain rfl : A_decidable_le = B_decidable_le := subsingleton.elim _ _,
+  obtain rfl : A_max = B_max := A_max_def.trans B_max_def.symm,
+  obtain rfl : A_min = B_min := A_min_def.trans B_min_def.symm,
+  congr
+end
 
 theorem preorder.ext {α} {A B : preorder α}
   (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y) : A = B :=
@@ -206,8 +214,12 @@ instance (α : Type*) [partial_order α] : partial_order (order_dual α) :=
 
 instance (α : Type*) [linear_order α] : linear_order (order_dual α) :=
 { le_total     := λ a b : α, le_total b a,
-  decidable_le := show decidable_rel (λ a b : α, b ≤ a), by apply_instance,
-  decidable_lt := show decidable_rel (λ a b : α, b < a), by apply_instance,
+  decidable_le := (infer_instance : decidable_rel (λ a b : α, b ≤ a)),
+  decidable_lt := (infer_instance : decidable_rel (λ a b : α, b < a)),
+  min := @max α _,
+  max := @min α _,
+  min_def := @linear_order.max_def α _,
+  max_def := @linear_order.min_def α _,
   .. order_dual.partial_order α }
 
 instance : Π [inhabited α], inhabited (order_dual α) := id