chore(tactic/reserved_notation): change precedence of sup and inf (#1…

…0623)

Put the precedence of `⊔` and `⊓` at 68 and 69 respectively, which is above `+` (65), `∑` and `∏` (67), and below `*` (70). This makes sure that inf and sup behave in the same way in expressions where arithmetic operations appear (which was not the case before).

Discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/inf.20and.20sup.20don't.20bind.20similarly



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

src/algebra/lattice_ordered_group.lean

@@ -108,10 +108,10 @@ by rw [← inv_inv (a⁻¹ ⊔ b⁻¹), inv_sup_eq_inv_inf_inv a⁻¹ b⁻¹, in
 -- Bourbaki A.VI.10 Prop 7
 -- a ⊓ b + (a ⊔ b) = a + b
 @[to_additive]
-lemma inf_mul_sup [covariant_class α α (*) (≤)] (a b : α) : a ⊓ b * (a ⊔ b) = a * b :=
-calc a ⊓ b * (a ⊔ b) = a ⊓ b * ((a * b) * (b⁻¹ ⊔ a⁻¹)) :
+lemma inf_mul_sup [covariant_class α α (*) (≤)] (a b : α) : (a ⊓ b) * (a ⊔ b) = a * b :=
+calc (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * ((a * b) * (b⁻¹ ⊔ a⁻¹)) :
   by { rw mul_sup b⁻¹ a⁻¹ (a * b), simp, }
-... = a ⊓ b * ((a * b) * (a ⊓ b)⁻¹) : by rw [inv_inf_eq_sup_inv, sup_comm]
+... = (a ⊓ b) * ((a * b) * (a ⊓ b)⁻¹) : by rw [inv_inf_eq_sup_inv, sup_comm]
 ... = a * b                       : by rw [mul_comm, inv_mul_cancel_right]
 
 namespace lattice_ordered_comm_group
@@ -372,8 +372,8 @@ theorem abs_div_sup_mul_abs_div_inf [covariant_class α α (*) (≤)] (a b c : 
   |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = |a / b| :=
 begin
   letI : distrib_lattice α := lattice_ordered_comm_group_to_distrib_lattice α,
-  calc |(a ⊔ c) / (b ⊔ c)| * |a ⊓ c / (b ⊓ c)| =
-    ((b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c))) * |a ⊓ c / (b ⊓ c)| : by rw sup_div_inf_eq_abs_div
+  calc |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| =
+    ((b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c))) * |(a ⊓ c) / (b ⊓ c)| : by rw sup_div_inf_eq_abs_div
   ... = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * (((b ⊓ c) ⊔ (a ⊓ c)) / ((b ⊓ c) ⊓ (a ⊓ c))) :
     by rw sup_div_inf_eq_abs_div (b ⊓ c) (a ⊓ c)
   ... = (b ⊔ a ⊔ c) / ((b ⊓ a) ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) : by
@@ -383,7 +383,7 @@ begin
     nth_rewrite 3 inf_comm,
     rw [inf_right_idem, inf_assoc], }
   ... = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) /(((b ⊓ a) ⊔ c) * (b ⊓ a ⊓ c)) : by rw div_mul_comm
-  ... = (b ⊔ a) * c / (b ⊓ a * c) :
+  ... = (b ⊔ a) * c / ((b ⊓ a) * c) :
     by rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
   ... = (b ⊔ a) / (b ⊓ a) : by rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left,
       ← div_eq_mul_inv]

src/tactic/reserved_notation.lean

@@ -51,8 +51,10 @@ precedence `?`:max
 precedence `fixing`:0
 
 -- used in `order/lattice.lean`
-reserve infixl ` ⊓ `:70
-reserve infixl ` ⊔ `:65
+-- These priorities are chosen to be above `+`, `∑`, and `∏`, but below `*`. There is no particular
+-- reason for this choice.
+reserve infixl ` ⊓ `:69
+reserve infixl ` ⊔ `:68
 
 -- used in `algebra/module/linear_map.lean`
 reserve infix ` ≃ₗ `:25