feat(intervals/image_preimage): preimage under multiplication (#3757)

Add lemmas `preimage_mul_const_Ixx` and `preimage_const_mul_Ixx`.
Also generalize `equiv.mul_left` and `equiv.mul_right` to `units`.

Author: urkud

src/algebra/ordered_field.lean

@@ -382,6 +382,10 @@ by rw [mul_comm, div_lt_iff hc]
 lemma div_lt_iff_of_neg (hc : c < 0) : b / c < a ↔ a * c < b :=
 ⟨mul_lt_of_neg_of_div_lt hc, div_lt_of_neg_of_mul_lt hc⟩
 
+lemma lt_div_iff_of_neg (hc : c < 0) : a < b / c ↔ b < a * c :=
+by rw [← neg_neg c, div_neg, lt_neg, div_lt_iff (neg_pos.2 hc), ← neg_mul_eq_neg_mul,
+  ← neg_mul_eq_mul_neg _ (-c)]
+
 lemma inv_le_inv (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
 by rw [inv_eq_one_div, div_le_iff ha,
        ← div_eq_inv_mul, one_le_div_iff_le hb]

src/data/equiv/mul_add.lean

@@ -304,7 +304,8 @@ by refine_struct { to_fun := add_equiv.to_equiv }; intros; refl
 end add_aut
 
 /-- A group is isomorphic to its group of units. -/
-def to_units (G) [group G] : G ≃* units G :=
+@[to_additive to_add_units "An additive group is isomorphic to its group of additive units"]
+def to_units {G} [group G] : G ≃* units G :=
 { to_fun := λ x, ⟨x, x⁻¹, mul_inv_self _, inv_mul_self _⟩,
   inv_fun := coe,
   left_inv := λ x, rfl,
@@ -323,6 +324,36 @@ def map_equiv (h : M ≃* N) : units M ≃* units N :=
   right_inv := λ u, ext $ h.right_inv u,
   .. map h.to_monoid_hom }
 
+/-- Left multiplication by a unit of a monoid is a permutation of the underlying type. -/
+@[to_additive "Left addition of an additive unit is a permutation of the underlying type."]
+def mul_left (u : units M) : equiv.perm M :=
+{ to_fun    := λx, u * x,
+  inv_fun   := λx, ↑u⁻¹ * x,
+  left_inv  := u.inv_mul_cancel_left,
+  right_inv := u.mul_inv_cancel_left }
+
+@[simp, to_additive]
+lemma coe_mul_left (u : units M) : ⇑u.mul_left = (*) u := rfl
+
+@[simp, to_additive]
+lemma mul_left_symm (u : units M) : u.mul_left.symm = u⁻¹.mul_left :=
+equiv.ext $ λ x, rfl
+
+/-- Right multiplication by a unit of a monoid is a permutation of the underlying type. -/
+@[to_additive "Right addition of an additive unit is a permutation of the underlying type."]
+def mul_right (u : units M) : equiv.perm M :=
+{ to_fun    := λx, x * u,
+  inv_fun   := λx, x * ↑u⁻¹,
+  left_inv  := λ x, mul_inv_cancel_right x u,
+  right_inv := λ x, inv_mul_cancel_right x u }
+
+@[simp, to_additive]
+lemma coe_mul_right (u : units M) : ⇑u.mul_right = λ x : M, x * u := rfl
+
+@[simp, to_additive]
+lemma mul_right_symm (u : units M) : u.mul_right.symm = u⁻¹.mul_right :=
+equiv.ext $ λ x, rfl
+
 end units
 
 namespace equiv
@@ -332,11 +363,7 @@ variables [group G]
 
 /-- Left multiplication in a `group` is a permutation of the underlying type. -/
 @[to_additive "Left addition in an `add_group` is a permutation of the underlying type."]
-protected def mul_left (a : G) : perm G :=
-{ to_fun    := λx, a * x,
-  inv_fun   := λx, a⁻¹ * x,
-  left_inv  := assume x, show a⁻¹ * (a * x) = x, from inv_mul_cancel_left a x,
-  right_inv := assume x, show a * (a⁻¹ * x) = x, from mul_inv_cancel_left a x }
+protected def mul_left (a : G) : perm G := (to_units a).mul_left
 
 @[simp, to_additive]
 lemma coe_mul_left (a : G) : ⇑(equiv.mul_left a) = (*) a := rfl
@@ -347,11 +374,7 @@ ext $ λ x, rfl
 
 /-- Right multiplication in a `group` is a permutation of the underlying type. -/
 @[to_additive "Right addition in an `add_group` is a permutation of the underlying type."]
-protected def mul_right (a : G) : perm G :=
-{ to_fun    := λx, x * a,
-  inv_fun   := λx, x * a⁻¹,
-  left_inv  := assume x, show (x * a) * a⁻¹ = x, from mul_inv_cancel_right x a,
-  right_inv := assume x, show (x * a⁻¹) * a = x, from inv_mul_cancel_right x a }
+protected def mul_right (a : G) : perm G := (to_units a).mul_right
 
 @[simp, to_additive]
 lemma coe_mul_right (a : G) : ⇑(equiv.mul_right a) = λ x, x * a := rfl

src/data/set/intervals/image_preimage.lean

@@ -278,17 +278,139 @@ section linear_ordered_field
 
 variables {k : Type u} [linear_ordered_field k]
 
+@[simp] lemma preimage_mul_const_Iio (a : k) {c : k} (h : 0 < c) :
+  (λ x, x * c) ⁻¹' (Iio a) = Iio (a / c) :=
+ext $ λ x, (lt_div_iff h).symm
+
+@[simp] lemma preimage_mul_const_Ioi (a : k) {c : k} (h : 0 < c) :
+  (λ x, x * c) ⁻¹' (Ioi a) = Ioi (a / c) :=
+ext $ λ x, (div_lt_iff h).symm
+
+@[simp] lemma preimage_mul_const_Iic (a : k) {c : k} (h : 0 < c) :
+  (λ x, x * c) ⁻¹' (Iic a) = Iic (a / c) :=
+ext $ λ x, (le_div_iff h).symm
+
+@[simp] lemma preimage_mul_const_Ici (a : k) {c : k} (h : 0 < c) :
+  (λ x, x * c) ⁻¹' (Ici a) = Ici (a / c) :=
+ext $ λ x, (div_le_iff h).symm
+
+@[simp] lemma preimage_mul_const_Ioo (a b : k) {c : k} (h : 0 < c) :
+  (λ x, x * c) ⁻¹' (Ioo a b) = Ioo (a / c) (b / c) :=
+by simp [← Ioi_inter_Iio, h]
+
+@[simp] lemma preimage_mul_const_Ioc (a b : k) {c : k} (h : 0 < c) :
+  (λ x, x * c) ⁻¹' (Ioc a b) = Ioc (a / c) (b / c) :=
+by simp [← Ioi_inter_Iic, h]
+
+@[simp] lemma preimage_mul_const_Ico (a b : k) {c : k} (h : 0 < c) :
+  (λ x, x * c) ⁻¹' (Ico a b) = Ico (a / c) (b / c) :=
+by simp [← Ici_inter_Iio, h]
+
+@[simp] lemma preimage_mul_const_Icc (a b : k) {c : k} (h : 0 < c) :
+  (λ x, x * c) ⁻¹' (Icc a b) = Icc (a / c) (b / c) :=
+by simp [← Ici_inter_Iic, h]
+
+@[simp] lemma preimage_mul_const_Iio_of_neg (a : k) {c : k} (h : c < 0) :
+  (λ x, x * c) ⁻¹' (Iio a) = Ioi (a / c) :=
+ext $ λ x, (div_lt_iff_of_neg h).symm
+
+@[simp] lemma preimage_mul_const_Ioi_of_neg (a : k) {c : k} (h : c < 0) :
+  (λ x, x * c) ⁻¹' (Ioi a) = Iio (a / c) :=
+ext $ λ x, (lt_div_iff_of_neg h).symm
+
+@[simp] lemma preimage_mul_const_Iic_of_neg (a : k) {c : k} (h : c < 0) :
+  (λ x, x * c) ⁻¹' (Iic a) = Ici (a / c) :=
+ext $ λ x, (div_le_iff_of_neg h).symm
+
+@[simp] lemma preimage_mul_const_Ici_of_neg (a : k) {c : k} (h : c < 0) :
+  (λ x, x * c) ⁻¹' (Ici a) = Iic (a / c) :=
+ext $ λ x, (le_div_iff_of_neg h).symm
+
+@[simp] lemma preimage_mul_const_Ioo_of_neg (a b : k) {c : k} (h : c < 0) :
+  (λ x, x * c) ⁻¹' (Ioo a b) = Ioo (b / c) (a / c) :=
+by simp [← Ioi_inter_Iio, h, inter_comm]
+
+@[simp] lemma preimage_mul_const_Ioc_of_neg (a b : k) {c : k} (h : c < 0) :
+  (λ x, x * c) ⁻¹' (Ioc a b) = Ico (b / c) (a / c) :=
+by simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, inter_comm]
+
+@[simp] lemma preimage_mul_const_Ico_of_neg (a b : k) {c : k} (h : c < 0) :
+  (λ x, x * c) ⁻¹' (Ico a b) = Ioc (b / c) (a / c) :=
+by simp [← Ici_inter_Iio, ← Ioi_inter_Iic, h, inter_comm]
+
+@[simp] lemma preimage_mul_const_Icc_of_neg (a b : k) {c : k} (h : c < 0) :
+  (λ x, x * c) ⁻¹' (Icc a b) = Icc (b / c) (a / c) :=
+by simp [← Ici_inter_Iic, h, inter_comm]
+
+@[simp] lemma preimage_const_mul_Iio (a : k) {c : k} (h : 0 < c) :
+  ((*) c) ⁻¹' (Iio a) = Iio (a / c) :=
+ext $ λ x, (lt_div_iff' h).symm
+
+@[simp] lemma preimage_const_mul_Ioi (a : k) {c : k} (h : 0 < c) :
+  ((*) c) ⁻¹' (Ioi a) = Ioi (a / c) :=
+ext $ λ x, (div_lt_iff' h).symm
+
+@[simp] lemma preimage_const_mul_Iic (a : k) {c : k} (h : 0 < c) :
+  ((*) c) ⁻¹' (Iic a) = Iic (a / c) :=
+ext $ λ x, (le_div_iff' h).symm
+
+@[simp] lemma preimage_const_mul_Ici (a : k) {c : k} (h : 0 < c) :
+  ((*) c) ⁻¹' (Ici a) = Ici (a / c) :=
+ext $ λ x, (div_le_iff' h).symm
+
+@[simp] lemma preimage_const_mul_Ioo (a b : k) {c : k} (h : 0 < c) :
+  ((*) c) ⁻¹' (Ioo a b) = Ioo (a / c) (b / c) :=
+by simp [← Ioi_inter_Iio, h]
+
+@[simp] lemma preimage_const_mul_Ioc (a b : k) {c : k} (h : 0 < c) :
+  ((*) c) ⁻¹' (Ioc a b) = Ioc (a / c) (b / c) :=
+by simp [← Ioi_inter_Iic, h]
+
+@[simp] lemma preimage_const_mul_Ico (a b : k) {c : k} (h : 0 < c) :
+  ((*) c) ⁻¹' (Ico a b) = Ico (a / c) (b / c) :=
+by simp [← Ici_inter_Iio, h]
+
+@[simp] lemma preimage_const_mul_Icc (a b : k) {c : k} (h : 0 < c) :
+  ((*) c) ⁻¹' (Icc a b) = Icc (a / c) (b / c) :=
+by simp [← Ici_inter_Iic, h]
+
+@[simp] lemma preimage_const_mul_Iio_of_neg (a : k) {c : k} (h : c < 0) :
+  ((*) c) ⁻¹' (Iio a) = Ioi (a / c) :=
+by simpa only [mul_comm] using preimage_mul_const_Iio_of_neg a h
+
+@[simp] lemma preimage_const_mul_Ioi_of_neg (a : k) {c : k} (h : c < 0) :
+  ((*) c) ⁻¹' (Ioi a) = Iio (a / c) :=
+by simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h
+
+@[simp] lemma preimage_const_mul_Iic_of_neg (a : k) {c : k} (h : c < 0) :
+  ((*) c) ⁻¹' (Iic a) = Ici (a / c) :=
+by simpa only [mul_comm] using preimage_mul_const_Iic_of_neg a h
+
+@[simp] lemma preimage_const_mul_Ici_of_neg (a : k) {c : k} (h : c < 0) :
+  ((*) c) ⁻¹' (Ici a) = Iic (a / c) :=
+by simpa only [mul_comm] using preimage_mul_const_Ici_of_neg a h
+
+@[simp] lemma preimage_const_mul_Ioo_of_neg (a b : k) {c : k} (h : c < 0) :
+  ((*) c) ⁻¹' (Ioo a b) = Ioo (b / c) (a / c) :=
+by simpa only [mul_comm] using preimage_mul_const_Ioo_of_neg a b h
+
+@[simp] lemma preimage_const_mul_Ioc_of_neg (a b : k) {c : k} (h : c < 0) :
+  ((*) c) ⁻¹' (Ioc a b) = Ico (b / c) (a / c) :=
+by simpa only [mul_comm] using preimage_mul_const_Ioc_of_neg a b h
+
+@[simp] lemma preimage_const_mul_Ico_of_neg (a b : k) {c : k} (h : c < 0) :
+  ((*) c) ⁻¹' (Ico a b) = Ioc (b / c) (a / c) :=
+by simpa only [mul_comm] using preimage_mul_const_Ico_of_neg a b h
+
+@[simp] lemma preimage_const_mul_Icc_of_neg (a b : k) {c : k} (h : c < 0) :
+  ((*) c) ⁻¹' (Icc a b) = Icc (b / c) (a / c) :=
+by simpa only [mul_comm] using preimage_mul_const_Icc_of_neg a b h
+
 lemma image_mul_right_Icc' (a b : k) {c : k} (h : 0 < c) :
   (λ x, x * c) '' Icc a b = Icc (a * c) (b * c) :=
 begin
-  ext x,
-  split,
-  { rintros ⟨x, hx, rfl⟩,
-    exact ⟨mul_le_mul_of_nonneg_right hx.1 (le_of_lt h),
-      mul_le_mul_of_nonneg_right hx.2 (le_of_lt h)⟩ },
-  { intro hx,
-    refine ⟨x / c, _, div_mul_cancel x (ne_of_gt h)⟩,
-    exact ⟨le_div_of_mul_le h hx.1, div_le_of_le_mul h (mul_comm b c ▸ hx.2)⟩ }
+  refine ((units.mk0 c (ne_of_gt h)).mul_right.image_eq_preimage _).trans _,
+  simp [h, division_def]
 end
 
 lemma image_mul_right_Icc {a b c : k} (hab : a ≤ b) (hc : 0 ≤ c) :

src/dynamics/circle/rotation_number/translation_number.lean

@@ -128,7 +128,7 @@ ext_iff
 `multiplicative ℝ` to `units circle_deg1_lift`, so the translation by `x` is
 `translation (multiplicative.of_add x)`. -/
 def translate : multiplicative ℝ →* units circle_deg1_lift :=
-by refine (units.map _).comp (to_units $ multiplicative ℝ).to_monoid_hom; exact
+by refine (units.map _).comp to_units.to_monoid_hom; exact
 { to_fun := λ x, ⟨λ y, x.to_add + y, λ y₁ y₂ h, add_le_add_left h _, λ y, (add_assoc _ _ _).symm⟩,
   map_one' := ext $ zero_add,
   map_mul' := λ x y, ext $ add_assoc _ _ }

src/group_theory/group_action.lean

@@ -205,10 +205,10 @@ section
 open mul_action quotient_group
 
 @[simp] lemma inv_smul_smul (c : α) (x : β) : c⁻¹ • c • x = x :=
-(to_units α c).inv_smul_smul x
+(to_units c).inv_smul_smul x
 
 @[simp] lemma smul_inv_smul (c : α) (x : β) : c • c⁻¹ • x = x :=
-(to_units α c).smul_inv_smul x
+(to_units c).smul_inv_smul x
 
 lemma inv_smul_eq_iff {a : α} {x y : β} : a⁻¹ • x = y ↔ x = a • y :=
 begin