import algebra.group.units

import algebra.group_with_zero.units.lemmas

import algebra.ring.defs

universes u

variables {α : Type u}

class invertible [has_mul α] [has_one α] (a : α) : Type u :=

(inv_of : α) (inv_of_mul_self : inv_of * a = 1) (mul_inv_of_self : a * inv_of = 1)

notation `⅟`:1034 := invertible.inv_of

lemma inv_of_mul_self [has_mul α] [has_one α] (a : α) [invertible a] : ⅟a * a = 1 :=

invertible.inv_of_mul_self

lemma mul_inv_of_self [has_mul α] [has_one α] (a : α) [invertible a] : a * ⅟a = 1 :=

invertible.mul_inv_of_self

lemma inv_of_mul_self_assoc [monoid α] (a b : α) [invertible a] : ⅟a * (a * b) = b :=

by rw [←mul_assoc, inv_of_mul_self, one_mul]

lemma mul_inv_of_self_assoc [monoid α] (a b : α) [invertible a] : a * (⅟a * b) = b :=

by rw [←mul_assoc, mul_inv_of_self, one_mul]

lemma mul_inv_of_mul_self_cancel [monoid α] (a b : α) [invertible b] : a * ⅟b * b = a :=

by simp [mul_assoc]

lemma mul_mul_inv_of_self_cancel [monoid α] (a b : α) [invertible b] : a * b * ⅟b = a :=

by simp [mul_assoc]

lemma inv_of_eq_right_inv [monoid α] {a b : α} [invertible a] (hac : a * b = 1) : ⅟a = b :=

left_inv_eq_right_inv (inv_of_mul_self _) hac

lemma inv_of_eq_left_inv [monoid α] {a b : α} [invertible a] (hac : b * a = 1) : ⅟a = b :=

(left_inv_eq_right_inv hac (mul_inv_of_self _)).symm

lemma invertible_unique {α : Type u} [monoid α] (a b : α) [invertible a] [invertible b]

(h : a = b) :

⅟a = ⅟b :=

by { apply inv_of_eq_right_inv, rw [h, mul_inv_of_self], }

instance [monoid α] (a : α) : subsingleton (invertible a) :=

⟨ λ ⟨b, hba, hab⟩ ⟨c, hca, hac⟩, by { congr, exact left_inv_eq_right_inv hba hac } ⟩

def invertible.copy' [mul_one_class α] {r : α} (hr : invertible r) (s : α) (si : α)

(hs : s = r) (hsi : si = ⅟r) :

invertible s :=

{ inv_of := si,

inv_of_mul_self := by rw [hs, hsi, inv_of_mul_self],

mul_inv_of_self := by rw [hs, hsi, mul_inv_of_self] }

def invertible.copy [mul_one_class α] {r : α} (hr : invertible r) (s : α) (hs : s = r) :

invertible s :=

hr.copy' _ _ hs rfl

def unit_of_invertible [monoid α] (a : α) [invertible a] : αˣ :=

{ val := a,

inv := ⅟a,

val_inv := by simp,

inv_val := by simp, }

lemma is_unit_of_invertible [monoid α] (a : α) [invertible a] : is_unit a :=

⟨unit_of_invertible a, rfl⟩

def units.invertible [monoid α] (u : αˣ) : invertible (u : α) :=

{ inv_of := ↑(u⁻¹), inv_of_mul_self := u.inv_mul, mul_inv_of_self := u.mul_inv }

@[simp] lemma inv_of_units [monoid α] (u : αˣ) [invertible (u : α)] : ⅟(u : α) = ↑(u⁻¹) :=

inv_of_eq_right_inv u.mul_inv

lemma is_unit.nonempty_invertible [monoid α] {a : α} (h : is_unit a) : nonempty (invertible a) :=

let ⟨x, hx⟩ := h in ⟨x.invertible.copy _ hx.symm⟩

noncomputable def is_unit.invertible [monoid α] {a : α} (h : is_unit a) : invertible a :=

classical.choice h.nonempty_invertible

@[simp] lemma nonempty_invertible_iff_is_unit [monoid α] (a : α) :

nonempty (invertible a) ↔ is_unit a :=

⟨nonempty.rec $ @is_unit_of_invertible _ _ _, is_unit.nonempty_invertible⟩

def invertible_of_group [group α] (a : α) : invertible a :=

⟨a⁻¹, inv_mul_self a, mul_inv_self a⟩

@[simp] lemma inv_of_eq_group_inv [group α] (a : α) [invertible a] : ⅟a = a⁻¹ :=

inv_of_eq_right_inv (mul_inv_self a)

def invertible_one [monoid α] : invertible (1 : α) :=

⟨1, mul_one _, one_mul _⟩

@[simp] lemma inv_of_one [monoid α] [invertible (1 : α)] : ⅟(1 : α) = 1 :=

inv_of_eq_right_inv (mul_one _)

def invertible_neg [has_mul α] [has_one α] [has_distrib_neg α] (a : α) [invertible a] :

invertible (-a) := ⟨-⅟a, by simp, by simp ⟩

@[simp] lemma inv_of_neg [monoid α] [has_distrib_neg α] (a : α) [invertible a] [invertible (-a)] :

⅟(-a) = -⅟a :=

inv_of_eq_right_inv (by simp)

@[simp] lemma one_sub_inv_of_two [ring α] [invertible (2:α)] : 1 - (⅟2:α) = ⅟2 :=

(is_unit_of_invertible (2:α)).mul_right_inj.1 $

by rw [mul_sub, mul_inv_of_self, mul_one, bit0, add_sub_cancel]

@[simp] lemma inv_of_two_add_inv_of_two [non_assoc_semiring α] [invertible (2 : α)] :

(⅟2 : α) + (⅟2 : α) = 1 :=

by rw [←two_mul, mul_inv_of_self]

instance invertible_inv_of [has_one α] [has_mul α] {a : α} [invertible a] : invertible (⅟a) :=

⟨ a, mul_inv_of_self a, inv_of_mul_self a ⟩

@[simp] lemma inv_of_inv_of [monoid α] (a : α) [invertible a] [invertible (⅟a)] : ⅟(⅟a) = a :=

inv_of_eq_right_inv (inv_of_mul_self _)

@[simp] lemma inv_of_inj [monoid α] {a b : α} [invertible a] [invertible b] :

⅟ a = ⅟ b ↔ a = b :=

⟨invertible_unique _ _, invertible_unique _ _⟩

def invertible_mul [monoid α] (a b : α) [invertible a] [invertible b] : invertible (a * b) :=

⟨ ⅟b * ⅟a, by simp [←mul_assoc], by simp [←mul_assoc] ⟩

@[simp] lemma inv_of_mul [monoid α] (a b : α) [invertible a] [invertible b] [invertible (a * b)] :

⅟(a * b) = ⅟b * ⅟a :=

inv_of_eq_right_inv (by simp [←mul_assoc])

@[reducible] def invertible.mul [monoid α] {a b : α} (ha : invertible a) (hb : invertible b) :

invertible (a * b) :=

invertible_mul _ _

theorem commute.inv_of_right [monoid α] {a b : α} [invertible b] (h : commute a b) :

commute a (⅟b) :=

calc a * (⅟b) = (⅟b) * (b * a * (⅟b)) : by simp [mul_assoc]

... = (⅟b) * (a * b * ((⅟b))) : by rw h.eq

... = (⅟b) * a : by simp [mul_assoc]

theorem commute.inv_of_left [monoid α] {a b : α} [invertible b] (h : commute b a) :

commute (⅟b) a :=

calc (⅟b) * a = (⅟b) * (a * b * (⅟b)) : by simp [mul_assoc]

... = (⅟b) * (b * a * (⅟b)) : by rw h.eq

... = a * (⅟b) : by simp [mul_assoc]

lemma commute_inv_of {M : Type*} [has_one M] [has_mul M] (m : M) [invertible m] :

commute m (⅟m) :=

calc m * ⅟m = 1 : mul_inv_of_self m

... = ⅟ m * m : (inv_of_mul_self m).symm

lemma nonzero_of_invertible [mul_zero_one_class α] (a : α) [nontrivial α] [invertible a] : a ≠ 0 :=

λ ha, zero_ne_one $ calc 0 = ⅟a * a : by simp [ha]

... = 1 : inv_of_mul_self a

@[priority 100] instance invertible.ne_zero [mul_zero_one_class α] [nontrivial α] (a : α)

[invertible a] : ne_zero a := ⟨nonzero_of_invertible a⟩

section monoid

variables [monoid α]

@[reducible] def invertible_of_invertible_mul (a b : α) [invertible a] [invertible (a * b)] :

invertible b :=

{ inv_of := ⅟(a * b) * a,

inv_of_mul_self := by rw [mul_assoc, inv_of_mul_self],

mul_inv_of_self := by rw [←(is_unit_of_invertible a).mul_right_inj, ←mul_assoc, ←mul_assoc,

mul_inv_of_self, mul_one, one_mul] }

@[reducible] def invertible_of_mul_invertible (a b : α) [invertible (a * b)] [invertible b] :

invertible a :=

{ inv_of := b * ⅟(a * b),

inv_of_mul_self := by rw [←(is_unit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc,

inv_of_mul_self, mul_one, one_mul],

mul_inv_of_self := by rw [←mul_assoc, mul_inv_of_self] }

@[simps] def invertible.mul_left {a : α} (ha : invertible a) (b : α) :

invertible b ≃ invertible (a * b) :=

{ to_fun := λ hb, by exactI invertible_mul a b,

inv_fun := λ hab, by exactI invertible_of_invertible_mul a _,

left_inv := λ hb, subsingleton.elim _ _,

right_inv := λ hab, subsingleton.elim _ _, }

@[simps] def invertible.mul_right (a : α) {b : α} (ha : invertible b) :

invertible a ≃ invertible (a * b) :=

{ to_fun := λ hb, by exactI invertible_mul a b,

inv_fun := λ hab, by exactI invertible_of_mul_invertible _ b,

left_inv := λ hb, subsingleton.elim _ _,

right_inv := λ hab, subsingleton.elim _ _, }

end monoid

section monoid_with_zero

variable [monoid_with_zero α]

@[simp] lemma ring.inverse_invertible (x : α) [invertible x] : ring.inverse x = ⅟x :=

ring.inverse_unit (unit_of_invertible _)

end monoid_with_zero

section group_with_zero

variable [group_with_zero α]

def invertible_of_nonzero {a : α} (h : a ≠ 0) : invertible a :=

⟨ a⁻¹, inv_mul_cancel h, mul_inv_cancel h ⟩

@[simp] lemma inv_of_eq_inv (a : α) [invertible a] : ⅟a = a⁻¹ :=

inv_of_eq_right_inv (mul_inv_cancel (nonzero_of_invertible a))

@[simp] lemma inv_mul_cancel_of_invertible (a : α) [invertible a] : a⁻¹ * a = 1 :=

inv_mul_cancel (nonzero_of_invertible a)

@[simp] lemma mul_inv_cancel_of_invertible (a : α) [invertible a] : a * a⁻¹ = 1 :=

mul_inv_cancel (nonzero_of_invertible a)

@[simp] lemma div_mul_cancel_of_invertible (a b : α) [invertible b] : a / b * b = a :=

div_mul_cancel a (nonzero_of_invertible b)

@[simp] lemma mul_div_cancel_of_invertible (a b : α) [invertible b] : a * b / b = a :=

mul_div_cancel a (nonzero_of_invertible b)

@[simp] lemma div_self_of_invertible (a : α) [invertible a] : a / a = 1 :=

div_self (nonzero_of_invertible a)

def invertible_div (a b : α) [invertible a] [invertible b] : invertible (a / b) :=

⟨b / a, by simp [←mul_div_assoc], by simp [←mul_div_assoc]⟩

@[simp] lemma inv_of_div (a b : α) [invertible a] [invertible b] [invertible (a / b)] :

⅟(a / b) = b / a :=

inv_of_eq_right_inv (by simp [←mul_div_assoc])

def invertible_inv {a : α} [invertible a] : invertible (a⁻¹) :=

⟨ a, by simp, by simp ⟩

end group_with_zero

def invertible.map {R : Type*} {S : Type*} {F : Type*} [mul_one_class R] [mul_one_class S]

[monoid_hom_class F R S] (f : F) (r : R) [invertible r] :

invertible (f r) :=

{ inv_of := f (⅟r),

inv_of_mul_self := by rw [←map_mul, inv_of_mul_self, map_one],

mul_inv_of_self := by rw [←map_mul, mul_inv_of_self, map_one] }

lemma map_inv_of {R : Type*} {S : Type*} {F : Type*} [mul_one_class R] [monoid S]

[monoid_hom_class F R S] (f : F) (r : R) [invertible r] [invertible (f r)] :

f (⅟r) = ⅟(f r) :=

by { letI := invertible.map f r, convert rfl }

@[simps {attrs := []}]

def invertible.of_left_inverse {R : Type*} {S : Type*} {G : Type*}

[mul_one_class R] [mul_one_class S] [monoid_hom_class G S R]

(f : R → S) (g : G) (r : R) (h : function.left_inverse g f) [invertible (f r)] :

invertible r :=

(invertible.map g (f r)).copy _ (h r).symm

def invertible_equiv_of_left_inverse {R : Type*} {S : Type*} {F G : Type*}

[monoid R] [monoid S] [monoid_hom_class F R S] [monoid_hom_class G S R]

(f : F) (g : G) (r : R) (h : function.left_inverse g f) :

invertible (f r) ≃ invertible r :=

{ to_fun := λ _, by exactI invertible.of_left_inverse f _ _ h,

inv_fun := λ _, by exactI invertible.map f _,

left_inv := λ x, subsingleton.elim _ _,

right_inv := λ x, subsingleton.elim _ _ }