refactor(library/init/reserved_notation): increase binding strength of ^-1 to max+10

library/algebra/category/constructions.lean

@@ -82,17 +82,17 @@ namespace category
     context
     local attribute discrete_category [instance]
     include H
-    theorem dicrete_category.endomorphism {a b : A} (f : a ⟶ b) : a = b :=
+    theorem discrete_category.endomorphism {a b : A} (f : a ⟶ b) : a = b :=
     decidable.rec_on (H a b) (λh f, h) (λh f, empty.rec _ f) f
 
-    theorem dicrete_category.discrete {a b : A} (f : a ⟶ b)
-      : eq.rec_on (dicrete_category.endomorphism f) f = (ID b) :=
+    theorem discrete_category.discrete {a b : A} (f : a ⟶ b)
+      : eq.rec_on (discrete_category.endomorphism f) f = (ID b) :=
     @subsingleton.elim _ !set_hom_subsingleton _ _
 
     definition discrete_category.rec_on {P : Πa b, a ⟶ b → Type} {a b : A} (f : a ⟶ b)
         (H : ∀a, P a a id) : P a b f :=
-    cast (dcongr_arg3 P rfl (dicrete_category.endomorphism f⁻¹)
-                            (@subsingleton.elim _ !set_hom_subsingleton _ _) ⁻¹) (H a)
+    cast (dcongr_arg3 P rfl (discrete_category.endomorphism f)⁻¹
+                            (@subsingleton.elim _ !set_hom_subsingleton _ _))⁻¹ (H a)
     end
   end
   section
@@ -241,7 +241,7 @@ namespace category
   functor.mk (λ a, sigma.mk (to_ob a) (h ∘ ob_hom a))
              (λ a b f, sigma.mk (hom_hom f)
        (calc
-         (h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : assoc h (ob_hom b) (hom_hom f)⁻¹
+         (h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : (assoc h (ob_hom b) (hom_hom f))⁻¹
            ... = h ∘ ob_hom a : congr_arg (λx, h ∘ x) (commute f)))
              (λ a, rfl)
              (λ a b c g f, dpair_eq rfl !proof_irrel)

library/algebra/category/morphism.lean

@@ -96,7 +96,7 @@ namespace morphism
   theorem section_of_id : section_of (ID a) = id :=
   section_eq_intro !id_compose
 
-  theorem iso_of_id : ID a⁻¹ = id :=
+  theorem iso_of_id : (ID a)⁻¹ = id :=
   inverse_eq_intro_left !id_compose
 
   theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g]
@@ -215,17 +215,17 @@ namespace morphism
       ... = g : id_left g
   theorem compose_pp_V : (r ∘ q) ∘ q⁻¹ = r :=
   calc
-    (r ∘ q) ∘ q⁻¹ = r ∘ q ∘ q⁻¹ : assoc r q (q⁻¹)⁻¹
+    (r ∘ q) ∘ q⁻¹ = r ∘ q ∘ q⁻¹ : (assoc r q (q⁻¹))⁻¹
       ... = r ∘ id : {compose_inverse q}
       ... = r : id_right r
   theorem compose_pV_p : (f ∘ q⁻¹) ∘ q = f :=
   calc
-    (f ∘ q⁻¹) ∘ q = f ∘ q⁻¹ ∘ q : assoc f (q⁻¹) q⁻¹
+    (f ∘ q⁻¹) ∘ q = f ∘ q⁻¹ ∘ q : (assoc f (q⁻¹) q)⁻¹
       ... = f ∘ id : {inverse_compose q}
       ... = f : id_right f
 
   theorem inv_pp [H' : is_iso p] : (q ∘ p)⁻¹ = p⁻¹ ∘ q⁻¹ :=
-  have H1 : (p⁻¹ ∘ q⁻¹) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)), from assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹,
+  have H1 : (p⁻¹ ∘ q⁻¹) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)), from (assoc (p⁻¹) (q⁻¹) (q ∘ p))⁻¹,
   have H2 : (p⁻¹) ∘ (q⁻¹ ∘ (q ∘ p)) = p⁻¹ ∘ p, from congr_arg _ (compose_V_pp q p),
   have H3 : p⁻¹ ∘ p = id, from inverse_compose p,
   inverse_eq_intro_left (H1 ⬝ H2 ⬝ H3)
@@ -253,18 +253,18 @@ namespace morphism
   theorem moveR_pM (H : w = f ∘ q⁻¹) : w ∘ q = f := H⁻¹ ▸ compose_pV_p f q
   theorem moveR_Vp (H : z = q ∘ p) : q⁻¹ ∘ z = p := H⁻¹ ▸ compose_V_pp q p
   theorem moveR_pV (H : x = r ∘ q) : x ∘ q⁻¹ = r := H⁻¹ ▸ compose_pp_V r q
-  theorem moveL_Mp (H : q⁻¹ ∘ g = y) : g = q ∘ y := moveR_Mp (H⁻¹)⁻¹
-  theorem moveL_pM (H : f ∘ q⁻¹ = w) : f = w ∘ q := moveR_pM (H⁻¹)⁻¹
-  theorem moveL_Vp (H : q ∘ p = z) : p = q⁻¹ ∘ z := moveR_Vp (H⁻¹)⁻¹
-  theorem moveL_pV (H : r ∘ q = x) : r = x ∘ q⁻¹ := moveR_pV (H⁻¹)⁻¹
-  theorem moveL_1V (H : h ∘ q = id) : h = q⁻¹ := inverse_eq_intro_left H⁻¹
-  theorem moveL_V1 (H : q ∘ h = id) : h = q⁻¹ := inverse_eq_intro_right H⁻¹
+  theorem moveL_Mp (H : q⁻¹ ∘ g = y) : g = q ∘ y := (moveR_Mp (H⁻¹))⁻¹
+  theorem moveL_pM (H : f ∘ q⁻¹ = w) : f = w ∘ q := (moveR_pM (H⁻¹))⁻¹
+  theorem moveL_Vp (H : q ∘ p = z) : p = q⁻¹ ∘ z := (moveR_Vp (H⁻¹))⁻¹
+  theorem moveL_pV (H : r ∘ q = x) : r = x ∘ q⁻¹ := (moveR_pV (H⁻¹))⁻¹
+  theorem moveL_1V (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_intro_left H)⁻¹
+  theorem moveL_V1 (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_intro_right H)⁻¹
   theorem moveL_1M (H : i ∘ q⁻¹ = id) : i = q := moveL_1V H ⬝ inverse_involutive q
   theorem moveL_M1 (H : q⁻¹ ∘ i = id) : i = q := moveL_V1 H ⬝ inverse_involutive q
-  theorem moveR_1M (H : id = i ∘ q⁻¹) : q = i := moveL_1M (H⁻¹)⁻¹
-  theorem moveR_M1 (H : id = q⁻¹ ∘ i) : q = i := moveL_M1 (H⁻¹)⁻¹
-  theorem moveR_1V (H : id = h ∘ q) : q⁻¹ = h := moveL_1V (H⁻¹)⁻¹
-  theorem moveR_V1 (H : id = q ∘ h) : q⁻¹ = h := moveL_V1 (H⁻¹)⁻¹
+  theorem moveR_1M (H : id = i ∘ q⁻¹) : q = i := (moveL_1M (H⁻¹))⁻¹
+  theorem moveR_M1 (H : id = q⁻¹ ∘ i) : q = i := (moveL_M1 (H⁻¹))⁻¹
+  theorem moveR_1V (H : id = h ∘ q) : q⁻¹ = h := (moveL_1V (H⁻¹))⁻¹
+  theorem moveR_V1 (H : id = q ∘ h) : q⁻¹ = h := (moveL_V1 (H⁻¹))⁻¹
   end
   end iso
 

library/data/nat/sub.lean

@@ -241,9 +241,9 @@ theorem sub_sub.cases {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m +
   (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) :=
 or.elim !le.total
   (assume H3 : n ≤ m,
-    sub_eq_zero_of_le H3⁻¹ ▸  (H2 (m - n) (add_sub_of_le H3⁻¹)))
+    (sub_eq_zero_of_le H3)⁻¹ ▸  (H2 (m - n) (add_sub_of_le H3)⁻¹))
   (assume H3 : m ≤ n,
-    sub_eq_zero_of_le H3⁻¹ ▸ (H1 (n - m) (add_sub_of_le H3⁻¹)))
+    (sub_eq_zero_of_le H3)⁻¹ ▸ (H1 (n - m) (add_sub_of_le H3)⁻¹))
 
 theorem sub_eq_of_add_eq {n m k : ℕ} (H : n + m = k) : k - n = m :=
 have H2 : k - n + n = m + n, from

library/init/reserved_notation.lean

@@ -20,11 +20,20 @@ notation `take`   binders `,` r:(scoped f, f) := r
   When hovering over a symbol, use "C-u C-x =" to see how to input it.
 -/
 
-/- Logical operations and relations -/
-
-definition std.prec.max   : num := 1024 -- reflects max precedence used internally
+definition std.prec.max   : num := 1024 -- the strength of application, identifiers, (, [, etc.
 definition std.prec.arrow : num := 25
 
+/-
+The next definition is "max + 10". It can be used e.g. for postfix operations that should
+be stronger than application.
+-/
+
+definition std.prec.max_plus :=
+num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ
+  (num.succ std.prec.max)))))))))
+
+/- Logical operations and relations -/
+
 reserve prefix `¬`:40
 reserve prefix `~`:40
 reserve infixr `∧`:35
@@ -38,8 +47,9 @@ reserve infix `≠`:50
 reserve infix `≈`:50
 reserve infix `∼`:50
 
-reserve infixr `∘`:60      -- input with \comp
-reserve postfix `⁻¹`:100  --input with \sy or \-1 or \inv
+reserve infixr `∘`:60                   -- input with \comp
+reserve postfix `⁻¹`:std.prec.max_plus  -- input with \sy or \-1 or \inv
+
 reserve infixl `⬝`:75
 reserve infixr `▸`:75
 

library/logic/eq.lean

@@ -29,7 +29,7 @@ namespace eq
   drec_on H rfl
 
   theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : rec_on H₁ b = rec_on H₂ b :=
-  rec_on_constant H₁ b ⬝ rec_on_constant H₂ b⁻¹
+  rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹
 
   theorem rec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) :
                        rec_on H b = rec_on H' b :=