From acb58e8a87d5e450aea2bf36b8d99c8951ff092c Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sat, 3 Dec 2016 12:05:19 -0500
Subject: [PATCH] feat(library/init/algebra/group,ring): alternative names for
 calculation lemmas

---
 library/init/algebra/group.lean | 9 +++++++++
 library/init/algebra/ring.lean  | 8 ++++++++
 2 files changed, 17 insertions(+)

diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean
index 39922a7b16..1bea68d0b4 100644
--- a/library/init/algebra/group.lean
+++ b/library/init/algebra/group.lean
@@ -59,6 +59,8 @@ monoid.mul_one
 @[simp] lemma mul_left_inv [group α] : ∀ a : α, a⁻¹ * a = 1 :=
 group.mul_left_inv
 
+def inv_mul_self := @mul_left_inv
+
 @[simp] lemma inv_mul_cancel_left [group α] (a b : α) : a⁻¹ * (a * b) = b :=
 by rw [-mul_assoc, mul_left_inv, one_mul]
 
@@ -78,6 +80,8 @@ inv_eq_of_mul_eq_one (mul_left_inv a)
 have a⁻¹⁻¹ * a⁻¹ = 1, by rw mul_left_inv,
 by rwa [inv_inv] at this
 
+def mul_inv_self := @mul_right_inv
+
 lemma inv_inj [group α] {a b : α} (h : a⁻¹ = b⁻¹) : a = b :=
 have a = a⁻¹⁻¹, by simp,
 begin rw this, simp [h] end
@@ -274,6 +278,11 @@ run_command transport_to_additive `eq_mul_of_inv_mul_eq `eq_add_of_neg_add_eq
 run_command transport_to_additive `mul_eq_of_eq_inv_mul `add_eq_of_eq_neg_add
 run_command transport_to_additive `mul_eq_of_eq_mul_inv `add_eq_of_eq_add_neg
 
+def neg_add_self := @add_left_neg
+def add_neg_self := @add_right_neg
+def eq_of_add_eq_add_left := @add_left_cancel
+def eq_of_add_eq_add_right := @add_right_cancel
+
 @[reducible] protected def algebra.sub [add_group α] (a b : α) : α :=
 a + -b
 
diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean
index f715952b4a..af34352d74 100644
--- a/library/init/algebra/ring.lean
+++ b/library/init/algebra/ring.lean
@@ -21,9 +21,13 @@ variable {α : Type u}
 lemma left_distrib [distrib α] (a b c : α) : a * (b + c) = a * b + a * c :=
 distrib.left_distrib a b c
 
+def mul_add := @left_distrib
+
 lemma right_distrib [distrib α] (a b c : α) : (a + b) * c = a * c + b * c :=
 distrib.right_distrib a b c
 
+def add_mul := @right_distrib
+
 class mul_zero_class (α : Type u) extends has_mul α, has_zero α :=
 (zero_mul : ∀ a : α, 0 * a = 0)
 (mul_zero : ∀ a : α, a * 0 = 0)
@@ -141,11 +145,15 @@ calc
    a * (b - c) = a * b + a * -c : left_distrib a b (-c)
            ... = a * b - a * c  : by simp
 
+def mul_sub := @mul_sub_left_distrib
+
 lemma mul_sub_right_distrib [s : ring α] (a b c : α) : (a - b) * c = a * c - b * c :=
 calc
   (a - b) * c = a * c  + -b * c : right_distrib a (-b) c
           ... = a * c - b * c   : by simp
 
+def sub_mul := @mul_sub_right_distrib
+
 class comm_ring (α : Type u) extends ring α, comm_semigroup α
 
 instance comm_ring.to_comm_semiring [s : comm_ring α] : comm_semiring α :=