feat: a * b ≠ b ↔ a ≠ 1 (#3726)

leanprover-community/mathlib#18635

* [`algebra.group.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..84771a9f5f0bd5e5d6218811556508ddf476dcbd)
* [`algebra.order.field.basic`@`44e29dbcff83ba7114a464d592b8c3743987c1e5`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/field/basic?range=44e29dbcff83ba7114a464d592b8c3743987c1e5..84771a9f5f0bd5e5d6218811556508ddf476dcbd)




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/Group/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 
 ! This file was ported from Lean 3 source module algebra.group.basic
-! leanprover-community/mathlib commit 2196ab363eb097c008d4497125e0dde23fb36db2
+! leanprover-community/mathlib commit 84771a9f5f0bd5e5d6218811556508ddf476dcbd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -191,6 +191,16 @@ theorem self_eq_mul_right : a = a * b ↔ b = 1 :=
 #align self_eq_mul_right self_eq_mul_right
 #align self_eq_add_right self_eq_add_right
 
+@[to_additive]
+theorem mul_right_ne_self : a * b ≠ a ↔ b ≠ 1 := mul_right_eq_self.not
+#align mul_right_ne_self mul_right_ne_self
+#align add_right_ne_self add_right_ne_self
+
+@[to_additive]
+theorem self_ne_mul_right : a ≠ a * b ↔ b ≠ 1 := self_eq_mul_right.not
+#align self_ne_mul_right self_ne_mul_right
+#align self_ne_add_right self_ne_add_right
+
 end LeftCancelMonoid
 
 section RightCancelMonoid
@@ -210,6 +220,16 @@ theorem self_eq_mul_left : b = a * b ↔ a = 1 :=
 #align self_eq_mul_left self_eq_mul_left
 #align self_eq_add_left self_eq_add_left
 
+@[to_additive]
+theorem mul_left_ne_self : a * b ≠ b ↔ a ≠ 1 := mul_left_eq_self.not
+#align mul_left_ne_self mul_left_ne_self
+#align add_left_ne_self add_left_ne_self
+
+@[to_additive]
+theorem self_ne_mul_left : b ≠ a * b ↔ a ≠ 1 := self_eq_mul_left.not
+#align self_ne_mul_left self_ne_mul_left
+#align self_ne_add_left self_ne_add_left
+
 end RightCancelMonoid
 
 section InvolutiveInv

Mathlib/Algebra/Order/Field/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 ! This file was ported from Lean 3 source module algebra.order.field.basic
-! leanprover-community/mathlib commit 44e29dbcff83ba7114a464d592b8c3743987c1e5
+! leanprover-community/mathlib commit 84771a9f5f0bd5e5d6218811556508ddf476dcbd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -511,22 +511,25 @@ theorem one_half_pos : (0 : α) < 1 / 2 :=
   half_pos zero_lt_one
 #align one_half_pos one_half_pos
 
-theorem div_two_lt_of_pos (h : 0 < a) : a / 2 < a := by
-  rw [div_lt_iff (zero_lt_two' α)]
-  exact lt_mul_of_one_lt_right h one_lt_two
-#align div_two_lt_of_pos div_two_lt_of_pos
+@[simp]
+theorem half_le_self_iff : a / 2 ≤ a ↔ 0 ≤ a := by
+  rw [div_le_iff (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]
+#align half_le_self_iff half_le_self_iff
 
-theorem half_lt_self : 0 < a → a / 2 < a :=
-  div_two_lt_of_pos
-#align half_lt_self half_lt_self
+@[simp]
+theorem half_lt_self_iff : a / 2 < a ↔ 0 < a := by
+  rw [div_lt_iff (zero_lt_two' α), mul_two, lt_add_iff_pos_left]
+#align half_lt_self_iff half_lt_self_iff
 
-theorem half_le_self (ha_nonneg : 0 ≤ a) : a / 2 ≤ a := by
-  by_cases h0 : a = 0
-  · simp [h0]
-  · rw [← Ne.def] at h0
-    exact (half_lt_self (lt_of_le_of_ne ha_nonneg h0.symm)).le
+alias half_le_self_iff ↔ _ half_le_self
 #align half_le_self half_le_self
 
+alias half_lt_self_iff ↔ _ half_lt_self
+#align half_lt_self half_lt_self
+
+alias half_lt_self ← div_two_lt_of_pos
+#align div_two_lt_of_pos div_two_lt_of_pos
+
 theorem one_half_lt_one : (1 / 2 : α) < 1 :=
   half_lt_self zero_lt_one
 #align one_half_lt_one one_half_lt_one