chore(algebra/group/basic): add 3 simp attrs (#9050)

archive/imo/imo2008_q2.lean

@@ -31,53 +31,28 @@ lemma subst_abc {x y z : ℝ} (h : x*y*z = 1) :
   ∃ a b c : ℝ, a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ x = a/b ∧ y = b/c ∧ z = c /a :=
 begin
   use [x, 1, 1/y],
-  have h₁ : x ≠ 0 := left_ne_zero_of_mul (left_ne_zero_of_mul_eq_one h),
-  have h₂ : (1 : ℝ) ≠ (0 : ℝ) := one_ne_zero,
-  have hy_ne_zero : y ≠ 0 := right_ne_zero_of_mul (left_ne_zero_of_mul_eq_one h),
-  have h₃ : 1/y ≠ 0 := one_div_ne_zero hy_ne_zero,
-  have h₄ : x = x / 1 := (div_one x).symm,
-  have h₅ : y = 1 / (1 / y) := (one_div_one_div y).symm,
-  have h₆ : z = 1 / y / x, { field_simp, linarith [h] },
-  exact ⟨h₁, h₂, h₃, h₄, h₅, h₆⟩,
+  obtain ⟨⟨hx, hy⟩, hz⟩ : (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0,
+    by simpa [not_or_distrib] using trans_rel_right (≠) h one_ne_zero,
+  have : z * (y * x) = 1, by { rw ← h, ac_refl },
+  field_simp *
 end
 
 theorem imo2008_q2a (x y z : ℝ) (h : x*y*z = 1) (hx : x ≠ 1) (hy : y ≠ 1) (hz : z ≠ 1) :
   x^2 / (x-1)^2 + y^2 / (y-1)^2 + z^2 / (z-1)^2 ≥ 1 :=
 begin
-  obtain ⟨a, b, c, ha, hb, hc, hx₂, hy₂, hz₂⟩ := subst_abc h,
-
-  set m := c-b with hm_abc,
-  set n := b-a with hn_abc,
-  have ha_cmn : a = c - m - n,      { linarith },
-  have hb_cmn : b = c - m,          { linarith },
-  have hab_mn : (a-b)^2 = n^2,      { rw [ha_cmn, hb_cmn], ring },
-  have hbc_mn : (b-c)^2 = m^2,      { rw hb_cmn, ring },
-  have hca_mn : (c-a)^2 = (m+n)^2,  { rw ha_cmn, ring },
-
+  obtain ⟨a, b, c, ha, hb, hc, rfl, rfl, rfl⟩ := subst_abc h,
+  obtain ⟨m, n, rfl, rfl⟩ : ∃ m n, b = c - m ∧ a = c - m - n,
+  { use [c - b, b - a], simp },
   have hm_ne_zero : m ≠ 0,
-  { rw hm_abc, rw hy₂ at hy, intro p, apply hy, field_simp, linarith },
-
+  { contrapose! hy, field_simp, assumption },
   have hn_ne_zero : n ≠ 0,
-  { rw hn_abc, rw hx₂ at hx, intro p, apply hx, field_simp, linarith },
-
+  { contrapose! hx, field_simp, assumption },
   have hmn_ne_zero : m + n ≠ 0,
-  { rw hm_abc, rw hn_abc, rw hz₂ at hz, intro p, apply hz, field_simp, linarith },
-
-  have key : x^2 / (x-1)^2 + y^2 / (y-1)^2 + z^2 / (z-1)^2 - 1 ≥ 0,
-  { calc  x^2 / (x-1)^2 + y^2 / (y-1)^2 + z^2 / (z-1)^2 - 1
-        = (a/b)^2 / (a/b-1)^2 + (b/c)^2 / (b/c-1)^2 + (c/a)^2 / (c/a-1)^2 - 1 :
-          by rw [hx₂, hy₂, hz₂]
-    ... = a^2/(a-b)^2 + b^2/(b-c)^2 + c^2/(c-a)^2 - 1 :
-          by field_simp [div_sub_one hb, div_sub_one hc, div_sub_one ha]
-    ... = (c-m-n)^2/n^2 + (c-m)^2/m^2 + c^2/(m+n)^2 - 1 :
-          by rw [hab_mn, hbc_mn, hca_mn, ha_cmn, hb_cmn]
-    ... = ( (c*(m^2+n^2+m*n) - m*(m+n)^2) / (m*n*(m+n)) )^2 :
-          by { ring_nf, field_simp, ring }
-    ... ≥ 0 :
-          sq_nonneg _ },
-
-
-  linarith [key],
+  { contrapose! hz, field_simp, linarith },
+  have hc_sub_sub : c - (c - m - n) = m + n, by abel,
+  rw [ge_iff_le, ← sub_nonneg],
+  convert sq_nonneg ((c*(m^2+n^2+m*n) - m*(m+n)^2) / (m*n*(m+n)) ),
+  field_simp *, ring
 end
 
 def rational_solutions := { s : ℚ×ℚ×ℚ | ∃ (x y z : ℚ), s = (x, y, z) ∧

src/algebra/group/basic.lean

@@ -395,10 +395,10 @@ sub_right_injective.eq_iff
 @[simp] lemma sub_left_inj : b - a = c - a ↔ b = c :=
 by { rw [sub_eq_add_neg, sub_eq_add_neg], exact add_left_inj _ }
 
-lemma sub_add_sub_cancel (a b c : G) : (a - b) + (b - c) = a - c :=
+@[simp] lemma sub_add_sub_cancel (a b c : G) : (a - b) + (b - c) = a - c :=
 by rw [← add_sub_assoc, sub_add_cancel]
 
-lemma sub_sub_sub_cancel_right (a b c : G) : (a - c) - (b - c) = a - b :=
+@[simp] lemma sub_sub_sub_cancel_right (a b c : G) : (a - c) - (b - c) = a - b :=
 by rw [← neg_sub c b, sub_neg_eq_add, sub_add_sub_cancel]
 
 theorem sub_sub_assoc_swap : a - (b - c) = a + c - b :=
@@ -506,6 +506,8 @@ by simp
 
 @[simp] lemma sub_sub_cancel (a b : G) : a - (a - b) = b := sub_sub_self a b
 
+@[simp] lemma sub_sub_cancel_left (a b : G) : a - b - a = -b := by simp
+
 lemma sub_eq_neg_add (a b : G) : a - b = -b + a :=
 by rw [sub_eq_add_neg, add_comm _ _]
 

src/analysis/calculus/fderiv_measurable.lean

@@ -332,10 +332,8 @@ begin
     { apply le_of_mem_A (hn e (n e) m (le_refl _) m_ge).2.2,
       { simp only [mem_closed_ball, dist_self],
         exact div_nonneg (le_of_lt P) (zero_le_two) },
-      { simp [dist_eq_norm],
-        convert h'k,
-        field_simp,
-        ring_exp } },
+      { simpa only [dist_eq_norm, add_sub_cancel', mem_closed_ball, pow_succ', mul_one_div]
+          using h'k } },
     have J2 : ∥f (x + y) - f x - L e (n e) m y∥ ≤ 4 * (1/2) ^ e * ∥y∥ := calc
       ∥f (x + y) - f x - L e (n e) m y∥ ≤ (1/2) ^ e * (1/2) ^ m :
         by simpa only [add_sub_cancel'] using J1
@@ -345,12 +343,10 @@ begin
     -- use the previous estimates to see that `f (x + y) - f x - f' y` is small.
     calc ∥f (x + y) - f x - f' y∥
         = ∥(f (x + y) - f x - L e (n e) m y) + (L e (n e) m - f') y∥ :
-      by { congr' 1, simp, abel }
-    ... ≤ ∥f (x + y) - f x - L e (n e) m y∥ + ∥(L e (n e) m - f') y∥ :
-      norm_add_le _ _
+      congr_arg _ (by simp)
     ... ≤ 4 * (1/2) ^ e * ∥y∥ + 12 * ∥c∥ * (1/2) ^ e * ∥y∥ :
-      add_le_add J2
-        (le_trans (le_op_norm _ _) (mul_le_mul_of_nonneg_right (Lf' _ _ m_ge) (norm_nonneg _)))
+      norm_add_le_of_le J2
+        ((le_op_norm _ _).trans (mul_le_mul_of_nonneg_right (Lf' _ _ m_ge) (norm_nonneg _)))
     ... = (4 + 12 * ∥c∥) * ∥y∥ * (1/2) ^ e : by ring
     ... ≤ (4 + 12 * ∥c∥) * ∥y∥ * (ε / (4 + 12 * ∥c∥)) :
       mul_le_mul_of_nonneg_left he.le

src/analysis/convex/basic.lean

@@ -740,7 +740,6 @@ convex_halfspace_gt (is_linear_map.mk complex.add_im complex.smul_im) _
 lemma convex_halfspace_im_lge (r : ℝ) : convex {c : ℂ | r ≤ c.im} :=
 convex_halfspace_ge (is_linear_map.mk complex.add_im complex.smul_im) _
 
-
 section submodule
 open submodule
 

src/analysis/convex/cone.lean

@@ -244,7 +244,7 @@ end
 def to_preorder (S : convex_cone E) (h₁ : pointed S) : preorder E :=
 { le := λ x y, y - x ∈ S,
   le_refl := λ x, by change x - x ∈ S; rw [sub_self x]; exact h₁,
-  le_trans := λ x y z xy zy, by simp [(show z - x = z - y + (y - x), by abel), add_mem S zy xy] }
+  le_trans := λ x y z xy zy, by simpa using add_mem S zy xy }
 
 /-- A pointed and salient cone defines a partial order. -/
 def to_partial_order (S : convex_cone E) (h₁ : pointed S) (h₂ : salient S) : partial_order E :=