feat(*): assorted simp lemmas for IMO 2019 q1 (#4383)

* mark some lemmas about cancelling in expressions with `(-)` as `simp`;
* simplify `a * b = a * c` to `b = c ∨ a = 0`, and similarly for
  `a * c = b * c;
* change `priority` of `monoid.has_pow` and `group.has_pow` to the
  default priority.
* simplify `monoid.pow` and `group.gpow` to `has_pow.pow`.

src/algebra/group/basic.lean

@@ -402,7 +402,7 @@ begin simp, rw [add_left_comm c], simp end
 lemma neg_neg_sub_neg (a b : G) : - (-a - -b) = a - b :=
 by simp
 
-lemma sub_sub_cancel (a b : G) : a - (a - b) = b := sub_sub_self a b
+@[simp] lemma sub_sub_cancel (a b : G) : a - (a - b) = b := sub_sub_self a b
 
 lemma sub_eq_neg_add (a b : G) : a - b = -b + a :=
 add_comm _ _
@@ -427,25 +427,27 @@ by rw [sub_eq_neg_add, neg_add_cancel_left]
 lemma add_sub_cancel'_right (a b : G) : a + (b - a) = b :=
 by rw [← add_sub_assoc, add_sub_cancel']
 
-@[simp] lemma add_add_neg_cancel'_right (a b : G) : a + (b + -a) = b :=
+-- This lemma is in the `simp` set under the name `add_neg_cancel_comm_assoc`,
+-- defined  in `algebra/group/commute`
+lemma add_add_neg_cancel'_right (a b : G) : a + (b + -a) = b :=
 add_sub_cancel'_right a b
 
 lemma sub_right_comm (a b c : G) : a - b - c = a - c - b :=
 add_right_comm _ _ _
 
-lemma add_add_sub_cancel (a b c : G) : (a + c) + (b - c) = a + b :=
+@[simp] lemma add_add_sub_cancel (a b c : G) : (a + c) + (b - c) = a + b :=
 by rw [add_assoc, add_sub_cancel'_right]
 
-lemma sub_add_add_cancel (a b c : G) : (a - c) + (b + c) = a + b :=
+@[simp] lemma sub_add_add_cancel (a b c : G) : (a - c) + (b + c) = a + b :=
 by rw [add_left_comm, sub_add_cancel, add_comm]
 
-lemma sub_add_sub_cancel' (a b c : G) : (a - b) + (c - a) = c - b :=
+@[simp] lemma sub_add_sub_cancel' (a b c : G) : (a - b) + (c - a) = c - b :=
 by rw add_comm; apply sub_add_sub_cancel
 
-lemma add_sub_sub_cancel (a b c : G) : (a + b) - (a - c) = b + c :=
+@[simp] lemma add_sub_sub_cancel (a b c : G) : (a + b) - (a - c) = b + c :=
 by rw [← sub_add, add_sub_cancel']
 
-lemma sub_sub_sub_cancel_left (a b c : G) : (c - a) - (c - b) = b - a :=
+@[simp] lemma sub_sub_sub_cancel_left (a b c : G) : (c - a) - (c - b) = b - a :=
 by rw [← neg_sub b c, sub_neg_eq_add, add_comm, sub_add_sub_cancel]
 
 lemma sub_eq_sub_iff_add_eq_add : a - b = c - d ↔ a + d = c + b :=

src/algebra/group/commute.lean

@@ -127,6 +127,40 @@ theorem inv_inv : commute a b → commute a⁻¹ b⁻¹ := semiconj_by.inv_inv_s
 @[simp, to_additive]
 theorem inv_inv_iff : commute a⁻¹ b⁻¹ ↔ commute a b := semiconj_by.inv_inv_symm_iff
 
+@[to_additive]
+protected theorem inv_mul_cancel (h : commute a b) : a⁻¹ * b * a = b :=
+by rw [h.inv_left.eq, inv_mul_cancel_right]
+
+@[to_additive]
+theorem inv_mul_cancel_assoc (h : commute a b) : a⁻¹ * (b * a) = b :=
+by rw [← mul_assoc, h.inv_mul_cancel]
+
+@[to_additive]
+protected theorem mul_inv_cancel (h : commute a b) : a * b * a⁻¹ = b :=
+by rw [h.eq, mul_inv_cancel_right]
+
+@[to_additive]
+theorem mul_inv_cancel_assoc (h : commute a b) : a * (b * a⁻¹) = b :=
+by rw [← mul_assoc, h.mul_inv_cancel]
+
 end group
 
 end commute
+
+section comm_group
+
+variables {G : Type*} [comm_group G] (a b : G)
+
+@[simp, to_additive] lemma mul_inv_cancel_comm : a * b * a⁻¹ = b :=
+(commute.all a b).mul_inv_cancel
+
+@[simp, to_additive] lemma mul_inv_cancel_comm_assoc : a * (b * a⁻¹) = b :=
+(commute.all a b).mul_inv_cancel_assoc
+
+@[simp, to_additive] lemma inv_mul_cancel_comm : a⁻¹ * b * a = b :=
+(commute.all a b).inv_mul_cancel
+
+@[simp, to_additive] lemma inv_mul_cancel_comm_assoc : a⁻¹ * (b * a) = b :=
+(commute.all a b).inv_mul_cancel_assoc
+
+end comm_group

src/algebra/group_power/basic.lean

@@ -48,11 +48,13 @@ def monoid.pow [has_mul M] [has_one M] (a : M) : ℕ → M
 /-- The scalar multiplication in an additive monoid.
 `n •ℕ a = a+a+...+a` n times. -/
 def nsmul [has_add A] [has_zero A] (n : ℕ) (a : A) : A :=
-@monoid.pow (multiplicative A) _ { one := (0 : A) } a n
+@monoid.pow (multiplicative A) _ _ a n
 
 infix ` •ℕ `:70 := nsmul
 
-@[priority 5] instance monoid.has_pow [monoid M] : has_pow M ℕ := ⟨monoid.pow⟩
+instance monoid.has_pow [monoid M] : has_pow M ℕ := ⟨monoid.pow⟩
+
+@[simp] lemma monoid.pow_eq_has_pow [monoid M] (a : M) (n : ℕ) : monoid.pow a n = a^n := rfl
 
 /-!
 ### Commutativity
@@ -248,10 +250,12 @@ with the definition `(-n) •ℤ a = -(n •ℕ a)`.
 def gsmul (n : ℤ) (a : A) : A :=
 @gpow (multiplicative A) _ a n
 
-@[priority 10] instance group.has_pow : has_pow G ℤ := ⟨gpow⟩
+instance group.has_pow : has_pow G ℤ := ⟨gpow⟩
 
 infix ` •ℤ `:70 := gsmul
 
+@[simp] lemma group.gpow_eq_has_pow (a : G) (n : ℤ) : gpow a n = a ^ n := rfl
+
 section nat
 
 @[simp] theorem inv_pow (a : G) (n : ℕ) : (a⁻¹)^n = (a^n)⁻¹ :=

src/algebra/group_with_zero.lean

@@ -350,6 +350,12 @@ lemma mul_left_inj' (hc : c ≠ 0) : a * c = b * c ↔ a = b := ⟨mul_right_can
 
 lemma mul_right_inj' (ha : a ≠ 0) : a * b = a * c ↔ b = c := ⟨mul_left_cancel' ha, λ h, h ▸ rfl⟩
 
+@[simp] lemma mul_eq_mul_right_iff : a * c = b * c ↔ a = b ∨ c = 0 :=
+by by_cases hc : c = 0; [simp [hc], simp [mul_left_inj', hc]]
+
+@[simp] lemma mul_eq_mul_left_iff : a * b = a * c ↔ b = c ∨ a = 0 :=
+by by_cases ha : a = 0; [simp [ha], simp [mul_right_inj', ha]]
+
 /-- Pullback a `monoid_with_zero` class along an injective function. -/
 protected def function.injective.cancel_monoid_with_zero [has_zero M₀'] [has_mul M₀'] [has_one M₀']
   (f : M₀' → M₀) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
@@ -760,7 +766,7 @@ local attribute [simp] mul_assoc mul_comm mul_left_comm
 
 lemma div_mul_div (a b c d : G₀) :
       (a / b) * (c / d) = (a * c) / (b * d) :=
-by { simp [div_eq_mul_inv], rw [mul_inv_rev', mul_comm d⁻¹] }
+by simp [div_eq_mul_inv, mul_inv']
 
 lemma mul_div_mul_left (a b : G₀) {c : G₀} (hc : c ≠ 0) :
       (c * a) / (c * b) = a / b :=

src/analysis/calculus/specific_functions.lean

@@ -61,7 +61,8 @@ begin
                (((has_deriv_at_exp _).comp x (has_deriv_at_inv hx).neg))).div
             (has_deriv_at_pow (2 * n) x) (pow_ne_zero _ hx) using 1,
   field_simp [hx, P_aux],
-  cases n; simp [nat.succ_eq_add_one, A]; ring_exp
+  -- `ring_exp` can't solve `p ∨ q` goal generated by `mul_eq_mul_right_iff`
+  cases n; simp [nat.succ_eq_add_one, A, -mul_eq_mul_right_iff]; ring_exp
 end
 
 /-- For positive values, the derivative of the `n`-th auxiliary function `f_aux n`

src/analysis/special_functions/trigonometric.lean

@@ -874,7 +874,7 @@ begin
   rw [add_comm, sub_add, sub_neg_eq_add], apply sub_lt_sub_left,
   apply add_lt_of_lt_sub_left,
   rw (show x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 / 12,
-    by simp [div_eq_mul_inv, (mul_sub _ _ _).symm, -sub_eq_add_neg]; congr; norm_num),
+    by simp [div_eq_mul_inv, ← mul_sub]; norm_num),
   apply mul_lt_mul',
   { rw [pow_succ x 3], refine le_trans _ (le_of_eq (one_mul _)),
     rw mul_le_mul_right, exact h', apply pow_pos h },

src/data/int/basic.lean

@@ -655,6 +655,10 @@ protected theorem div_eq_of_eq_mul_right {a b c : ℤ} (H1 : b ≠ 0) (H2 : a =
   a / b = c :=
 by rw [H2, int.mul_div_cancel_left _ H1]
 
+protected theorem eq_div_of_mul_eq_right {a b c : ℤ} (H1 : a ≠ 0) (H2 : a * b = c) :
+  b = c / a :=
+eq.symm $ int.div_eq_of_eq_mul_right H1 H2.symm
+
 protected theorem div_eq_iff_eq_mul_right {a b c : ℤ} (H : b ≠ 0) (H' : b ∣ a) :
   a / b = c ↔ a = b * c :=
 ⟨int.eq_mul_of_div_eq_right H', int.div_eq_of_eq_mul_right H⟩

src/data/padics/padic_integers.lean

@@ -137,9 +137,8 @@ def coe.ring_hom : ℤ_[p] →+* ℚ_[p]  :=
 @[simp, norm_cast] lemma coe_sub : ∀ (z1 z2 : ℤ_[p]), (↑(z1 - z2) : ℚ_[p]) = ↑z1 - ↑z2 :=
 coe.ring_hom.map_sub
 
-@[simp, norm_cast] lemma cast_pow (x : ℤ_[p]) : ∀ (n : ℕ), (↑(x^n) : ℚ_[p]) = (↑x : ℚ_[p])^n
-| 0 := by simp
-| (k+1) := by simp [monoid.pow, pow]; congr; apply cast_pow
+@[simp, norm_cast] lemma coet_pow (x : ℤ_[p]) (n : ℕ) : (↑(x^n) : ℚ_[p]) = (↑x : ℚ_[p])^n :=
+coe.ring_hom.map_pow x n
 
 @[simp] lemma mk_coe : ∀ (k : ℤ_[p]), (⟨k, k.2⟩ : ℤ_[p]) = k
 | ⟨_, _⟩ := rfl
@@ -154,7 +153,6 @@ instance : char_zero ℤ_[p] :=
   λ m n h, cast_injective $
   show (m:ℚ_[p]) = n, by { rw subtype.ext_iff at h, norm_cast at h, exact h } }
 
-
 @[simp, norm_cast] lemma coe_int_eq (z1 z2 : ℤ) : (z1 : ℤ_[p]) = z2 ↔ z1 = z2 :=
 suffices (z1 : ℚ_[p]) = z2 ↔ z1 = z2, from iff.trans (by norm_cast) this,
 by norm_cast

src/set_theory/ordinal_notation.lean

@@ -643,8 +643,8 @@ begin
   haveI := (NF_repr_split' e₂).1,
   casesI a with a0 n a',
   { cases m with m,
-    { by_cases o₂ = 0; simp [pow, power, e₁, h]; apply_instance },
-    { by_cases m = 0; simp [pow, power, e₁, e₂, h]; apply_instance } },
+    { by_cases o₂ = 0; simp [pow, power, *]; apply_instance },
+    { by_cases m = 0; simp [pow, power, -monoid.pow_eq_has_pow, *]; apply_instance } },
   { simp [pow, power, e₁, e₂, split_eq_scale_split' e₂],
     have := na.fst,
     cases k with k; simp [succ_eq_add_one, power]; resetI; apply_instance }