<commit_before>/-
Copyright (c) 2017 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>, <NAME>, <NAME>, <NAME>
-/
import algebra.group.basic
import logic.nontrivial

/-!
# Units (i.e., invertible elements) of a multiplicative monoid
-/

universe u
variable {α : Type u}

/-- Units of a monoid, bundled version. An element of a `monoid` is a unit if it has a two-sided
inverse. This version bundles the inverse element so that it can be computed. For a predicate
see `is_unit`. -/
structure units (α : Type u) [monoid α] :=
(val : α)
(inv : α)
(val_inv : val * inv = 1)
(inv_val : inv * val = 1)

/-- Units of an add_monoid, bundled version. An element of an add_monoid is a unit if it has a
    two-sided additive inverse. This version bundles the inverse element so that it can be
    computed. For a predicate see `is_add_unit`. -/
structure add_units (α : Type u) [add_monoid α] :=
(val : α)
(neg : α)
(val_neg : val + neg = 0)
(neg_val : neg + val = 0)

attribute [to_additive add_units] units

namespace units

variables [monoid α]

@[to_additive] instance : has_coe (units α) α := ⟨val⟩

@[to_additive] instance : has_inv (units α) := ⟨λ u, ⟨u.2, u.1, u.4, u.3⟩⟩

/-- See Note [custom simps projection] -/
@[to_additive /-" See Note [custom simps projection] "-/]
def simps.coe (u : units α) : α := u

/-- See Note [custom simps projection] -/
@[to_additive /-" See Note [custom simps projection] "-/]
def simps.coe_inv (u : units α) : α := ↑(u⁻¹)

initialize_simps_projections units (val → coe as_prefix, inv → coe_inv as_prefix)
initialize_simps_projections add_units (val → coe as_prefix, neg → coe_neg as_prefix)

@[simp, to_additive] lemma coe_mk (a : α) (b h₁ h₂) : ↑(units.mk a b h₁ h₂) = a := rfl

@[ext, to_additive] theorem ext :
  function.injective (coe : units α → α)
| ⟨v, i₁, vi₁, iv₁⟩ ⟨v', i₂, vi₂, iv₂⟩ e :=
  by change v = v' at e; subst v'; congr;
      simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

@[norm_cast, to_additive] theorem eq_iff {a b : units α} :
  (a : α) = b ↔ a = b := ext.eq_iff

@[to_additive] theorem ext_iff {a b : units α} :
  a = b ↔ (a : α) = b := eq_iff.symm

@[to_additive] instance [decidable_eq α] : decidable_eq (units α) :=
λ a b, decidable_of_iff' _ ext_iff

@[simp, to_additive] theorem mk_coe (u : units α) (y h₁ h₂) :
  mk (u : α) y h₁ h₂ = u :=
ext rfl

/-- Copy a unit, adjusting definition equalities. -/
@[to_additive /-"Copy an `add_unit`, adjusting definitional equalities."-/, simps]
def copy (u : units α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(u⁻¹)) : units α :=
{ val := val, inv := inv,
  inv_val := hv.symm ▸ hi.symm ▸ u.inv_val, val_inv := hv.symm ▸ hi.symm ▸ u.val_inv }

@[to_additive]
lemma copy_eq (u : units α) (val hv inv hi) :
  u.copy val hv inv hi = u :=
ext hv

/-- Units of a monoid form a group. -/
@[to_additive] instance : group (units α) :=
{ mul := λ u₁ u₂, ⟨u₁.val * u₂.val, u₂.inv * u₁.inv,
    by rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv],
    by rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]⟩,
  one := ⟨1, 1, one_mul 1, one_mul 1⟩,
  mul_one := λ u, ext $ mul_one u,
  one_mul := λ u, ext $ one_mul u,
  mul_assoc := λ u₁ u₂ u₃, ext $ mul_assoc u₁ u₂ u₃,
  inv := has_inv.inv,
  mul_left_inv := λ u, ext u.inv_val }

variables (a b : units α) {c : units α}
@[simp, norm_cast, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl
attribute [norm_cast] add_units.coe_add

@[simp, norm_cast, to_additive] lemma coe_one : ((1 : units α) : α) = 1 := rfl
attribute [norm_cast] add_units.coe_zero

@[simp, norm_cast, to_additive] lemma coe_eq_one {a : units α} : (a : α) = 1 ↔ a = 1 :=
by rw [←units.coe_one, eq_iff]

@[simp, to_additive] lemma inv_mk (x y : α) (h₁ h₂) : (mk x y h₁ h₂)⁻¹ = mk y x h₂ h₁ := rfl

@[to_additive] lemma val_coe : (↑a : α) = a.val := rfl

@[norm_cast, to_additive] lemma coe_inv'' : ((a⁻¹ : units α) : α) = a.inv := rfl
attribute [norm_cast] add_units.coe_neg''

@[simp, to_additive] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _
@[simp, to_additive] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _

@[to_additive] lemma inv_mul_of_eq {u : units α} {a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1 :=
by { rw [←h, u.inv_mul], }<commit_msg>chore(algebra/group/units): Make coercion the simp-normal form of units (#8568)<commit_after>/-
Copyright (c) 2017 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>, <NAME>, <NAME>, <NAME>
-/
import algebra.group.basic
import logic.nontrivial

/-!
# Units (i.e., invertible elements) of a multiplicative monoid
-/

universe u
variable {α : Type u}

/-- Units of a monoid, bundled version. An element of a `monoid` is a unit if it has a two-sided
inverse. This version bundles the inverse element so that it can be computed. For a predicate
see `is_unit`. -/
structure units (α : Type u) [monoid α] :=
(val : α)
(inv : α)
(val_inv : val * inv = 1)
(inv_val : inv * val = 1)

/-- Units of an add_monoid, bundled version. An element of an add_monoid is a unit if it has a
    two-sided additive inverse. This version bundles the inverse element so that it can be
    computed. For a predicate see `is_add_unit`. -/
structure add_units (α : Type u) [add_monoid α] :=
(val : α)
(neg : α)
(val_neg : val + neg = 0)
(neg_val : neg + val = 0)

attribute [to_additive add_units] units

namespace units

variables [monoid α]

@[to_additive] instance : has_coe (units α) α := ⟨val⟩

@[to_additive] instance : has_inv (units α) := ⟨λ u, ⟨u.2, u.1, u.4, u.3⟩⟩

/-- See Note [custom simps projection] -/
@[to_additive /-" See Note [custom simps projection] "-/]
def simps.coe (u : units α) : α := u

/-- See Note [custom simps projection] -/
@[to_additive /-" See Note [custom simps projection] "-/]
def simps.coe_inv (u : units α) : α := ↑(u⁻¹)

initialize_simps_projections units (val → coe as_prefix, inv → coe_inv as_prefix)
initialize_simps_projections add_units (val → coe as_prefix, neg → coe_neg as_prefix)

@[simp, to_additive] lemma coe_mk (a : α) (b h₁ h₂) : ↑(units.mk a b h₁ h₂) = a := rfl

@[ext, to_additive] theorem ext :
  function.injective (coe : units α → α)
| ⟨v, i₁, vi₁, iv₁⟩ ⟨v', i₂, vi₂, iv₂⟩ e :=
  by change v = v' at e; subst v'; congr;
      simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

@[norm_cast, to_additive] theorem eq_iff {a b : units α} :
  (a : α) = b ↔ a = b := ext.eq_iff

@[to_additive] theorem ext_iff {a b : units α} :
  a = b ↔ (a : α) = b := eq_iff.symm

@[to_additive] instance [decidable_eq α] : decidable_eq (units α) :=
λ a b, decidable_of_iff' _ ext_iff

@[simp, to_additive] theorem mk_coe (u : units α) (y h₁ h₂) :
  mk (u : α) y h₁ h₂ = u :=
ext rfl

/-- Copy a unit, adjusting definition equalities. -/
@[to_additive /-"Copy an `add_unit`, adjusting definitional equalities."-/, simps]
def copy (u : units α) (val : α) (hv : val = u) (inv : α) (hi : inv = ↑(u⁻¹)) : units α :=
{ val := val, inv := inv,
  inv_val := hv.symm ▸ hi.symm ▸ u.inv_val, val_inv := hv.symm ▸ hi.symm ▸ u.val_inv }

@[to_additive]
lemma copy_eq (u : units α) (val hv inv hi) :
  u.copy val hv inv hi = u :=
ext hv

/-- Units of a monoid form a group. -/
@[to_additive] instance : group (units α) :=
{ mul := λ u₁ u₂, ⟨u₁.val * u₂.val, u₂.inv * u₁.inv,
    by rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv],
    by rw [mul_assoc, ← mul_assoc u₁.inv, inv_val, one_mul, inv_val]⟩,
  one := ⟨1, 1, one_mul 1, one_mul 1⟩,
  mul_one := λ u, ext $ mul_one u,
  one_mul := λ u, ext $ one_mul u,
  mul_assoc := λ u₁ u₂ u₃, ext $ mul_assoc u₁ u₂ u₃,
  inv := has_inv.inv,
  mul_left_inv := λ u, ext u.inv_val }

variables (a b : units α) {c : units α}
@[simp, norm_cast, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl
attribute [norm_cast] add_units.coe_add

@[simp, norm_cast, to_additive] lemma coe_one : ((1 : units α) : α) = 1 := rfl
attribute [norm_cast] add_units.coe_zero

@[simp, norm_cast, to_additive] lemma coe_eq_one {a : units α} : (a : α) = 1 ↔ a = 1 :=
by rw [←units.coe_one, eq_iff]

@[simp, to_additive] lemma inv_mk (x y : α) (h₁ h₂) : (mk x y h₁ h₂)⁻¹ = mk y x h₂ h₁ := rfl

@[simp, to_additive] lemma val_eq_coe : a.val = (↑a : α) := rfl

@[simp, to_additive] lemma inv_eq_coe_inv : a.inv = ((a⁻¹ : units α) : α) := rfl

@[simp, to_additive] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _
@[simp, to_additive] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _

@[to_additive] lemma inv_mul_of_eq {u : units α} {a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1 :=
by { rw [←h, u.inv_mul], }
{'fraction_non_alphanumeric': 0.1550180253517851, 'fraction_numerical': 0.006279799976741482, 'mean_word_length': 3.4034818228366617, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '638781', 'n_tokens_mistral': 3880, 'n_tokens_neox': 3723, 'n_words': 1252}