import algebra.group.prod

import algebra.hom.equiv.basic

import data.setoid.basic

import group_theory.submonoid.operations

variables (M : Type*) {N : Type*} {P : Type*}

open function setoid

structure add_con [has_add M] extends setoid M :=

(add' : ∀ {w x y z}, r w x → r y z → r (w + y) (x + z))

@[to_additive add_con] structure con [has_mul M] extends setoid M :=

(mul' : ∀ {w x y z}, r w x → r y z → r (w * y) (x * z))

add_decl_doc add_con.to_setoid

add_decl_doc con.to_setoid

variables {M}

inductive add_con_gen.rel [has_add M] (r : M → M → Prop) : M → M → Prop

| of : Π x y, r x y → add_con_gen.rel x y

| refl : Π x, add_con_gen.rel x x

| symm : Π x y, add_con_gen.rel x y → add_con_gen.rel y x

| trans : Π x y z, add_con_gen.rel x y → add_con_gen.rel y z → add_con_gen.rel x z

| add : Π w x y z, add_con_gen.rel w x → add_con_gen.rel y z → add_con_gen.rel (w + y) (x + z)

inductive con_gen.rel [has_mul M] (r : M → M → Prop) : M → M → Prop

| of : Π x y, r x y → con_gen.rel x y

| refl : Π x, con_gen.rel x x

| symm : Π x y, con_gen.rel x y → con_gen.rel y x

| trans : Π x y z, con_gen.rel x y → con_gen.rel y z → con_gen.rel x z

| mul : Π w x y z, con_gen.rel w x → con_gen.rel y z → con_gen.rel (w * y) (x * z)

def con_gen [has_mul M] (r : M → M → Prop) : con M :=

⟨⟨con_gen.rel r, ⟨con_gen.rel.refl, con_gen.rel.symm, con_gen.rel.trans⟩⟩, con_gen.rel.mul⟩

namespace con

variables [has_mul M] [has_mul N] [has_mul P] (c : con M)

instance : inhabited (con M) :=

⟨con_gen empty_relation⟩

instance : has_coe_to_fun (con M) (λ _, M → M → Prop) := ⟨λ c, λ x y, @setoid.r _ c.to_setoid x y⟩

@[simp, to_additive] lemma rel_eq_coe (c : con M) : c.r = c := rfl

protected lemma refl (x) : c x x := c.to_setoid.refl' x

protected lemma symm : ∀ {x y}, c x y → c y x := λ _ _ h, c.to_setoid.symm' h

protected lemma trans : ∀ {x y z}, c x y → c y z → c x z :=

λ _ _ _ h, c.to_setoid.trans' h

protected lemma mul : ∀ {w x y z}, c w x → c y z → c (w * y) (x * z) :=

λ _ _ _ _ h1 h2, c.mul' h1 h2

@[simp, to_additive] lemma rel_mk {s : setoid M} {h a b} :

con.mk s h a b ↔ r a b :=

iff.rfl

instance : has_mem (M × M) (con M) := ⟨λ x c, c x.1 x.2⟩

variables {c}

lemma ext' {c d : con M} (H : c.r = d.r) : c = d :=

by { rcases c with ⟨⟨⟩⟩, rcases d with ⟨⟨⟩⟩, cases H, congr, }

lemma ext {c d : con M} (H : ∀ x y, c x y ↔ d x y) : c = d :=

ext' $ by ext; apply H

lemma to_setoid_inj {c d : con M} (H : c.to_setoid = d.to_setoid) : c = d :=

ext $ ext_iff.1 H

lemma ext_iff {c d : con M} : (∀ x y, c x y ↔ d x y) ↔ c = d :=

⟨ext, λ h _ _, h ▸ iff.rfl⟩

lemma ext'_iff {c d : con M} : c.r = d.r ↔ c = d :=

⟨ext', λ h, h ▸ rfl⟩

def mul_ker (f : M → P) (h : ∀ x y, f (x * y) = f x * f y) : con M :=

{ to_setoid := setoid.ker f,

mul' := λ _ _ _ _ h1 h2, by { dsimp [setoid.ker, on_fun] at *, rw [h, h1, h2, h], } }

protected def prod (c : con M) (d : con N) : con (M × N) :=

{ mul' := λ _ _ _ _ h1 h2, ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩, ..c.to_setoid.prod d.to_setoid }

def pi {ι : Type*} {f : ι → Type*} [Π i, has_mul (f i)]

(C : Π i, con (f i)) : con (Π i, f i) :=

{ mul' := λ _ _ _ _ h1 h2 i, (C i).mul (h1 i) (h2 i), ..@pi_setoid _ _ $ λ i, (C i).to_setoid }

variables (c)

protected def quotient := quotient $ c.to_setoid

instance : has_coe_t M c.quotient := ⟨@quotient.mk _ c.to_setoid⟩

priority 500] -- Lower the priority since it unifies with any quotient type.

instance [d : ∀ a b, decidable (c a b)] : decidable_eq c.quotient :=

@quotient.decidable_eq M c.to_setoid d

@[simp, to_additive] lemma quot_mk_eq_coe {M : Type*} [has_mul M] (c : con M) (x : M) :

quot.mk c x = (x : c.quotient) :=

rfl

protected def lift_on {β} {c : con M} (q : c.quotient) (f : M → β)

(h : ∀ a b, c a b → f a = f b) : β := quotient.lift_on' q f h

protected def lift_on₂ {β} {c : con M} (q r : c.quotient) (f : M → M → β)

(h : ∀ a₁ a₂ b₁ b₂, c a₁ b₁ → c a₂ b₂ → f a₁ a₂ = f b₁ b₂) : β := quotient.lift_on₂' q r f h

protected def hrec_on₂ {cM : con M} {cN : con N} {φ : cM.quotient → cN.quotient → Sort*}

(a : cM.quotient) (b : cN.quotient)

(f : Π (x : M) (y : N), φ x y) (h : ∀ x y x' y', cM x x' → cN y y' → f x y == f x' y') :

φ a b :=

quotient.hrec_on₂' a b f h

@[simp, to_additive] lemma hrec_on₂_coe {cM : con M} {cN : con N}

{φ : cM.quotient → cN.quotient → Sort*} (a : M) (b : N)

(f : Π (x : M) (y : N), φ x y) (h : ∀ x y x' y', cM x x' → cN y y' → f x y == f x' y') :

con.hrec_on₂ ↑a ↑b f h = f a b :=

rfl

variables {c}

protected lemma induction_on {C : c.quotient → Prop} (q : c.quotient) (H : ∀ x : M, C x) : C q :=

quotient.induction_on' q H

protected lemma induction_on₂ {d : con N} {C : c.quotient → d.quotient → Prop}

(p : c.quotient) (q : d.quotient) (H : ∀ (x : M) (y : N), C x y) : C p q :=

quotient.induction_on₂' p q H

variables (c)

protected lemma eq {a b : M} : (a : c.quotient) = b ↔ c a b :=

quotient.eq'

instance has_mul : has_mul c.quotient :=

⟨quotient.map₂' (*) $ λ _ _ h1 _ _ h2, c.mul h1 h2⟩

lemma mul_ker_mk_eq : mul_ker (coe : M → c.quotient) (λ x y, rfl) = c :=

ext $ λ x y, quotient.eq'

variables {c}

lemma coe_mul (x y : M) : (↑(x * y) : c.quotient) = ↑x * ↑y := rfl

protected lemma lift_on_coe {β} (c : con M) (f : M → β)

(h : ∀ a b, c a b → f a = f b) (x : M) :

con.lift_on (x : c.quotient) f h = f x := rfl

protected def congr {c d : con M} (h : c = d) : c.quotient ≃* d.quotient :=

{ map_mul' := λ x y, by rcases x; rcases y; refl,

..quotient.congr (equiv.refl M) $ by apply ext_iff.2 h }

instance : has_le (con M) := ⟨λ c d, ∀ ⦃x y⦄, c x y → d x y⟩

theorem le_def {c d : con M} : c ≤ d ↔ ∀ {x y}, c x y → d x y := iff.rfl

instance : has_Inf (con M) :=

⟨λ S, ⟨⟨λ x y, ∀ c : con M, c ∈ S → c x y,

⟨λ x c hc, c.refl x, λ _ _ h c hc, c.symm $ h c hc,

λ _ _ _ h1 h2 c hc, c.trans (h1 c hc) $ h2 c hc⟩⟩,

λ _ _ _ _ h1 h2 c hc, c.mul (h1 c hc) $ h2 c hc⟩⟩

lemma Inf_to_setoid (S : set (con M)) : (Inf S).to_setoid = Inf (to_setoid '' S) :=

setoid.ext' $ λ x y, ⟨λ h r ⟨c, hS, hr⟩, by rw ←hr; exact h c hS,

λ h c hS, h c.to_setoid ⟨c, hS, rfl⟩⟩

lemma Inf_def (S : set (con M)) : ⇑(Inf S) = Inf (@set.image (con M) (M → M → Prop) coe_fn S) :=

by { ext, simp only [Inf_image, infi_apply, infi_Prop_eq], refl }

instance : partial_order (con M) :=

{ le := (≤),

lt := λ c d, c ≤ d ∧ ¬d ≤ c,

le_refl := λ c _ _, id,

le_trans := λ c1 c2 c3 h1 h2 x y h, h2 $ h1 h,

lt_iff_le_not_le := λ _ _, iff.rfl,

le_antisymm := λ c d hc hd, ext $ λ x y, ⟨λ h, hc h, λ h, hd h⟩ }

instance : complete_lattice (con M) :=

{ inf := λ c d, ⟨(c.to_setoid ⊓ d.to_setoid), λ _ _ _ _ h1 h2, ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩⟩,

inf_le_left := λ _ _ _ _ h, h.1,

inf_le_right := λ _ _ _ _ h, h.2,

le_inf := λ _ _ _ hb hc _ _ h, ⟨hb h, hc h⟩,

top := { mul' := by tauto, ..setoid.complete_lattice.top},

le_top := λ _ _ _ h, trivial,

bot := { mul' := λ _ _ _ _ h1 h2, h1 ▸ h2 ▸ rfl, ..setoid.complete_lattice.bot},

bot_le := λ c x y h, h ▸ c.refl x,

.. complete_lattice_of_Inf (con M) $ assume s,

⟨λ r hr x y h, (h : ∀ r ∈ s, (r : con M) x y) r hr, λ r hr x y h r' hr', hr hr' h⟩ }

lemma inf_def {c d : con M} : (c ⊓ d).r = c.r ⊓ d.r := rfl

theorem inf_iff_and {c d : con M} {x y} : (c ⊓ d) x y ↔ c x y ∧ d x y := iff.rfl

theorem con_gen_eq (r : M → M → Prop) :

con_gen r = Inf {s : con M | ∀ x y, r x y → s x y} :=

le_antisymm

(λ x y H, con_gen.rel.rec_on H (λ _ _ h _ hs, hs _ _ h) (con.refl _) (λ _ _ _, con.symm _)

(λ _ _ _ _ _, con.trans _)

$ λ w x y z _ _ h1 h2 c hc, c.mul (h1 c hc) $ h2 c hc)

(Inf_le (λ _ _, con_gen.rel.of _ _))

theorem con_gen_le {r : M → M → Prop} {c : con M} (h : ∀ x y, r x y → @setoid.r _ c.to_setoid x y) :

con_gen r ≤ c :=

by rw con_gen_eq; exact Inf_le h

theorem con_gen_mono {r s : M → M → Prop} (h : ∀ x y, r x y → s x y) :

con_gen r ≤ con_gen s :=

con_gen_le $ λ x y hr, con_gen.rel.of _ _ $ h x y hr

lemma con_gen_of_con (c : con M) : con_gen c = c :=

le_antisymm (by rw con_gen_eq; exact Inf_le (λ _ _, id)) con_gen.rel.of

lemma con_gen_idem (r : M → M → Prop) :

con_gen (con_gen r) = con_gen r :=

con_gen_of_con _

lemma sup_eq_con_gen (c d : con M) :

c ⊔ d = con_gen (λ x y, c x y ∨ d x y) :=

rw con_gen_eq,

apply congr_arg Inf,

simp only [le_def, or_imp_distrib, ← forall_and_distrib]

lemma sup_def {c d : con M} : c ⊔ d = con_gen (c.r ⊔ d.r) :=

by rw sup_eq_con_gen; refl

lemma Sup_eq_con_gen (S : set (con M)) :

Sup S = con_gen (λ x y, ∃ c : con M, c ∈ S ∧ c x y) :=

rw con_gen_eq,

apply congr_arg Inf,

ext,

exact ⟨λ h _ _ ⟨r, hr⟩, h hr.1 hr.2,

λ h r hS _ _ hr, h _ _ ⟨r, hS, hr⟩⟩,

lemma Sup_def {S : set (con M)} :

Sup S = con_gen (Sup (@set.image (con M) (M → M → Prop) coe_fn S)) :=

rw [Sup_eq_con_gen, Sup_image],

congr' with x y,

simp only [Sup_image, supr_apply, supr_Prop_eq, exists_prop, rel_eq_coe]

variables (M)

protected def gi :

@galois_insertion (M → M → Prop) (con M) _ _ con_gen coe_fn :=

{ choice := λ r h, con_gen r,

gc := λ r c, ⟨λ H _ _ h, H $ con_gen.rel.of _ _ h, λ H, con_gen_of_con c ▸ con_gen_mono H⟩,

le_l_u := λ x, (con_gen_of_con x).symm ▸ le_refl x,

choice_eq := λ _ _, rfl }

variables {M} (c)

def map_gen (f : M → N) : con N :=

con_gen $ λ x y, ∃ a b, f a = x ∧ f b = y ∧ c a b

def map_of_surjective (f : M → N) (H : ∀ x y, f (x * y) = f x * f y) (h : mul_ker f H ≤ c)

(hf : surjective f) : con N :=

{ mul' := λ w x y z ⟨a, b, hw, hx, h1⟩ ⟨p, q, hy, hz, h2⟩,

⟨a * p, b * q, by rw [H, hw, hy], by rw [H, hx, hz], c.mul h1 h2⟩,

..c.to_setoid.map_of_surjective f h hf }

lemma map_of_surjective_eq_map_gen {c : con M} {f : M → N} (H : ∀ x y, f (x * y) = f x * f y)

(h : mul_ker f H ≤ c) (hf : surjective f) :

c.map_gen f = c.map_of_surjective f H h hf :=

by rw ←con_gen_of_con (c.map_of_surjective f H h hf); refl

def comap (f : M → N) (H : ∀ x y, f (x * y) = f x * f y) (c : con N) : con M :=

{ mul' := λ w x y z h1 h2, show c (f (w * y)) (f (x * z)), by rw [H, H]; exact c.mul h1 h2,

..c.to_setoid.comap f }

@[simp, to_additive] lemma comap_rel {f : M → N} (H : ∀ x y, f (x * y) = f x * f y)

{c : con N} {x y : M} :

comap f H c x y ↔ c (f x) (f y) :=

iff.rfl

open _root_.quotient

def correspondence : {d // c ≤ d} ≃o (con c.quotient) :=

{ to_fun := λ d, d.1.map_of_surjective coe _

(by rw mul_ker_mk_eq; exact d.2) $ @exists_rep _ c.to_setoid,

inv_fun := λ d, ⟨comap (coe : M → c.quotient) (λ x y, rfl) d, λ _ _ h,

show d _ _, by rw c.eq.2 h; exact d.refl _ ⟩,

left_inv := λ d, subtype.ext_iff_val.2 $ ext $ λ _ _,

⟨λ h, let ⟨a, b, hx, hy, H⟩ := h in

d.1.trans (d.1.symm $ d.2 $ c.eq.1 hx) $ d.1.trans H $ d.2 $ c.eq.1 hy,

λ h, ⟨_, _, rfl, rfl, h⟩⟩,

right_inv := λ d, let Hm : mul_ker (coe : M → c.quotient) (λ x y, rfl) ≤

comap (coe : M → c.quotient) (λ x y, rfl) d :=

λ x y h, show d _ _, by rw mul_ker_mk_eq at h; exact c.eq.2 h ▸ d.refl _ in

ext $ λ x y, ⟨λ h, let ⟨a, b, hx, hy, H⟩ := h in hx ▸ hy ▸ H,

con.induction_on₂ x y $ λ w z h, ⟨w, z, rfl, rfl, h⟩⟩,

map_rel_iff' := λ s t, ⟨λ h _ _ hs, let ⟨a, b, hx, hy, ht⟩ := h ⟨_, _, rfl, rfl, hs⟩ in

t.1.trans (t.1.symm $ t.2 $ eq_rel.1 hx) $ t.1.trans ht $ t.2 $ eq_rel.1 hy,

λ h _ _ hs, let ⟨a, b, hx, hy, Hs⟩ := hs in ⟨a, b, hx, hy, h Hs⟩⟩ }

section mul_one_class

variables {M} [mul_one_class M] [mul_one_class N] [mul_one_class P] (c : con M)

instance mul_one_class : mul_one_class c.quotient :=

{ one := ((1 : M) : c.quotient),

mul := (*),

mul_one := λ x, quotient.induction_on' x $ λ _, congr_arg (coe : M → c.quotient) $ mul_one _,

one_mul := λ x, quotient.induction_on' x $ λ _, congr_arg (coe : M → c.quotient) $ one_mul _ }

variables {c}

lemma coe_one : ((1 : M) : c.quotient) = 1 := rfl

variables (M c)

protected def submonoid : submonoid (M × M) :=

{ carrier := { x | c x.1 x.2 },

one_mem' := c.iseqv.1 1,

mul_mem' := λ _ _, c.mul }

variables {M c}

def of_submonoid (N : submonoid (M × M)) (H : equivalence (λ x y, (x, y) ∈ N)) : con M :=

{ r := λ x y, (x, y) ∈ N,

iseqv := H,

mul' := λ _ _ _ _, N.mul_mem }

instance to_submonoid : has_coe (con M) (submonoid (M × M)) := ⟨λ c, c.submonoid M⟩

@[to_additive] lemma mem_coe {c : con M} {x y} :

(x, y) ∈ (↑c : submonoid (M × M)) ↔ (x, y) ∈ c := iff.rfl

theorem to_submonoid_inj (c d : con M) (H : (c : submonoid (M × M)) = d) : c = d :=

ext $ λ x y, show (x, y) ∈ (c : submonoid (M × M)) ↔ (x, y) ∈ ↑d, by rw H

lemma le_iff {c d : con M} : c ≤ d ↔ (c : submonoid (M × M)) ≤ d :=

⟨λ h x H, h H, λ h x y hc, h $ show (x, y) ∈ c, from hc⟩

def ker (f : M →* P) : con M := mul_ker f f.3

lemma ker_rel (f : M →* P) {x y} : ker f x y ↔ f x = f y := iff.rfl

instance quotient.inhabited : inhabited c.quotient := ⟨((1 : M) : c.quotient)⟩

variables (c)

def mk' : M →* c.quotient := ⟨coe, rfl, λ _ _, rfl⟩

variables (x y : M)

lemma mk'_ker : ker c.mk' = c := ext $ λ _ _, c.eq

variables {c}

lemma mk'_surjective : surjective c.mk' :=

quotient.surjective_quotient_mk'

@[simp, to_additive] lemma coe_mk' : (c.mk' : M → c.quotient) = coe := rfl

@[simp, to_additive] lemma mrange_mk' : c.mk'.mrange = ⊤ :=

monoid_hom.mrange_top_iff_surjective.2 mk'_surjective

lemma ker_apply_eq_preimage {f : M →* P} (x) : (ker f) x = f ⁻¹' {f x} :=

set.ext $ λ x,

⟨λ h, set.mem_preimage.2 $ set.mem_singleton_iff.2 h.symm,

λ h, (set.mem_singleton_iff.1 $ set.mem_preimage.1 h).symm⟩

lemma comap_eq {f : N →* M} : comap f f.map_mul c = ker (c.mk'.comp f) :=

ext $ λ x y, show c _ _ ↔ c.mk' _ = c.mk' _, by rw ←c.eq; refl

variables (c) (f : M →* P)

def lift (H : c ≤ ker f) : c.quotient →* P :=

{ to_fun := λ x, con.lift_on x f $ λ _ _ h, H h,

map_one' := by rw ←f.map_one; refl,

map_mul' := λ x y, con.induction_on₂ x y $ λ m n, f.map_mul m n ▸ rfl }

variables {c f}

lemma lift_mk' (H : c ≤ ker f) (x) :

c.lift f H (c.mk' x) = f x := rfl

lemma lift_coe (H : c ≤ ker f) (x : M) :

c.lift f H x = f x := rfl

theorem lift_comp_mk' (H : c ≤ ker f) :

(c.lift f H).comp c.mk' = f := by ext; refl

lemma lift_apply_mk' (f : c.quotient →* P) :

c.lift (f.comp c.mk') (λ x y h, show f ↑x = f ↑y, by rw c.eq.2 h) = f :=

by ext; rcases x; refl

lemma lift_funext (f g : c.quotient →* P) (h : ∀ a : M, f a = g a) : f = g :=

rw [←lift_apply_mk' f, ←lift_apply_mk' g],

congr' 1,

exact monoid_hom.ext_iff.2 h,

theorem lift_unique (H : c ≤ ker f) (g : c.quotient →* P)

(Hg : g.comp c.mk' = f) : g = c.lift f H :=

lift_funext g (c.lift f H) $ λ x, by { subst f, refl }

theorem lift_range (H : c ≤ ker f) : (c.lift f H).mrange = f.mrange :=

submonoid.ext $ λ x, ⟨by rintros ⟨⟨y⟩, hy⟩; exact ⟨y, hy⟩, λ ⟨y, hy⟩, ⟨↑y, hy⟩⟩

lemma lift_surjective_of_surjective (h : c ≤ ker f) (hf : surjective f) :

surjective (c.lift f h) :=

λ y, exists.elim (hf y) $ λ w hw, ⟨w, (lift_mk' h w).symm ▸ hw⟩

variables (c f)

lemma ker_eq_lift_of_injective (H : c ≤ ker f) (h : injective (c.lift f H)) :

ker f = c :=

to_setoid_inj $ ker_eq_lift_of_injective f H h

variables {c}

def ker_lift : (ker f).quotient →* P :=

(ker f).lift f $ λ _ _, id

variables {f}

lemma ker_lift_mk (x : M) : ker_lift f x = f x := rfl

lemma ker_lift_range_eq : (ker_lift f).mrange = f.mrange :=

lift_range $ λ _ _, id

lemma ker_lift_injective (f : M →* P) : injective (ker_lift f) :=

λ x y, quotient.induction_on₂' x y $ λ _ _, (ker f).eq.2

def map (c d : con M) (h : c ≤ d) : c.quotient →* d.quotient :=

c.lift d.mk' $ λ x y hc, show (ker d.mk') x y, from

(mk'_ker d).symm ▸ h hc

lemma map_apply {c d : con M} (h : c ≤ d) (x) :

c.map d h x = c.lift d.mk' (λ x y hc, d.eq.2 $ h hc) x := rfl

variables (c)

noncomputable def quotient_ker_equiv_range (f : M →* P) : (ker f).quotient ≃* f.mrange :=

{ map_mul' := monoid_hom.map_mul _,

..equiv.of_bijective

((@mul_equiv.to_monoid_hom (ker_lift f).mrange _ _ _

$ mul_equiv.submonoid_congr ker_lift_range_eq).comp (ker_lift f).mrange_restrict) $

(equiv.bijective _).comp

⟨λ x y h, ker_lift_injective f $ by rcases x; rcases y; injections,

λ ⟨w, z, hz⟩, ⟨z, by rcases hz; rcases _x; refl⟩⟩ }

def quotient_ker_equiv_of_right_inverse (f : M →* P) (g : P → M)

(hf : function.right_inverse g f) :

(ker f).quotient ≃* P :=

{ to_fun := ker_lift f,

inv_fun := coe ∘ g,

left_inv := λ x, ker_lift_injective _ (by rw [function.comp_app, ker_lift_mk, hf]),

right_inv := hf,

.. ker_lift f }

noncomputable def quotient_ker_equiv_of_surjective (f : M →* P) (hf : surjective f) :

(ker f).quotient ≃* P :=

quotient_ker_equiv_of_right_inverse _ _ hf.has_right_inverse.some_spec

noncomputable def comap_quotient_equiv (f : N →* M) :

(comap f f.map_mul c).quotient ≃* (c.mk'.comp f).mrange :=

(con.congr comap_eq).trans $ quotient_ker_equiv_range $ c.mk'.comp f

def quotient_quotient_equiv_quotient (c d : con M) (h : c ≤ d) :

(ker (c.map d h)).quotient ≃* d.quotient :=

{ map_mul' := λ x y, con.induction_on₂ x y $ λ w z, con.induction_on₂ w z $ λ a b,

show _ = d.mk' a * d.mk' b, by rw ←d.mk'.map_mul; refl,

..quotient_quotient_equiv_quotient c.to_setoid d.to_setoid h }

end mul_one_class

section monoids

protected lemma pow {M : Type*} [monoid M] (c : con M) :

∀ (n : ℕ) {w x}, c w x → c (w ^ n) (x ^ n)

| 0 w x h := by simpa using c.refl _

| (nat.succ n) w x h := by simpa [pow_succ] using c.mul h (pow n h)

instance {M : Type*} [mul_one_class M] (c : con M) : has_one c.quotient :=

{ one := ((1 : M) : c.quotient) }

lemma smul {α M : Type*} [mul_one_class M] [has_smul α M] [is_scalar_tower α M M] (c : con M)

(a : α) {w x : M} (h : c w x) : c (a • w) (a • x) :=

by simpa only [smul_one_mul] using c.mul (c.refl' (a • 1 : M)) h

instance _root_.add_con.quotient.has_nsmul

{M : Type*} [add_monoid M] (c : add_con M) : has_smul ℕ c.quotient :=

{ smul := λ n, quotient.map' ((•) n) $ λ x y, c.nsmul n }

instance {M : Type*} [monoid M] (c : con M) : has_pow c.quotient ℕ :=

{ pow := λ x n, quotient.map' (λ x, x ^ n) (λ x y, c.pow n) x }

instance semigroup {M : Type*} [semigroup M] (c : con M) : semigroup c.quotient :=

function.surjective.semigroup _ quotient.surjective_quotient_mk' (λ _ _, rfl)

instance comm_semigroup {M : Type*} [comm_semigroup M] (c : con M) : comm_semigroup c.quotient :=

function.surjective.comm_semigroup _ quotient.surjective_quotient_mk' (λ _ _, rfl)

instance monoid {M : Type*} [monoid M] (c : con M) : monoid c.quotient :=

function.surjective.monoid _ quotient.surjective_quotient_mk' rfl (λ _ _, rfl) (λ _ _, rfl)

instance comm_monoid {M : Type*} [comm_monoid M] (c : con M) :

comm_monoid c.quotient :=

function.surjective.comm_monoid _ quotient.surjective_quotient_mk' rfl (λ _ _, rfl) (λ _ _, rfl)

end monoids

section groups

variables {M} [group M] [group N] [group P] (c : con M)

protected lemma inv : ∀ {w x}, c w x → c w⁻¹ x⁻¹ :=

λ x y h, by simpa using c.symm (c.mul (c.mul (c.refl x⁻¹) h) (c.refl y⁻¹))

protected lemma div : ∀ {w x y z}, c w x → c y z → c (w / y) (x / z) :=

λ w x y z h1 h2, by simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2)

protected lemma zpow : ∀ (n : ℤ) {w x}, c w x → c (w ^ n) (x ^ n)

| (int.of_nat n) w x h := by simpa only [zpow_of_nat] using c.pow _ h

| -[1+ n] w x h := by simpa only [zpow_neg_succ_of_nat] using c.inv (c.pow _ h)

instance has_inv : has_inv c.quotient :=

⟨quotient.map' has_inv.inv $ λ a b, c.inv⟩

instance has_div : has_div c.quotient :=

⟨quotient.map₂' (/) $ λ _ _ h₁ _ _ h₂, c.div h₁ h₂⟩

instance _root_.add_con.quotient.has_zsmul

{M : Type*} [add_group M] (c : add_con M) : has_smul ℤ c.quotient :=

⟨λ z, quotient.map' ((•) z) $ λ x y, c.zsmul z⟩

instance has_zpow : has_pow c.quotient ℤ :=

⟨λ x z, quotient.map' (λ x, x ^ z) (λ x y h, c.zpow z h) x⟩

instance group : group c.quotient :=

function.surjective.group _ quotient.surjective_quotient_mk' rfl

(λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

end groups

section units

variables {α : Type*} [monoid M] {c : con M}

@[to_additive] def lift_on_units (u : units c.quotient)

(f : Π (x y : M), c (x * y) 1 → c (y * x) 1 → α)

(Hf : ∀ x y hxy hyx x' y' hxy' hyx', c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx') :

α :=

refine @con.hrec_on₂ M M _ _ c c (λ x y, x * y = 1 → y * x = 1 → α)

(u : c.quotient) (↑u⁻¹ : c.quotient)

(λ (x y : M) (hxy : (x * y : c.quotient) = 1) (hyx : (y * x : c.quotient) = 1),

f x y (c.eq.1 hxy) (c.eq.1 hyx)) (λ x y x' y' hx hy, _) u.3 u.4,