From a607e7dd573b73e3dfa3d1e2ef01027417285b0c Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Wed, 25 Feb 2015 13:32:19 -0500
Subject: [PATCH] feat(library/algebra/group): add rules for sub equalities

---
 library/algebra/group.lean  | 61 +++++++++++++++++++++++++------------
 library/data/int/basic.lean | 24 ++++++++++-----
 2 files changed, 57 insertions(+), 28 deletions(-)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index f7f536969..c8591a4ef 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -208,29 +208,28 @@ section group
       ... = 1 * b : H
       ... = b : one_mul
 
-  -- TODO: better names for the next eight theorems? (Also for additive ones.)
-  theorem eq_mul_inv_of_mul_eq {a b c : A} (H : a * b = c) : a = c * b⁻¹ :=
+  theorem eq_mul_inv_of_mul_eq {a b c : A} (H : a * c = b) : a = b * c⁻¹ :=
   H ▸ !mul_inv_cancel_right⁻¹
 
-  theorem eq_inv_mul_of_mul_eq {a b c : A} (H : a * b = c) : b = a⁻¹ * c :=
+  theorem eq_inv_mul_of_mul_eq {a b c : A} (H : b * a = c) : a = b⁻¹ * c :=
   H ▸ !inv_mul_cancel_left⁻¹
 
-  theorem inv_mul_eq_of_eq_mul {a b c : A} (H : a = b * c) : b⁻¹ * a = c :=
+  theorem inv_mul_eq_of_eq_mul {a b c : A} (H : b = a * c) : a⁻¹ * b = c :=
   H⁻¹ ▸ !inv_mul_cancel_left
 
-  theorem mul_inv_eq_of_eq_mul {a b c : A} (H : a = b * c) : a * c⁻¹ = b :=
+  theorem mul_inv_eq_of_eq_mul {a b c : A} (H : a = c * b) : a * b⁻¹ = c :=
   H⁻¹ ▸ !mul_inv_cancel_right
 
-  theorem eq_mul_of_mul_inv_eq {a b c : A} (H : a * b⁻¹ = c) : a = c * b :=
+  theorem eq_mul_of_mul_inv_eq {a b c : A} (H : a * c⁻¹ = b) : a = b * c :=
   !inv_inv ▸ (eq_mul_inv_of_mul_eq H)
 
-  theorem eq_mul_of_inv_mul_eq {a b c : A} (H : a⁻¹ * b = c) : b = a * c :=
+  theorem eq_mul_of_inv_mul_eq {a b c : A} (H : b⁻¹ * a = c) : a = b * c :=
   !inv_inv ▸ (eq_inv_mul_of_mul_eq H)
 
-  theorem mul_eq_of_eq_inv_mul {a b c : A} (H : a = b⁻¹ * c) : b * a = c :=
+  theorem mul_eq_of_eq_inv_mul {a b c : A} (H : b = a⁻¹ * c) : a * b = c :=
   !inv_inv ▸ (inv_mul_eq_of_eq_mul H)
 
-  theorem mul_eq_of_eq_mul_inv {a b c : A} (H : a = b * c⁻¹) : a * c = b :=
+  theorem mul_eq_of_eq_mul_inv {a b c : A} (H : a = c * b⁻¹) : a * b = c :=
   !inv_inv ▸ (mul_inv_eq_of_eq_mul H)
 
   theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
@@ -316,28 +315,29 @@ section add_group
       rewrite ⟨add.assoc, add_neg_cancel_left, add.right_inv⟩
     end
 
-  theorem eq_add_neg_of_add_eq {a b c : A} (H : a + b = c) : a = c + -b :=
+  -- TODO: delete these in favor of sub rules?
+  theorem eq_add_neg_of_add_eq {a b c : A} (H : a + c = b) : a = b + -c :=
   H ▸ !add_neg_cancel_right⁻¹
 
-  theorem eq_neg_add_of_add_eq {a b c : A} (H : a + b = c) : b = -a + c :=
+  theorem eq_neg_add_of_add_eq {a b c : A} (H : b + a = c) : a = -b + c :=
   H ▸ !neg_add_cancel_left⁻¹
 
-  theorem neg_add_eq_of_eq_add {a b c : A} (H : a = b + c) : -b + a = c :=
+  theorem neg_add_eq_of_eq_add {a b c : A} (H : b = a + c) : -a + b = c :=
   H⁻¹ ▸ !neg_add_cancel_left
 
-  theorem add_neg_eq_of_eq_add {a b c : A} (H : a = b + c) : a + -c = b :=
+  theorem add_neg_eq_of_eq_add {a b c : A} (H : a = c + b) : a + -b = c :=
   H⁻¹ ▸ !add_neg_cancel_right
 
-  theorem eq_add_of_add_neg_eq {a b c : A} (H : a + -b = c) : a = c + b :=
+  theorem eq_add_of_add_neg_eq {a b c : A} (H : a + -c = b) : a = b + c :=
   !neg_neg ▸ (eq_add_neg_of_add_eq H)
 
-  theorem eq_add_of_neg_add_eq {a b c : A} (H : -a + b = c) : b = a + c :=
+  theorem eq_add_of_neg_add_eq {a b c : A} (H : -b + a = c) : a = b + c :=
   !neg_neg ▸ (eq_neg_add_of_add_eq H)
 
-  theorem add_eq_of_eq_neg_add {a b c : A} (H : a = -b + c) : b + a = c :=
+  theorem add_eq_of_eq_neg_add {a b c : A} (H : b = -a + c) : a + b = c :=
   !neg_neg ▸ (neg_add_eq_of_eq_add H)
 
-  theorem add_eq_of_eq_add_neg {a b c : A} (H : a = b + -c) : a + c = b :=
+  theorem add_eq_of_eq_add_neg {a b c : A} (H : a = c + -b) : a + b = c :=
   !neg_neg ▸ (add_neg_eq_of_eq_add H)
 
   theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
@@ -420,14 +420,24 @@ section add_group
       ... ↔ c - d = 0 : H ▸ !iff.refl
       ... ↔ c = d : iff.symm (eq_iff_sub_eq_zero c d)
 
+  theorem eq_sub_of_add_eq {a b c : A} (H : a + c = b) : a = b - c :=
+  !eq_add_neg_of_add_eq H
+
+  theorem sub_eq_of_eq_add {a b c : A} (H : a = c + b) : a - b = c :=
+  !add_neg_eq_of_eq_add H
+
+  theorem eq_add_of_sub_eq {a b c : A} (H : a - c = b) : a = b + c :=
+  eq_add_of_add_neg_eq H
+
+  theorem add_eq_of_eq_sub {a b c : A} (H : a = c - b) : a + b = c :=
+  add_eq_of_eq_add_neg H
 end add_group
 
 structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A
 
 section add_comm_group
-
-variable [s : add_comm_group A]
-include s
+  variable [s : add_comm_group A]
+  include s
 
   theorem sub_add_eq_sub_sub (a b c : A) : a - (b + c) = a - b - c :=
   !add.comm ▸ !sub_add_eq_sub_sub_swap
@@ -444,6 +454,17 @@ include s
   theorem add_sub_add_left_eq_sub (a b c : A) : (c + a) - (c + b) = a - b :=
   by rewrite ⟨sub_add_eq_sub_sub, (add.comm c a), add_sub_cancel⟩
 
+  theorem eq_sub_of_add_eq' {a b c : A} (H : c + a = b) : a = b - c :=
+  !eq_sub_of_add_eq (!add.comm ▸ H)
+
+  theorem sub_eq_of_eq_add' {a b c : A} (H : a = b + c) : a - b = c :=
+  !sub_eq_of_eq_add (!add.comm ▸ H)
+
+  theorem eq_add_of_sub_eq' {a b c : A} (H : a - b = c) : a = b + c :=
+  !add.comm ▸ eq_add_of_sub_eq H
+
+  theorem add_eq_of_eq_sub' {a b c : A} (H : b = c - a) : a + b = c :=
+  !add.comm ▸ add_eq_of_eq_sub H
 end add_comm_group
 
 /- bundled structures -/
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index baf8f658d..e919a593e 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -656,21 +656,21 @@ section port_algebra
   theorem add_neg_cancel_left : ∀a b : ℤ, a + (-a + b) = b := algebra.add_neg_cancel_left
   theorem add_neg_cancel_right : ∀a b : ℤ, a + b + -b = a := algebra.add_neg_cancel_right
   theorem neg_add_rev : ∀a b : ℤ, -(a + b) = -b + -a := algebra.neg_add_rev
-  theorem eq_add_neg_of_add_eq : ∀{a b c : ℤ}, a + b = c → a = c + -b :=
+  theorem eq_add_neg_of_add_eq : ∀{a b c : ℤ}, a + c = b → a = b + -c :=
     @algebra.eq_add_neg_of_add_eq _ _
-  theorem eq_neg_add_of_add_eq : ∀{a b c : ℤ}, a + b = c → b = -a + c :=
+  theorem eq_neg_add_of_add_eq : ∀{a b c : ℤ}, b + a = c → a = -b + c :=
     @algebra.eq_neg_add_of_add_eq _ _
-  theorem neg_add_eq_of_eq_add : ∀{a b c : ℤ}, a = b + c → -b + a = c :=
+  theorem neg_add_eq_of_eq_add : ∀{a b c : ℤ}, b = a + c → -a + b = c :=
     @algebra.neg_add_eq_of_eq_add _ _
-  theorem add_neg_eq_of_eq_add : ∀{a b c : ℤ}, a = b + c → a + -c = b :=
+  theorem add_neg_eq_of_eq_add : ∀{a b c : ℤ}, a = c + b → a + -b = c :=
     @algebra.add_neg_eq_of_eq_add _ _
-  theorem eq_add_of_add_neg_eq : ∀{a b c : ℤ}, a + -b = c → a = c + b :=
+  theorem eq_add_of_add_neg_eq : ∀{a b c : ℤ}, a + -c = b → a = b + c :=
     @algebra.eq_add_of_add_neg_eq _ _
-  theorem eq_add_of_neg_add_eq : ∀{a b c : ℤ}, -a + b = c → b = a + c :=
+  theorem eq_add_of_neg_add_eq : ∀{a b c : ℤ}, -b + a = c → a = b + c :=
     @algebra.eq_add_of_neg_add_eq _ _
-  theorem add_eq_of_eq_neg_add : ∀{a b c : ℤ}, a = -b + c → b + a = c :=
+  theorem add_eq_of_eq_neg_add : ∀{a b c : ℤ}, b = -a + c → a + b = c :=
     @algebra.add_eq_of_eq_neg_add _ _
-  theorem add_eq_of_eq_add_neg : ∀{a b c : ℤ}, a = b + -c → a + c = b :=
+  theorem add_eq_of_eq_add_neg : ∀{a b c : ℤ}, a = c + -b → a + b = c :=
     @algebra.add_eq_of_eq_add_neg _ _
   theorem add_eq_iff_eq_neg_add : ∀a b c : ℤ, a + b = c ↔ b = -a + c :=
     @algebra.add_eq_iff_eq_neg_add _ _
@@ -694,6 +694,10 @@ section port_algebra
   theorem eq_sub_iff_add_eq : ∀a b c : ℤ, a = b - c ↔ a + c = b := algebra.eq_sub_iff_add_eq
   theorem eq_iff_eq_of_sub_eq_sub : ∀{a b c d : ℤ}, a - b = c - d → a = b ↔ c = d :=
     @algebra.eq_iff_eq_of_sub_eq_sub _ _
+  theorem eq_sub_of_add_eq : ∀{a b c : ℤ}, a + c = b → a = b - c := @algebra.eq_sub_of_add_eq _ _
+  theorem sub_eq_of_eq_add : ∀{a b c : ℤ}, a = c + b → a - b = c := @algebra.sub_eq_of_eq_add _ _
+  theorem eq_add_of_sub_eq : ∀{a b c : ℤ}, a - c = b → a = b + c := @algebra.eq_add_of_sub_eq _ _
+  theorem add_eq_of_eq_sub : ∀{a b c : ℤ}, a = c - b → a + b = c := @algebra.add_eq_of_eq_sub _ _
   theorem sub_add_eq_sub_sub : ∀a b c : ℤ, a - (b + c) = a - b - c := algebra.sub_add_eq_sub_sub
   theorem neg_add_eq_sub : ∀a b : ℤ, -a + b = b - a := algebra.neg_add_eq_sub
   theorem neg_add : ∀a b : ℤ, -(a + b) = -a + -b := algebra.neg_add
@@ -701,6 +705,10 @@ section port_algebra
   theorem sub_sub_ : ∀a b c : ℤ, a - b - c = a - (b + c) := algebra.sub_sub
   theorem add_sub_add_left_eq_sub : ∀a b c : ℤ, (c + a) - (c + b) = a - b :=
     algebra.add_sub_add_left_eq_sub
+  theorem eq_sub_of_add_eq' : ∀{a b c : ℤ}, c + a = b → a = b - c := @algebra.eq_sub_of_add_eq' _ _
+  theorem sub_eq_of_eq_add' : ∀{a b c : ℤ}, a = b + c → a - b = c := @algebra.sub_eq_of_eq_add' _ _
+  theorem eq_add_of_sub_eq' : ∀{a b c : ℤ}, a - b = c → a = b + c := @algebra.eq_add_of_sub_eq' _ _
+  theorem add_eq_of_eq_sub' : ∀{a b c : ℤ}, b = c - a → a + b = c := @algebra.add_eq_of_eq_sub' _ _
   theorem ne_zero_of_mul_ne_zero_right : ∀{a b : ℤ}, a * b ≠ 0 → a ≠ 0 :=
     @algebra.ne_zero_of_mul_ne_zero_right _ _
   theorem ne_zero_of_mul_ne_zero_left : ∀{a b : ℤ}, a * b ≠ 0 → b ≠ 0 :=