chore(algebra/group/basic): dedup, add a lemma (#6810)

* drop `sub_eq_zero_iff_eq`, was a duplicate of `sub_eq_zero`;
* add a `simp` lemma `sub_eq_self : a - b = a ↔ b = 0`.

src/algebra/direct_limit.lean

@@ -479,7 +479,7 @@ theorem of_injective [directed_system G (λ i j h, f' i j h)]
   function.injective (of G (λ i j h, f' i j h) i) :=
 begin
   suffices : ∀ x, of G (λ i j h, f' i j h) i x = 0 → x = 0,
-  { intros x y hxy, rw ← sub_eq_zero_iff_eq, apply this,
+  { intros x y hxy, rw ← sub_eq_zero, apply this,
     rw [(of G _ i).map_sub, hxy, sub_self] },
   intros x hx, rcases of.zero_exact hx with ⟨j, hij, hfx⟩,
   apply hf i j hij, rw [hfx, (f' i j hij).map_zero]

src/algebra/group/basic.lean

@@ -333,25 +333,14 @@ lemma add_sub_assoc (a b c : G) : a + b - c = a + (b - c) :=
 by rw [sub_eq_add_neg, add_assoc, ←sub_eq_add_neg]
 
 lemma eq_of_sub_eq_zero (h : a - b = 0) : a = b :=
-have 0 + b = b, by rw zero_add,
-have (a - b) + b = b, by rwa h,
-by rwa [sub_eq_add_neg, neg_add_cancel_right] at this
-
-lemma sub_eq_zero_of_eq (h : a = b) : a - b = 0 :=
-by rw [h, sub_self]
-
-lemma sub_eq_zero_iff_eq : a - b = 0 ↔ a = b :=
-⟨eq_of_sub_eq_zero, sub_eq_zero_of_eq⟩
+calc a = a - b + b : (sub_add_cancel a b).symm
+   ... = b         : by rw [h, zero_add]
 
 @[simp] lemma sub_zero (a : G) : a - 0 = a :=
 by rw [sub_eq_add_neg, neg_zero, add_zero]
 
 lemma sub_ne_zero_of_ne (h : a ≠ b) : a - b ≠ 0 :=
-begin
-  intro hab,
-  apply h,
-  apply eq_of_sub_eq_zero hab
-end
+mt eq_of_sub_eq_zero h
 
 @[simp] lemma sub_neg_eq_add (a b : G) : a - (-b) = a + b :=
 by rw [sub_eq_add_neg, neg_neg]
@@ -372,13 +361,13 @@ by simp
 by rw [sub_add_eq_sub_sub_swap]; simp
 
 lemma eq_sub_of_add_eq (h : a + c = b) : a = b - c :=
-by simp [h.symm]
+by simp [← h]
 
 lemma sub_eq_of_eq_add (h : a = c + b) : a - b = c :=
 by simp [h]
 
 lemma eq_add_of_sub_eq (h : a - c = b) : a = b + c :=
-by simp [h.symm]
+by simp [← h]
 
 lemma add_eq_of_eq_sub (h : a = c - b) : a + b = c :=
 by simp [h]
@@ -401,9 +390,14 @@ by simp
 theorem sub_eq_zero : a - b = 0 ↔ a = b :=
 ⟨eq_of_sub_eq_zero, λ h, by rw [h, sub_self]⟩
 
+alias sub_eq_zero ↔ _ sub_eq_zero_of_eq
+
 theorem sub_ne_zero : a - b ≠ 0 ↔ a ≠ b :=
 not_congr sub_eq_zero
 
+@[simp] theorem sub_eq_self : a - b = a ↔ b = 0 :=
+by rw [sub_eq_add_neg, add_right_eq_self, neg_eq_zero]
+
 theorem eq_sub_iff_add_eq : a = b - c ↔ a + c = b :=
 by rw [sub_eq_add_neg, eq_add_neg_iff_add_eq]
 

src/algebra/lie/basic.lean

@@ -114,10 +114,10 @@ instance lie_algebra_self_module : lie_module R L L :=
   lie_smul := by apply lie_algebra.lie_smul, }
 
 @[simp] lemma neg_lie : ⁅-x, m⁆ = -⁅x, m⁆ :=
-by { rw [←sub_eq_zero_iff_eq, sub_neg_eq_add, ←add_lie], simp, }
+by { rw [←sub_eq_zero, sub_neg_eq_add, ←add_lie], simp, }
 
 @[simp] lemma lie_neg : ⁅x, -m⁆ = -⁅x, m⁆ :=
-by { rw [←sub_eq_zero_iff_eq, sub_neg_eq_add, ←lie_add], simp, }
+by { rw [←sub_eq_zero, sub_neg_eq_add, ←lie_add], simp, }
 
 @[simp] lemma gsmul_lie (a : ℤ) : ⁅a • x, m⁆ = a • ⁅x, m⁆ :=
 add_monoid_hom.map_gsmul ⟨λ (x : L), ⁅x, m⁆, zero_lie m, λ _ _, add_lie _ _ _⟩ _ _

src/algebra/linear_recurrence.lean

@@ -196,9 +196,9 @@ begin
               ring_hom.id_apply, polynomial.eval₂_monomial, polynomial.eval₂_sub],
   split,
   { intro h,
-    simpa [sub_eq_zero_iff_eq] using h 0 },
+    simpa [sub_eq_zero] using h 0 },
   { intros h n,
-    simp only [pow_add, sub_eq_zero_iff_eq.mp h, mul_sum],
+    simp only [pow_add, sub_eq_zero.mp h, mul_sum],
     exact sum_congr rfl (λ _ _, by ring) }
 end
 

src/algebra/ring/basic.lean

@@ -878,10 +878,10 @@ def add_monoid_hom.mk_ring_hom_of_mul_self_of_two_ne_zero [comm_ring β] (f : β
     intros x y,
     have hxy := h (x + y),
     rw [mul_add, add_mul, add_mul, f.map_add, f.map_add, f.map_add, f.map_add, h x, h y, add_mul,
-      mul_add, mul_add, ← sub_eq_zero_iff_eq, add_comm, ← sub_sub, ← sub_sub, ← sub_sub,
+      mul_add, mul_add, ← sub_eq_zero, add_comm, ← sub_sub, ← sub_sub, ← sub_sub,
       mul_comm y x, mul_comm (f y) (f x)] at hxy,
     simp only [add_assoc, add_sub_assoc, add_sub_cancel'_right] at hxy,
-    rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero, sub_eq_zero_iff_eq,
+    rw [sub_sub, ← two_mul, ← add_sub_assoc, ← two_mul, ← mul_sub, mul_eq_zero, sub_eq_zero,
       or_iff_not_imp_left] at hxy,
     exact hxy h_two,
   end,

src/analysis/special_functions/trigonometric.lean

@@ -1573,9 +1573,9 @@ begin
     apply_instance, },
   { rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub],
     rintro (⟨k, H⟩ | ⟨k, H⟩),
-    rw [← sub_eq_zero_iff_eq, cos_sub_cos, H, mul_assoc 2 π k,
+    rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k,
         mul_div_cancel_left _ (@two_ne_zero ℝ _ _), mul_comm π _, sin_int_mul_pi, mul_zero],
-    rw [← sub_eq_zero_iff_eq, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
+    rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
         mul_div_cancel_left _ (@two_ne_zero ℝ _ _), mul_comm π _, sin_int_mul_pi, mul_zero,
         zero_mul] }
 end
@@ -1592,12 +1592,12 @@ begin
     exact h.symm },
   { rw [angle_eq_iff_two_pi_dvd_sub, ←eq_sub_iff_add_eq, ←coe_sub, angle_eq_iff_two_pi_dvd_sub],
     rintro (⟨k, H⟩ | ⟨k, H⟩),
-    rw [← sub_eq_zero_iff_eq, sin_sub_sin, H, mul_assoc 2 π k,
+    rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k,
          mul_div_cancel_left _ (@two_ne_zero ℝ _ _), mul_comm π _, sin_int_mul_pi, mul_zero,
          zero_mul],
     have H' : θ + ψ = (2 * k) * π + π := by rwa [←sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add,
       mul_assoc, mul_comm π _, ←mul_assoc] at H,
-    rw [← sub_eq_zero_iff_eq, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
+    rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
         mul_div_cancel_left _ (@two_ne_zero ℝ _ _), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
         mul_zero] }
 end
@@ -1608,7 +1608,7 @@ begin
   cases sin_eq_iff_eq_or_add_eq_pi.mp Hsin with hs hs, { exact hs },
   rw [eq_neg_iff_add_eq_zero, hs] at hc,
   cases quotient.exact' hc with n hn, change n •ℤ _ = _ at hn,
-  rw [← neg_one_mul, add_zero, ← sub_eq_zero_iff_eq, gsmul_eq_mul, ← mul_assoc, ← sub_mul,
+  rw [← neg_one_mul, add_zero, ← sub_eq_zero, gsmul_eq_mul, ← mul_assoc, ← sub_mul,
       mul_eq_zero, eq_false_intro (ne_of_gt pi_pos), or_false, sub_neg_eq_add,
       ← int.cast_zero, ← int.cast_one, ← int.cast_bit0, ← int.cast_mul, ← int.cast_add,
       int.cast_inj] at hn,

src/data/polynomial/eval.lean

@@ -789,7 +789,7 @@ eval₂_neg _
 eval₂_sub _
 
 lemma root_X_sub_C : is_root (X - C a) b ↔ a = b :=
-by rw [is_root.def, eval_sub, eval_X, eval_C, sub_eq_zero_iff_eq, eq_comm]
+by rw [is_root.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
 
 @[simp] lemma neg_comp : (-p).comp q = -p.comp q := eval₂_neg _
 

src/data/polynomial/ring_division.lean

@@ -395,7 +395,7 @@ roots ((X : polynomial R) ^ n - C a)
 @[simp] lemma mem_nth_roots {n : ℕ} (hn : 0 < n) {a x : R} :
   x ∈ nth_roots n a ↔ x ^ n = a :=
 by rw [nth_roots, mem_roots (X_pow_sub_C_ne_zero hn a),
-  is_root.def, eval_sub, eval_C, eval_pow, eval_X, sub_eq_zero_iff_eq]
+  is_root.def, eval_sub, eval_C, eval_pow, eval_X, sub_eq_zero]
 
 @[simp] lemma nth_roots_zero (r : R) : nth_roots 0 r = 0 :=
 by simp only [empty_eq_zero, pow_zero, nth_roots, ← C_1, ← C_sub, roots_C]

src/data/real/golden_ratio.lean

@@ -162,14 +162,14 @@ end
 lemma geom_gold_is_sol_fib_rec : fib_rec.is_solution (pow φ) :=
 begin
   rw [fib_rec.geom_sol_iff_root_char_poly, fib_rec_char_poly_eq],
-  simp [sub_eq_zero_iff_eq]
+  simp [sub_eq_zero]
 end
 
 /-- The geometric sequence `λ n, ψ^n` is a solution of `fib_rec`. -/
 lemma geom_gold_conj_is_sol_fib_rec : fib_rec.is_solution (pow ψ) :=
 begin
   rw [fib_rec.geom_sol_iff_root_char_poly, fib_rec_char_poly_eq],
-  simp [sub_eq_zero_iff_eq]
+  simp [sub_eq_zero]
 end
 
 end fibrec

src/data/real/liouville.lean

@@ -51,7 +51,7 @@ begin
        ← int.cast_sub, ← int.cast_abs, ← int.cast_mul, int.cast_lt] at a1,
   -- At a0, clear denominators...
   replace a0 : ¬a * q - ↑b * p = 0, by
-    rwa [ne.def, div_eq_div_iff b0 (ne_of_gt qR0), mul_comm ↑p, ← sub_eq_zero_iff_eq,
+    rwa [ne.def, div_eq_div_iff b0 (ne_of_gt qR0), mul_comm ↑p, ← sub_eq_zero,
       -- ... and revert to integers
       ← int.cast_coe_nat, ← int.cast_mul, ← int.cast_mul, ← int.cast_sub, int.cast_eq_zero] at a0,
   -- Actually, `q` is a natural number

src/field_theory/abel_ruffini.lean

@@ -103,7 +103,7 @@ begin
   apply is_solvable_of_comm,
   intros σ τ,
   ext a ha,
-  rw [mem_root_set hn'', alg_hom.map_sub, aeval_X_pow, aeval_one, sub_eq_zero_iff_eq] at ha,
+  rw [mem_root_set hn'', alg_hom.map_sub, aeval_X_pow, aeval_one, sub_eq_zero] at ha,
   have key : ∀ σ : (X ^ n - 1 : polynomial F).gal, ∃ m : ℕ, σ a = a ^ m,
   { intro σ,
     obtain ⟨m, hm⟩ := σ.to_alg_hom.to_ring_hom.map_root_of_unity_eq_pow_self
@@ -136,11 +136,11 @@ begin
   have mem_range : ∀ {c}, c ^ n = 1 → ∃ d, algebra_map F (X ^ n - C a).splitting_field d = c :=
     λ c hc, ring_hom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c (or.resolve_left h hn'''
       (minpoly.irreducible ((splitting_field.normal (X ^ n - C a)).is_integral c)) (minpoly.dvd F c
-      (by rwa [map_id, alg_hom.map_sub, sub_eq_zero_iff_eq, aeval_X_pow, aeval_one])))),
+      (by rwa [map_id, alg_hom.map_sub, sub_eq_zero, aeval_X_pow, aeval_one])))),
   apply is_solvable_of_comm,
   intros σ τ,
   ext b hb,
-  rw [mem_root_set hn'', alg_hom.map_sub, aeval_X_pow, aeval_C, sub_eq_zero_iff_eq] at hb,
+  rw [mem_root_set hn'', alg_hom.map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hb,
   have hb' : b ≠ 0,
   { intro hb',
     rw [hb', zero_pow hn'] at hb,
@@ -168,7 +168,7 @@ begin
   have hn'' : (X ^ n - C a).degree ≠ 0 :=
     ne_of_eq_of_ne (degree_X_pow_sub_C hn' a) (mt with_bot.coe_eq_coe.mp hn),
   obtain ⟨b, hb⟩ := exists_root_of_splits i h hn'',
-  rw [eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero_iff_eq] at hb,
+  rw [eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] at hb,
   have hb' : b ≠ 0,
   { intro hb',
     rw [hb', zero_pow hn'] at hb,

src/geometry/euclidean/basic.lean

@@ -399,7 +399,7 @@ lemma dist_smul_vadd_eq_dist {v : V} (p₁ p₂ : P) (hv : v ≠ 0) (r : ℝ) :
   dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ (r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫) :=
 begin
   conv_lhs { rw [←mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_square,
-                 ←sub_eq_zero_iff_eq, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂,
+                 ←sub_eq_zero, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂,
                  ←real_inner_self_eq_norm_square, sub_self] },
   have hvi : ⟪v, v⟫ ≠ 0, by simpa using hv,
   have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 =

src/linear_algebra/affine_space/affine_subspace.lean

@@ -1084,7 +1084,7 @@ begin
     rcases hv1 with ⟨r, rfl⟩,
     use [r, v2 +ᵥ p1, vadd_mem_of_mem_direction hv2 hp1],
     symmetry' at hp,
-    rw [←sub_eq_zero_iff_eq, ←vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp,
+    rw [←sub_eq_zero, ←vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp,
     rw [hp, vadd_assoc] },
   { rintros ⟨r, p3, hp3, rfl⟩,
     use [r • (p2 -ᵥ p1), submodule.mem_span_singleton.2 ⟨r, rfl⟩, p3 -ᵥ p1,

src/linear_algebra/dual.lean

@@ -363,7 +363,7 @@ lemma decomposition (v : V) : dual_pair.lc e (h.coeffs v) = v :=
 begin
   refine eq_of_sub_eq_zero (h.total _),
   intros i,
-  simp [-sub_eq_add_neg, linear_map.map_sub, h.dual_lc, sub_eq_zero_iff_eq]
+  simp [-sub_eq_add_neg, linear_map.map_sub, h.dual_lc, sub_eq_zero]
 end
 
 lemma mem_of_mem_span {H : set ι} {x : V} (hmem : x ∈ submodule.span K (e '' H)) :

src/number_theory/bernoulli.lean

@@ -223,7 +223,7 @@ begin
       split_ifs at h with h2,
       { rw h2 at hlt, exfalso, exact lt_irrefl _ hlt, },
       have hn : (n! : ℚ) ≠ 0, { simp [factorial_ne_zero], },
-      rw [←mul_div_assoc, sub_eq_zero_iff_eq, div_eq_iff hn, div_mul_cancel _ hn,
+      rw [←mul_div_assoc, sub_eq_zero, div_eq_iff hn, div_mul_cancel _ hn,
         neg_one_pow_of_odd h_odd, neg_mul_eq_neg_mul_symm, one_mul] at h,
       exact eq_zero_of_neg_eq h.symm, },
     { exfalso,

src/ring_theory/jacobson.lean

@@ -294,7 +294,7 @@ begin
     { rw [set.mem_set_of_eq, degree_le_zero_iff] at hy,
       refine hy.symm ▸ ⟨X - C (ϕ.to_map ((quotient.mk P') (p.coeff 0))), monic_X_sub_C _, _⟩,
       simp only [eval₂_sub, eval₂_C, eval₂_X],
-      rw [sub_eq_zero_iff_eq, ← φ'.comp_apply, localization_map.map_comp, ring_hom.comp_apply],
+      rw [sub_eq_zero, ← φ'.comp_apply, localization_map.map_comp, ring_hom.comp_apply],
       refl } },
   { obtain ⟨p, rfl⟩ := quotient.mk_surjective p',
     refine polynomial.induction_on p

src/ring_theory/jacobson_ideal.lean

@@ -194,7 +194,7 @@ end
 
 lemma mem_jacobson_bot {x : R} : x ∈ jacobson (⊥ : ideal R) ↔ ∀ y, is_unit (x * y + 1) :=
 ⟨λ hx y, let ⟨z, hz⟩ := (mem_jacobson_iff.1 hx) y in
-  is_unit_iff_exists_inv.2 ⟨z, by rwa [add_mul, one_mul, ← sub_eq_zero_iff_eq]⟩,
+  is_unit_iff_exists_inv.2 ⟨z, by rwa [add_mul, one_mul, ← sub_eq_zero]⟩,
 λ h, mem_jacobson_iff.mpr (λ y, (let ⟨b, hb⟩ := is_unit_iff_exists_inv.1 (h y) in
   ⟨b, (submodule.mem_bot R).2 (hb ▸ (by ring))⟩))⟩
 

src/ring_theory/localization.lean

@@ -937,9 +937,9 @@ begin
     rw ← ring_hom.map_mul at hn,
     replace hn := congr_arg (ideal.quotient_map I f.to_map le_rfl) hn,
     simp only [ring_hom.map_one, ideal.quotient_map_mk, ring_hom.map_mul] at hn,
-    rw [ideal.quotient_map_mk, ← sub_eq_zero_iff_eq, ← ring_hom.map_sub,
+    rw [ideal.quotient_map_mk, ← sub_eq_zero, ← ring_hom.map_sub,
       ideal.quotient.eq_zero_iff_mem, ← ideal.quotient.eq_zero_iff_mem, ring_hom.map_sub,
-      sub_eq_zero_iff_eq, localization_map.mk'_eq_mul_mk'_one],
+      sub_eq_zero, localization_map.mk'_eq_mul_mk'_one],
     simp only [mul_eq_mul_left_iff, ring_hom.map_mul],
     exact or.inl (mul_left_cancel' (λ hn, hM (ideal.quotient.eq_zero_iff_mem.2
       (ideal.mem_comap.2 (ideal.quotient.eq_zero_iff_mem.1 hn)))) (trans hn

src/ring_theory/polynomial/basic.lean

@@ -352,7 +352,7 @@ begin
   { obtain ⟨f, hf⟩ := mem_image_of_mem_map_of_surjective (polynomial.map_ring_hom i)
       (polynomial.map_surjective _ (((quotient.mk I).comp C).range_restrict_surjective)) this,
     refine sub_add_cancel (C y) f ▸ I.add_mem (hi' _ : (C y - f) ∈ I) hf.1,
-    rw [ring_hom.mem_ker, ring_hom.map_sub, hf.2, sub_eq_zero_iff_eq, coe_map_ring_hom, map_C] },
+    rw [ring_hom.mem_ker, ring_hom.map_sub, hf.2, sub_eq_zero, coe_map_ring_hom, map_C] },
   exact hx,
 end