refactor(*): remove local simp AC lemmas

Using local simp lemmas everywhere for mul_assoc and friends defeats the purpose of the change in core. Now theorems are proven with only the AC lemmas actually used in the proof.

algebra/field.lean

@@ -28,6 +28,12 @@ end
 
 end division_ring
 
+section
+variables [field α] {a b c : α}
+
+lemma div_eq_inv_mul : a / b = b⁻¹ * a := mul_comm _ _
+end
+
 section
 variables [discrete_field α] {a b c : α}
 

algebra/functions.lean

@@ -35,6 +35,21 @@ lemma lt_max_iff : a < max b c ↔ a < b ∨ a < c :=
     | or.inr h := lt_of_lt_of_le h (le_max_right _ _)
     end)⟩
 
+theorem le_max_left_iff_true (a b : α) : a ≤ max a b ↔ true :=
+iff_true_intro (le_max_left a b)
+
+theorem le_max_right_iff_true (a b : α) : b ≤ max a b ↔ true :=
+iff_true_intro (le_max_right a b)
+
+theorem min_right_comm (a b c : α) : min (min a b) c = min (min a c) b :=
+right_comm min min_comm min_assoc a b c
+
+theorem max.left_comm (a b c : α) : max a (max b c) = max b (max a c) :=
+left_comm max max_comm max_assoc a b c
+
+theorem max.right_comm (a b c : α) : max (max a b) c = max (max a c) b :=
+right_comm max max_comm max_assoc a b c
+
 lemma max_min_distrib_left : max a (min b c) = min (max a b) (max a c) :=
 begin
   apply le_antisymm (le_min

algebra/group_power.lean

@@ -13,8 +13,6 @@ Note: power adopts the convention that 0^0=1.
 -/
 import data.nat.basic data.int.basic algebra.group
 
-local attribute [simp] mul_comm mul_assoc mul_left_comm
-
 universe u
 variable {α : Type u}
 
@@ -49,7 +47,7 @@ attribute [to_additive add_monoid.smul_one] pow_one
 
 @[to_additive smul_add_comm']
 theorem pow_mul_comm' (a : α) (n : ℕ) : a^n * a = a * a^n :=
-by induction n with n ih; simp [*, pow_succ]
+by induction n with n ih; simp [*, pow_succ, mul_assoc]
 
 theorem pow_succ' (a : α) (n : ℕ) : a^(n+1) = a^n * a :=
 by simp [pow_succ, pow_mul_comm']
@@ -59,7 +57,7 @@ attribute [to_additive smul_succ'] pow_succ'
 
 @[to_additive add_monoid.smul_add]
 theorem pow_add (a : α) (m n : ℕ) : a^(m + n) = a^m * a^n :=
-by induction n; simp [*, pow_succ', nat.add_succ]
+by induction n; simp [*, pow_succ', nat.add_succ, mul_assoc]
 
 @[simp] theorem one_pow (n : ℕ) : (1 : α)^n = (1:α) :=
 by induction n; simp [*, pow_succ]
@@ -99,7 +97,7 @@ attribute [to_additive list.sum_repeat] list.prod_repeat
 end monoid
 
 theorem nat.pow_eq_pow (p q : ℕ) : nat.pow p q = p ^ q :=
-by induction q; [refl, simp [nat.pow_succ, pow_succ, *]]
+by induction q; [refl, simp [nat.pow_succ, pow_succ, mul_comm, *]]
 
 /- commutative monoid -/
 
@@ -108,7 +106,7 @@ variables [comm_monoid α] {β : Type*} [add_comm_monoid β]
 
 theorem mul_pow (a b : α) : ∀ n, (a * b)^n = a^n * b^n
 | 0     := by simp
-| (n+1) := by simp [pow_succ]; rw mul_pow
+| (n+1) := by simp [pow_succ, mul_assoc, mul_left_comm]; rw mul_pow
 theorem add_monoid.add_smul (a b : β) : ∀ n, (a + b)•n = a•n + b•n
 | 0     := by simp
 | (n+1) := by simp [smul_succ]; rw add_monoid.add_smul
@@ -192,7 +190,7 @@ section discrete_field
 variables [discrete_field α] {a b c : α} {n : ℕ}
 
 theorem pow_inv (ha : a ≠ 0) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
-by induction n with n ih; simp [pow_succ, mul_inv', pow_ne_zero, *]
+by induction n with n ih; simp [pow_succ, mul_inv', pow_ne_zero, mul_comm, *]
 
 end discrete_field
 

algebra/order.lean

@@ -22,15 +22,14 @@ lemma lt_iff_le_and_ne [partial_order α] {a b : α} : a < b ↔ a ≤ b ∧ a 
 lemma eq_or_lt_of_le [partial_order α] {a b : α} (h : a ≤ b) : a = b ∨ a < b :=
 (lt_or_eq_of_le h).symm
 
-@[simp] lemma not_lt [linear_order α] {a b : α} : ¬ a < b ↔ b ≤ a :=
-⟨(lt_or_ge a b).resolve_left, not_lt_of_le⟩
+@[simp] lemma not_lt [linear_order α] {a b : α} : ¬ a < b ↔ b ≤ a := ⟨le_of_not_gt, not_lt_of_ge⟩
 
-lemma le_of_not_lt [linear_order α] {a b : α} : ¬ a < b → b ≤ a :=
-not_lt.1
+lemma le_of_not_lt [linear_order α] {a b : α} : ¬ a < b → b ≤ a := not_lt.1
 
-@[simp] lemma not_le [linear_order α] {a b : α} : ¬ a ≤ b ↔ b < a :=
-(lt_iff_le_not_le.trans ⟨and.right,
-  λ h, ⟨(le_total _ _).resolve_left h, h⟩⟩).symm
+@[simp] lemma not_le [linear_order α] {a b : α} : ¬ a ≤ b ↔ b < a := (lt_iff_not_ge b a).symm
+
+lemma lt_or_le [linear_order α] : ∀ a b : α, a < b ∨ b ≤ a := lt_or_ge
+lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ a > b := le_or_gt
 
 lemma not_lt_iff_eq_or_lt [linear_order α] {a b : α} : ¬ a < b ↔ a = b ∨ b < a :=
 not_lt.trans $ le_iff_eq_or_lt.trans $ or_congr eq_comm iff.rfl