doc-next-gen

Mathlib.GroupTheory.Congruence.Defs

Module docstring

{"# Congruence relations

This file defines congruence relations: equivalence relations that preserve a binary operation, which in this case is multiplication or addition. The principal definition is a structure extending a Setoid (an equivalence relation), and the inductive definition of the smallest congruence relation containing a binary relation is also given (see ConGen).

The file also proves basic properties of the quotient of a type by a congruence relation, and the complete lattice of congruence relations on a type. We then establish an order-preserving bijection between the set of congruence relations containing a congruence relation c and the set of congruence relations on the quotient by c.

The second half of the file concerns congruence relations on monoids, in which case the quotient by the congruence relation is also a monoid.

Implementation notes

The inductive definition of a congruence relation could be a nested inductive type, defined using the equivalence closure of a binary relation EqvGen, but the recursor generated does not work. A nested inductive definition could conceivably shorten proofs, because they would allow invocation of the corresponding lemmas about EqvGen.

The lemmas refl, symm and trans are not tagged with @[refl], @[symm], and @[trans] respectively as these tags do not work on a structure coerced to a binary relation.

There is a coercion from elements of a type to the element's equivalence class under a congruence relation.

A congruence relation on a monoid M can be thought of as a submonoid of M × M for which membership is an equivalence relation, but whilst this fact is established in the file, it is not used, since this perspective adds more layers of definitional unfolding.

Tags

congruence, congruence relation, quotient, quotient by congruence relation, monoid, quotient monoid, isomorphism theorems "}

AddCon structure
[Add M] extends Setoid M
Full source 
/-- A congruence relation on a type with an addition is an equivalence relation which
    preserves addition. -/
structure AddCon [Add M] extends Setoid M where
  /-- Additive congruence relations are closed under addition -/
  add' : ∀ {w x y z}, r w x → r y z → r (w + y) (x + z)
Additive congruence relation
Informal description
A congruence relation on a type $M$ with an addition operation is an equivalence relation $\sim$ on $M$ that preserves addition, meaning that for any $x_1, x_2, y_1, y_2 \in M$, if $x_1 \sim y_1$ and $x_2 \sim y_2$, then $x_1 + x_2 \sim y_1 + y_2$.
Con structure
[Mul M] extends Setoid M
Full source 
/-- A congruence relation on a type with a multiplication is an equivalence relation which
    preserves multiplication. -/
@[to_additive AddCon]
structure Con [Mul M] extends Setoid M where
  /-- Congruence relations are closed under multiplication -/
  mul' : ∀ {w x y z}, r w x → r y z → r (w * y) (x * z)
Congruence relation on a multiplicative structure
Informal description
A congruence relation on a type $M$ with a multiplication operation is an equivalence relation $\sim$ on $M$ that preserves multiplication, i.e., for all $x_1, x_2, y_1, y_2 \in M$, if $x_1 \sim y_1$ and $x_2 \sim y_2$, then $x_1 \cdot x_2 \sim y_1 \cdot y_2$.
AddConGen.Rel inductive
[Add M] (r : M → M → Prop) : M → M → Prop
Full source 
/-- The inductively defined smallest additive congruence relation containing a given binary
    relation. -/
inductive AddConGen.Rel [Add M] (r : M → M → Prop) : M → M → Prop
  | of : ∀ x y, r x y → AddConGen.Rel r x y
  | refl : ∀ x, AddConGen.Rel r x x
  | symm : ∀ {x y}, AddConGen.Rel r x y → AddConGen.Rel r y x
  | trans : ∀ {x y z}, AddConGen.Rel r x y → AddConGen.Rel r y z → AddConGen.Rel r x z
  | add : ∀ {w x y z}, AddConGen.Rel r w x → AddConGen.Rel r y z → AddConGen.Rel r (w + y) (x + z)
Generating relation for additive congruence
Informal description
The relation `AddConGen.Rel r` is the smallest additive congruence relation on a type `M` with an addition operation that contains the binary relation `r`. It is defined inductively as the smallest relation that includes `r` and is closed under reflexivity, symmetry, transitivity, and compatibility with addition (i.e., if `x₁ ~ y₁` and `x₂ ~ y₂`, then `x₁ + x₂ ~ y₁ + y₂`).
ConGen.Rel inductive
[Mul M] (r : M → M → Prop) : M → M → Prop
Full source 
/-- The inductively defined smallest multiplicative congruence relation containing a given binary
    relation. -/
@[to_additive AddConGen.Rel]
inductive ConGen.Rel [Mul M] (r : M → M → Prop) : M → M → Prop
  | of : ∀ x y, r x y → ConGen.Rel r x y
  | refl : ∀ x, ConGen.Rel r x x
  | symm : ∀ {x y}, ConGen.Rel r x y → ConGen.Rel r y x
  | trans : ∀ {x y z}, ConGen.Rel r x y → ConGen.Rel r y z → ConGen.Rel r x z
  | mul : ∀ {w x y z}, ConGen.Rel r w x → ConGen.Rel r y z → ConGen.Rel r (w * y) (x * z)
Generating relation of the smallest multiplicative congruence
Informal description
The inductive relation `ConGen.Rel r` is the smallest multiplicative congruence relation on a type `M` with multiplication that contains the binary relation `r`. It is defined inductively such that it includes `r` and is closed under reflexivity, symmetry, transitivity, and multiplication. More precisely, for a binary relation `r : M → M → Prop` on a multiplicative structure `M`, the relation `ConGen.Rel r` is the smallest relation satisfying: 1. If `r x y` holds, then `ConGen.Rel r x y` holds. 2. `ConGen.Rel r x x` for any `x : M` (reflexivity). 3. If `ConGen.Rel r x y`, then `ConGen.Rel r y x` (symmetry). 4. If `ConGen.Rel r x y` and `ConGen.Rel r y z`, then `ConGen.Rel r x z` (transitivity). 5. If `ConGen.Rel r x₁ y₁` and `ConGen.Rel r x₂ y₂`, then `ConGen.Rel r (x₁ * x₂) (y₁ * y₂)` (multiplicative closure).
conGen definition
[Mul M] (r : M → M → Prop) : Con M
Full source 
/-- The inductively defined smallest multiplicative congruence relation containing a given binary
    relation. -/
@[to_additive addConGen "The inductively defined smallest additive congruence relation containing
a given binary relation."]
def conGen [Mul M] (r : M → M → Prop) : Con M :=
  ⟨⟨ConGen.Rel r, ⟨ConGen.Rel.refl, ConGen.Rel.symm, ConGen.Rel.trans⟩⟩, ConGen.Rel.mul⟩
Smallest multiplicative congruence relation containing a given relation
Informal description
Given a binary relation `r` on a multiplicative structure `M`, the function `conGen r` constructs the smallest congruence relation on `M` that contains `r`. This congruence relation is defined as the equivalence closure of `r` that is also closed under multiplication, meaning it satisfies reflexivity, symmetry, transitivity, and compatibility with multiplication. More precisely, `conGen r` is the smallest relation `~` such that: 1. If `r x y` holds, then `x ~ y`. 2. `x ~ x` for all `x ∈ M` (reflexivity). 3. If `x ~ y`, then `y ~ x` (symmetry). 4. If `x ~ y` and `y ~ z`, then `x ~ z` (transitivity). 5. If `x₁ ~ y₁` and `x₂ ~ y₂`, then `x₁ * x₂ ~ y₁ * y₂` (multiplicative compatibility).
Con.instInhabited instance
: Inhabited (Con M)
Full source 
@[to_additive]
instance : Inhabited (Con M) :=
  ⟨conGen EmptyRelation⟩
Nonempty Collection of Congruence Relations on a Multiplicative Structure
Informal description
For any type $M$ with a multiplication operation, the collection of congruence relations on $M$ is nonempty.
Con.instFunLikeForallProp instance
: FunLike (Con M) M (M → Prop)
Full source 
/-- A coercion from a congruence relation to its underlying binary relation. -/
@[to_additive "A coercion from an additive congruence relation to its underlying binary relation."]
instance : FunLike (Con M) M (M → Prop) where
  coe c := c.r
  coe_injective' x y h := by
    rcases x with ⟨⟨x, _⟩, _⟩
    rcases y with ⟨⟨y, _⟩, _⟩
    have : x = y := h
    subst x; rfl
Congruence Relations as Predicate Functions
Informal description
For any type $M$ with a multiplication operation, a congruence relation $c$ on $M$ can be viewed as a function from $M$ to the set of predicates on $M$. This means that for each $x \in M$, the relation $c(x)$ is a predicate that holds for all $y \in M$ such that $x \sim y$ under the congruence relation $c$.
Con.rel_eq_coe theorem
(c : Con M) : c.r = c
Full source 
@[to_additive (attr := simp)]
theorem rel_eq_coe (c : Con M) : c.r = c :=
  rfl
Congruence Relation Equals Its Underlying Relation
Informal description
For any congruence relation $c$ on a multiplicative structure $M$, the underlying relation $c.r$ is equal to $c$ itself.
Con.refl theorem
(x) : c x x
Full source 
/-- Congruence relations are reflexive. -/
@[to_additive "Additive congruence relations are reflexive."]
protected theorem refl (x) : c x x :=
  c.toSetoid.refl' x
Reflexivity of Congruence Relations
Informal description
For any congruence relation $c$ on a multiplicative structure $M$ and any element $x \in M$, the relation $x \sim x$ holds under $c$.
Con.symm theorem
{x y} : c x y → c y x
Full source 
/-- Congruence relations are symmetric. -/
@[to_additive "Additive congruence relations are symmetric."]
protected theorem symm {x y} : c x y → c y x := c.toSetoid.symm'
Symmetry of Congruence Relations
Informal description
For any congruence relation $c$ on a multiplicative structure $M$ and any elements $x, y \in M$, if $x \sim y$ under $c$, then $y \sim x$ under $c$.
Con.trans theorem
{x y z} : c x y → c y z → c x z
Full source 
/-- Congruence relations are transitive. -/
@[to_additive "Additive congruence relations are transitive."]
protected theorem trans {x y z} : c x y → c y z → c x z := c.toSetoid.trans'
Transitivity of Congruence Relations
Informal description
For any congruence relation $c$ on a multiplicative structure $M$ and any elements $x, y, z \in M$, if $x \sim y$ and $y \sim z$ under $c$, then $x \sim z$ under $c$.
Con.mul theorem
{w x y z} : c w x → c y z → c (w * y) (x * z)
Full source 
/-- Multiplicative congruence relations preserve multiplication. -/
@[to_additive "Additive congruence relations preserve addition."]
protected theorem mul {w x y z} : c w x → c y z → c (w * y) (x * z) := c.mul'
Multiplication Preservation under Congruence Relations
Informal description
For any congruence relation $c$ on a multiplicative structure $M$ and any elements $w, x, y, z \in M$, if $w \sim x$ and $y \sim z$ under $c$, then $w \cdot y \sim x \cdot z$ under $c$.
Con.rel_mk theorem
{s : Setoid M} {h a b} : Con.mk s h a b ↔ r a b
Full source 
@[to_additive (attr := simp)]
theorem rel_mk {s : Setoid M} {h a b} : Con.mkCon.mk s h a b ↔ r a b :=
  Iff.rfl
Characterization of Congruence Relation Construction via Setoid
Informal description
For a setoid `s` on a multiplicative structure `M` and a proof `h` that `s` preserves multiplication, the congruence relation `Con.mk s h` relates elements `a` and `b` if and only if the underlying relation `r` of the setoid relates `a` and `b`. In other words, for `a, b ∈ M`, we have `Con.mk s h a b ↔ r a b`.
Con.instMembershipProd instance
: Membership (M × M) (Con M)
Full source 
/-- Given a type `M` with a multiplication, a congruence relation `c` on `M`, and elements of `M`
    `x, y`, `(x, y) ∈ M × M` iff `x` is related to `y` by `c`. -/
@[to_additive instMembershipProd
  "Given a type `M` with an addition, `x, y ∈ M`, and an additive congruence relation
`c` on `M`, `(x, y) ∈ M × M` iff `x` is related to `y` by `c`."]
instance instMembershipProd : Membership (M × M) (Con M) :=
  ⟨fun c x => c x.1 x.2⟩
Membership in Congruence Relations for Multiplicative Structures
Informal description
For a type $M$ with a multiplication operation and a congruence relation $c$ on $M$, we say $(x, y) \in c$ if $x$ is related to $y$ by $c$.
Con.ext' theorem
{c d : Con M} (H : ⇑c = ⇑d) : c = d
Full source 
/-- The map sending a congruence relation to its underlying binary relation is injective. -/
@[to_additive "The map sending an additive congruence relation to its underlying binary relation
is injective."]
theorem ext' {c d : Con M} (H : ⇑c = ⇑d) : c = d := DFunLike.coe_injective H
Injectivity of Congruence Relation Underlying Map
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, if the underlying binary relations of $c$ and $d$ are equal (i.e., $c(x, y) = d(x, y)$ for all $x, y \in M$), then $c = d$.
Con.ext theorem
{c d : Con M} (H : ∀ x y, c x y ↔ d x y) : c = d
Full source 
/-- Extensionality rule for congruence relations. -/
@[to_additive (attr := ext) "Extensionality rule for additive congruence relations."]
theorem ext {c d : Con M} (H : ∀ x y, c x y ↔ d x y) : c = d :=
  ext' <| by ext; apply H
Extensionality of Congruence Relations via Underlying Relations
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, if for all elements $x, y \in M$ the relation $c(x, y)$ holds if and only if $d(x, y)$ holds, then $c = d$.
Con.toSetoid_inj theorem
{c d : Con M} (H : c.toSetoid = d.toSetoid) : c = d
Full source 
/-- The map sending a congruence relation to its underlying equivalence relation is injective. -/
@[to_additive "The map sending an additive congruence relation to its underlying equivalence
relation is injective."]
theorem toSetoid_inj {c d : Con M} (H : c.toSetoid = d.toSetoid) : c = d :=
  ext <| Setoid.ext_iff.1 H
Injectivity of Congruence Relation to Underlying Equivalence Relation
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, if their underlying equivalence relations (as setoids) are equal, then $c = d$.
Con.coe_inj theorem
{c d : Con M} : ⇑c = ⇑d ↔ c = d
Full source 
/-- Two congruence relations are equal iff their underlying binary relations are equal. -/
@[to_additive "Two additive congruence relations are equal iff their underlying binary relations
are equal."]
theorem coe_inj {c d : Con M} : ⇑c = ⇑d ↔ c = d := DFunLike.coe_injective.eq_iff
Equality of Congruence Relations via Underlying Relations
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, the underlying binary relations of $c$ and $d$ are equal if and only if $c = d$.
Con.Quotient definition
Full source 
/-- Defining the quotient by a congruence relation of a type with a multiplication. -/
@[to_additive "Defining the quotient by an additive congruence relation of a type with
an addition."]
protected def Quotient :=
  Quotient c.toSetoid
Quotient by a congruence relation
Informal description
The quotient of a type $M$ by a congruence relation $c$ on $M$, denoted $M/c$, is the set of equivalence classes of elements of $M$ under the equivalence relation defined by $c$.
Con.toQuotient definition
: M → c.Quotient
Full source 
/-- The morphism into the quotient by a congruence relation -/
@[to_additive (attr := coe) "The morphism into the quotient by an additive congruence relation"]
def toQuotient : M → c.Quotient :=
  Quotient.mk''
Canonical projection to the quotient by a congruence relation
Informal description
The function maps an element \( x \) of a type \( M \) to its equivalence class \([x]\) in the quotient \( M/c \), where \( c \) is a congruence relation on \( M \).
Con.instCoeTCQuotient instance
: CoeTC M c.Quotient
Full source 
/-- Coercion from a type with a multiplication to its quotient by a congruence relation.

See Note [use has_coe_t]. -/
@[to_additive "Coercion from a type with an addition to its quotient by an additive congruence
relation"]
instance (priority := 10) : CoeTC M c.Quotient :=
  ⟨toQuotient⟩
Canonical Projection to the Quotient by a Congruence Relation
Informal description
For any type $M$ with a multiplication operation and a congruence relation $c$ on $M$, there is a canonical function from $M$ to the quotient $M/c$ that maps each element $x \in M$ to its equivalence class $[x] \in M/c$.
Con.instDecidableEqQuotientOfDecidableCoeForallProp instance
[∀ a b, Decidable (c a b)] : DecidableEq c.Quotient
Full source 
/-- The quotient by a decidable congruence relation has decidable equality. -/
@[to_additive "The quotient by a decidable additive congruence relation has decidable equality."]
instance (priority := 500) [∀ a b, Decidable (c a b)] : DecidableEq c.Quotient :=
  inferInstanceAs (DecidableEq (Quotient c.toSetoid))
Decidable Equality for Quotient by Decidable Congruence Relation
Informal description
For any type $M$ with a multiplication operation and a congruence relation $c$ on $M$, if the relation $c$ is decidable (i.e., for any $a, b \in M$, it is decidable whether $a \sim b$ under $c$), then the quotient $M/c$ has decidable equality.
Con.quot_mk_eq_coe theorem
{M : Type*} [Mul M] (c : Con M) (x : M) : Quot.mk c x = (x : c.Quotient)
Full source 
@[to_additive (attr := simp)]
theorem quot_mk_eq_coe {M : Type*} [Mul M] (c : Con M) (x : M) : Quot.mk c x = (x : c.Quotient) :=
  rfl
Equivalence Class Construction via Quotient Projection
Informal description
For any type $M$ with a multiplication operation and any congruence relation $c$ on $M$, the equivalence class of an element $x \in M$ under $c$ (constructed via `Quot.mk`) is equal to the image of $x$ under the canonical projection to the quotient $M/c$.
Con.liftOn definition
{β} {c : Con M} (q : c.Quotient) (f : M → β) (h : ∀ a b, c a b → f a = f b) : β
Full source 
/-- The function on the quotient by a congruence relation `c` induced by a function that is
    constant on `c`'s equivalence classes. -/
@[to_additive "The function on the quotient by a congruence relation `c`
induced by a function that is constant on `c`'s equivalence classes."]
protected def liftOn {β} {c : Con M} (q : c.Quotient) (f : M → β) (h : ∀ a b, c a b → f a = f b) :
    β :=
  Quotient.liftOn' q f h
Lifting a function to the quotient by a congruence relation
Informal description
Given a congruence relation $c$ on a multiplicative structure $M$, a function $f \colon M \to \beta$ that is constant on $c$-equivalence classes, and an element $q$ of the quotient $M/c$, the function `Con.liftOn` lifts $f$ to a function on the quotient by applying $f$ to any representative of $q$'s equivalence class. More precisely, for any $q \in M/c$ and any function $f \colon M \to \beta$ satisfying $f(a) = f(b)$ whenever $a \sim b$ under $c$, the value $\text{Con.liftOn}\ q\ f\ h$ is $f(x)$ for any $x$ in the equivalence class represented by $q$.
Con.liftOn₂ definition
{β} {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₂) : β
Full source 
/-- The binary function on the quotient by a congruence relation `c` induced by a binary function
    that is constant on `c`'s equivalence classes. -/
@[to_additive "The binary function on the quotient by a congruence relation `c`
induced by a binary function that is constant on `c`'s equivalence classes."]
protected def liftOn₂ {β} {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.liftOn₂' q r f h
Lifting a binary function to the quotient by a congruence relation
Informal description
Given a congruence relation $c$ on a multiplicative structure $M$, two elements $q, r$ of the quotient $M/c$, and a binary function $f \colon M \times M \to \beta$ that respects $c$ (i.e., $f(a_1, a_2) = f(b_1, b_2)$ whenever $a_1 \sim b_1$ and $a_2 \sim b_2$ under $c$), the function `Con.liftOn₂` lifts $f$ to a binary function on the quotient by applying $f$ to any representatives of $q$ and $r$'s equivalence classes.
Con.hrecOn₂ definition
{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' → HEq (f x y) (f x' y')) : φ a b
Full source 
/-- A version of `Quotient.hrecOn₂'` for quotients by `Con`. -/
@[to_additive "A version of `Quotient.hrecOn₂'` for quotients by `AddCon`."]
protected def hrecOn₂ {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' → HEq (f x y) (f x' y')) : φ a b :=
  Quotient.hrecOn₂' a b f h
Heterogeneous recursion on quotients by congruence relations
Informal description
Given congruence relations $c_M$ on $M$ and $c_N$ on $N$, and a dependent type $\varphi$ indexed by pairs of equivalence classes in $M/c_M$ and $N/c_N$, the function `Con.hrecOn₂` allows defining a function on the quotients by recursion. For any equivalence classes $a \in M/c_M$ and $b \in N/c_N$, and any function $f \colon M \times N \to \varphi(x,y)$ that respects the congruence relations (i.e., $f(x,y)$ and $f(x',y')$ are heterogeneously equal whenever $x \sim_{c_M} x'$ and $y \sim_{c_N} y'$), the value $\text{Con.hrecOn₂}\ a\ b\ f\ h$ is well-defined and yields an element of $\varphi(a,b)$.
Con.hrec_on₂_coe theorem
{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' → HEq (f x y) (f x' y')) : Con.hrecOn₂ (↑a) (↑b) f h = f a b
Full source 
@[to_additive (attr := simp)]
theorem 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' → HEq (f x y) (f x' y')) :
    Con.hrecOn₂ (↑a) (↑b) f h = f a b :=
  rfl
Heterogeneous Recursion on Quotients by Congruence Relations Preserves Function Application
Informal description
Let $M$ and $N$ be types with congruence relations $c_M$ and $c_N$ respectively, and let $\varphi$ be a dependent type indexed by pairs of equivalence classes in $M/c_M$ and $N/c_N$. For any elements $a \in M$ and $b \in N$, and any function $f \colon M \times N \to \varphi(x,y)$ that respects the congruence relations (i.e., $f(x,y)$ and $f(x',y')$ are heterogeneously equal whenever $x \sim_{c_M} x'$ and $y \sim_{c_N} y'$), the value of the heterogeneous recursion function applied to the equivalence classes $[a]$ and $[b]$ is equal to $f(a,b)$. In other words, $\text{Con.hrecOn₂}([a], [b], f, h) = f(a,b)$.
Con.induction_on theorem
{C : c.Quotient → Prop} (q : c.Quotient) (H : ∀ x : M, C x) : C q
Full source 
/-- The inductive principle used to prove propositions about the elements of a quotient by a
    congruence relation. -/
@[to_additive (attr := elab_as_elim) "The inductive principle used to prove propositions about
the elements of a quotient by an additive congruence relation."]
protected theorem induction_on {C : c.Quotient → Prop} (q : c.Quotient) (H : ∀ x : M, C x) : C q :=
  Quotient.inductionOn' q H
Induction Principle for Quotient by Congruence Relation
Informal description
Let $M$ be a type with a congruence relation $c$, and let $C$ be a predicate on the quotient $M/c$. For any equivalence class $q \in M/c$, if $C([x])$ holds for every $x \in M$, then $C(q)$ holds.
Con.induction_on₂ theorem
{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
Full source 
/-- A version of `Con.induction_on` for predicates which take two arguments. -/
@[to_additive (attr := elab_as_elim) "A version of `AddCon.induction_on` for predicates which take
two arguments."]
protected theorem 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.inductionOn₂' p q H
Double Induction Principle for Quotients by Congruence Relations
Informal description
Let $M$ and $N$ be types with congruence relations $c$ and $d$ respectively, and let $C$ be a predicate on the product of their quotients $M/c \times N/d$. For any equivalence classes $p \in M/c$ and $q \in N/d$, if $C([x], [y])$ holds for all $x \in M$ and $y \in N$, then $C(p, q)$ holds.
Con.eq theorem
{a b : M} : (a : c.Quotient) = (b : c.Quotient) ↔ c a b
Full source 
/-- Two elements are related by a congruence relation `c` iff they are represented by the same
    element of the quotient by `c`. -/
@[to_additive (attr := simp) "Two elements are related by an additive congruence relation `c` iff
they are represented by the same element of the quotient by `c`."]
protected theorem eq {a b : M} : (a : c.Quotient) = (b : c.Quotient) ↔ c a b :=
  Quotient.eq''
Equality in Quotient by Congruence Relation Characterizes Congruence
Informal description
For any elements $a, b$ in a type $M$ with a congruence relation $c$, the equivalence classes of $a$ and $b$ in the quotient $M/c$ are equal if and only if $a$ is related to $b$ under the congruence relation $c$. That is, $[a] = [b] \leftrightarrow c(a, b)$.
Con.hasMul instance
: Mul c.Quotient
Full source 
/-- The multiplication induced on the quotient by a congruence relation on a type with a
    multiplication. -/
@[to_additive "The addition induced on the quotient by an additive congruence relation on a type
with an addition."]
instance hasMul : Mul c.Quotient :=
  ⟨Quotient.map₂ (· * ·) fun _ _ h1 _ _ h2 => c.mul h1 h2⟩
Multiplication on the Quotient by a Congruence Relation
Informal description
The quotient $M/c$ of a multiplicative structure $M$ by a congruence relation $c$ inherits a multiplication operation defined by $[x] \cdot [y] = [x \cdot y]$, where $[x]$ denotes the equivalence class of $x \in M$ under $c$.
Con.coe_mul theorem
(x y : M) : (↑(x * y) : c.Quotient) = ↑x * ↑y
Full source 
/-- The coercion to the quotient of a congruence relation commutes with multiplication (by
    definition). -/
@[to_additive (attr := simp) "The coercion to the quotient of an additive congruence relation
commutes with addition (by definition)."]
theorem coe_mul (x y : M) : (↑(x * y) : c.Quotient) = ↑x * ↑y :=
  rfl
Compatibility of Quotient Projection with Multiplication: $[x \cdot y] = [x] \cdot [y]$
Informal description
For any elements $x$ and $y$ in a multiplicative structure $M$ with a congruence relation $c$, the equivalence class of the product $x \cdot y$ in the quotient $M/c$ equals the product of the equivalence classes of $x$ and $y$. That is, $[x \cdot y] = [x] \cdot [y]$.
Con.liftOn_coe theorem
{β} (c : Con M) (f : M → β) (h : ∀ a b, c a b → f a = f b) (x : M) : Con.liftOn (x : c.Quotient) f h = f x
Full source 
/-- Definition of the function on the quotient by a congruence relation `c` induced by a function
    that is constant on `c`'s equivalence classes. -/
@[to_additive (attr := simp) "Definition of the function on the quotient by an additive congruence
relation `c` induced by a function that is constant on `c`'s equivalence classes."]
protected theorem liftOn_coe {β} (c : Con M) (f : M → β) (h : ∀ a b, c a b → f a = f b) (x : M) :
    Con.liftOn (x : c.Quotient) f h = f x :=
  rfl
Lifted Function Evaluation on Quotient Representatives
Informal description
Let $M$ be a type with a multiplication operation, $c$ a congruence relation on $M$, and $f \colon M \to \beta$ a function that is constant on $c$-equivalence classes (i.e., $f(a) = f(b)$ whenever $a \sim b$ under $c$). Then for any $x \in M$, the value of the lifted function $\text{Con.liftOn}$ applied to the equivalence class $[x] \in M/c$ equals $f(x)$, i.e., \[ \text{Con.liftOn}([x], f, h) = f(x). \]
Con.instLE instance
: LE (Con M)
Full source 
/-- For congruence relations `c, d` on a type `M` with a multiplication, `c ≤ d` iff `∀ x y ∈ M`,
    `x` is related to `y` by `d` if `x` is related to `y` by `c`. -/
@[to_additive "For additive congruence relations `c, d` on a type `M` with an addition, `c ≤ d` iff
`∀ x y ∈ M`, `x` is related to `y` by `d` if `x` is related to `y` by `c`."]
instance : LE (Con M) where
  le c d := ∀ ⦃x y⦄, c x y → d x y
Partial Order on Congruence Relations
Informal description
For any type $M$ with a multiplication operation, the set of congruence relations on $M$ is equipped with a partial order $\leq$ where for two congruence relations $c$ and $d$, $c \leq d$ if and only if for all $x, y \in M$, whenever $x$ is related to $y$ by $c$, then $x$ is also related to $y$ by $d$.
Con.le_def theorem
{c d : Con M} : c ≤ d ↔ ∀ {x y}, c x y → d x y
Full source 
/-- Definition of `≤` for congruence relations. -/
@[to_additive "Definition of `≤` for additive congruence relations."]
theorem le_def {c d : Con M} : c ≤ d ↔ ∀ {x y}, c x y → d x y :=
  Iff.rfl
Definition of Partial Order on Congruence Relations: $c \leq d$ iff $c \subseteq d$
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, the relation $c \leq d$ holds if and only if for all $x, y \in M$, whenever $x$ is related to $y$ under $c$, then $x$ is also related to $y$ under $d$.
Con.instInfSet instance
: InfSet (Con M)
Full source 
/-- The infimum of a set of congruence relations on a given type with a multiplication. -/
@[to_additive "The infimum of a set of additive congruence relations on a given type with
an addition."]
instance : InfSet (Con M) where
  sInf S :=
    { r := fun x y => ∀ c : Con M, c ∈ S → c x y
      iseqv := ⟨fun x c _ => c.refl x, fun h c hc => c.symm <| h c hc,
        fun h1 h2 c hc => c.trans (h1 c hc) <| h2 c hc⟩
      mul' := fun h1 h2 c hc => c.mul (h1 c hc) <| h2 c hc }
Infimum of Congruence Relations on a Multiplicative Structure
Informal description
For any type $M$ with a multiplication operation, the set of congruence relations on $M$ has an infimum operation. Given a family of congruence relations $\{c_i\}_{i \in I}$ on $M$, their infimum $\bigwedge_{i \in I} c_i$ is the greatest congruence relation that is contained in every $c_i$.
Con.sInf_toSetoid theorem
(S : Set (Con M)) : (sInf S).toSetoid = sInf (toSetoid '' S)
Full source 
/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
    under the map to the underlying equivalence relation. -/
@[to_additive "The infimum of a set of additive congruence relations is the same as the infimum of
the set's image under the map to the underlying equivalence relation."]
theorem sInf_toSetoid (S : Set (Con M)) : (sInf S).toSetoid = sInf (toSetoidtoSetoid '' S) :=
  Setoid.ext fun x y =>
    ⟨fun h r ⟨c, hS, hr⟩ => by rw [← hr]; exact h c hS, fun h c hS => h c.toSetoid ⟨c, hS, rfl⟩⟩
Infimum of Congruence Relations Preserves Underlying Equivalence Relation
Informal description
For any set $S$ of congruence relations on a multiplicative structure $M$, the underlying equivalence relation of the infimum of $S$ is equal to the infimum of the set of equivalence relations obtained by applying the `toSetoid` function to each congruence relation in $S$. In other words, $\left(\bigwedge S\right)_{\text{equiv}} = \bigwedge \{c_{\text{equiv}} \mid c \in S\}$.
Con.coe_sInf theorem
(S : Set (Con M)) : ⇑(sInf S) = sInf ((⇑) '' S)
Full source 
/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
    under the map to the underlying binary relation. -/
@[to_additive (attr := simp, norm_cast)
  "The infimum of a set of additive congruence relations is the same as the infimum
  of the set's image under the map to the underlying binary relation."]
theorem coe_sInf (S : Set (Con M)) :
    ⇑(sInf S) = sInf ((⇑) '' S) := by
  ext
  simp only [sInf_image, iInf_apply, iInf_Prop_eq]
  rfl
Infimum of Congruence Relations as Infimum of Binary Relations
Informal description
For any set $S$ of congruence relations on a multiplicative structure $M$, the underlying binary relation of the infimum of $S$ is equal to the infimum of the set of binary relations obtained by applying the coercion function to each congruence relation in $S$. In other words, $\bigwedge S = \bigwedge \{c \mid c \in S\}$ where the infima are taken in the lattice of binary relations on $M$.
Con.coe_iInf theorem
{ι : Sort*} (f : ι → Con M) : ⇑(iInf f) = ⨅ i, ⇑(f i)
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_iInf {ι : Sort*} (f : ι → Con M) : ⇑(iInf f) = ⨅ i, ⇑(f i) := by
  rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
Infimum of Congruence Relations as Infimum of Binary Relations (Indexed)
Informal description
For any family of congruence relations $\{c_i\}_{i \in \iota}$ on a multiplicative structure $M$, the underlying binary relation of the infimum of the family is equal to the infimum of the family of binary relations obtained by applying the coercion function to each congruence relation $c_i$. In other words, $\bigwedge_{i \in \iota} c_i = \bigwedge_{i \in \iota} c_i$ where the infima are taken in the lattice of binary relations on $M$.
Con.instPartialOrder instance
: PartialOrder (Con M)
Full source 
@[to_additive]
instance : PartialOrder (Con M) where
  le_refl _ _ _ := id
  le_trans _ _ _ h1 h2 _ _ h := h2 <| h1 h
  le_antisymm _ _ hc hd := ext fun _ _ => ⟨fun h => hc h, fun h => hd h⟩
Partial Order on Congruence Relations
Informal description
For any type $M$ with a multiplication operation, the set of congruence relations on $M$ forms a partial order under the relation $\leq$, where $c \leq d$ if and only if for all $x, y \in M$, $x \sim_c y$ implies $x \sim_d y$.
Con.instCompleteLattice instance
: CompleteLattice (Con M)
Full source 
/-- The complete lattice of congruence relations on a given type with a multiplication. -/
@[to_additive "The complete lattice of additive congruence relations on a given type with
an addition."]
instance : CompleteLattice (Con M) where
  __ := completeLatticeOfInf (Con M) fun s =>
      ⟨fun r hr x y h => (h : ∀ r ∈ s, (r : Con M) x y) r hr, fun r hr x y h r' hr' =>
        hr hr'
          h⟩
  inf c d := ⟨c.toSetoid ⊓ d.toSetoid, fun h1 h2 => ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩⟩
  inf_le_left _ _ := fun _ _ h => h.1
  inf_le_right _ _ := fun _ _ h => h.2
  le_inf  _ _ _ hb hc := fun _ _ h => ⟨hb h, hc h⟩
  top := { Setoid.completeLattice.top with mul' := by tauto }
  le_top _ := fun _ _ _ => trivial
  bot := { Setoid.completeLattice.bot with mul' := fun h1 h2 => h1 ▸ h2 ▸ rfl }
  bot_le c := fun x _ h => h ▸ c.refl x
Complete Lattice of Congruence Relations on a Multiplicative Structure
Informal description
For any type $M$ with a multiplication operation, the set of congruence relations on $M$ forms a complete lattice. This means that for any family of congruence relations on $M$, both their supremum (least upper bound) and infimum (greatest lower bound) exist and are themselves congruence relations on $M$.
Con.coe_inf theorem
{c d : Con M} : ⇑(c ⊓ d) = ⇑c ⊓ ⇑d
Full source 
/-- The infimum of two congruence relations equals the infimum of the underlying binary
    operations. -/
@[to_additive (attr := simp, norm_cast)
  "The infimum of two additive congruence relations equals the infimum of the underlying binary
  operations."]
theorem coe_inf {c d : Con M} : ⇑(c ⊓ d) = ⇑c ⊓ ⇑d :=
  rfl
Infimum of Congruence Relations as Infimum of Binary Relations
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, the underlying binary relation of their infimum $c \sqcap d$ is equal to the infimum of their underlying binary relations. That is, for all $x, y \in M$, $(c \sqcap d)(x, y) \leftrightarrow c(x, y) \wedge d(x, y)$.
Con.inf_iff_and theorem
{c d : Con M} {x y} : (c ⊓ d) x y ↔ c x y ∧ d x y
Full source 
/-- Definition of the infimum of two congruence relations. -/
@[to_additive "Definition of the infimum of two additive congruence relations."]
theorem inf_iff_and {c d : Con M} {x y} : (c ⊓ d) x y ↔ c x y ∧ d x y :=
  Iff.rfl
Characterization of Infimum of Congruence Relations: $(c \sqcap d)(x, y) \leftrightarrow c(x, y) \land d(x, y)$
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, and for any elements $x, y \in M$, the infimum relation $c \sqcap d$ relates $x$ and $y$ if and only if both $c$ relates $x$ and $y$ and $d$ relates $x$ and $y$. In other words, $(c \sqcap d)(x, y) \leftrightarrow c(x, y) \land d(x, y)$.
Con.conGen_eq theorem
(r : M → M → Prop) : conGen r = sInf {s : Con M | ∀ x y, r x y → s x y}
Full source 
/-- The inductively defined smallest congruence relation containing a binary relation `r` equals
    the infimum of the set of congruence relations containing `r`. -/
@[to_additive addConGen_eq "The inductively defined smallest additive congruence relation
containing a binary relation `r` equals the infimum of the set of additive congruence relations
containing `r`."]
theorem conGen_eq (r : M → M → Prop) : conGen r = sInf { s : Con M | ∀ x y, r x y → s x y } :=
  le_antisymm
    (le_sInf (fun s hs x y (hxy : (conGen r) x y) =>
      show s x y by
        apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
        · exact fun x y h => hs x y h
        · exact s.refl'
        · exact fun _ => s.symm'
        · exact fun _ _ => s.trans'
        · exact fun _ _ => s.mul))
    (sInf_le ConGen.Rel.of)
Smallest Congruence Relation as Infimum of Containing Relations
Informal description
For any binary relation $r$ on a multiplicative structure $M$, the smallest congruence relation $\operatorname{conGen}(r)$ containing $r$ is equal to the infimum of the set of all congruence relations on $M$ that contain $r$. In other words, \[ \operatorname{conGen}(r) = \bigwedge \{ s \in \operatorname{Con}(M) \mid \forall x y, r(x,y) \to s(x,y) \}. \]
Con.conGen_le theorem
{r : M → M → Prop} {c : Con M} (h : ∀ x y, r x y → c x y) : conGen r ≤ c
Full source 
/-- The smallest congruence relation containing a binary relation `r` is contained in any
    congruence relation containing `r`. -/
@[to_additive addConGen_le "The smallest additive congruence relation containing a binary
relation `r` is contained in any additive congruence relation containing `r`."]
theorem conGen_le {r : M → M → Prop} {c : Con M} (h : ∀ x y, r x y → c x y) :
    conGen r ≤ c := by rw [conGen_eq]; exact sInf_le h
Minimality of the Congruence Relation Generated by $r$
Informal description
For any binary relation $r$ on a multiplicative structure $M$ and any congruence relation $c$ on $M$, if $r(x,y)$ implies $c(x,y)$ for all $x, y \in M$, then the smallest congruence relation $\operatorname{conGen}(r)$ containing $r$ is contained in $c$, i.e., $\operatorname{conGen}(r) \leq c$.
Con.conGen_mono theorem
{r s : M → M → Prop} (h : ∀ x y, r x y → s x y) : conGen r ≤ conGen s
Full source 
/-- Given binary relations `r, s` with `r` contained in `s`, the smallest congruence relation
    containing `s` contains the smallest congruence relation containing `r`. -/
@[to_additive addConGen_mono "Given binary relations `r, s` with `r` contained in `s`, the
smallest additive congruence relation containing `s` contains the smallest additive congruence
relation containing `r`."]
theorem conGen_mono {r s : M → M → Prop} (h : ∀ x y, r x y → s x y) : conGen r ≤ conGen s :=
  conGen_le fun x y hr => ConGen.Rel.of _ _ <| h x y hr
Monotonicity of Congruence Relation Generation
Informal description
Let $M$ be a type with a multiplication operation, and let $r$ and $s$ be binary relations on $M$ such that $r(x,y)$ implies $s(x,y)$ for all $x, y \in M$. Then the smallest congruence relation $\operatorname{conGen}(r)$ containing $r$ is contained in the smallest congruence relation $\operatorname{conGen}(s)$ containing $s$, i.e., $\operatorname{conGen}(r) \leq \operatorname{conGen}(s)$.
Con.conGen_of_con theorem
(c : Con M) : conGen c = c
Full source 
/-- Congruence relations equal the smallest congruence relation in which they are contained. -/
@[to_additive (attr := simp) addConGen_of_addCon "Additive congruence relations equal the smallest
additive congruence relation in which they are contained."]
theorem conGen_of_con (c : Con M) : conGen c = c :=
  le_antisymm (by rw [conGen_eq]; exact sInf_le fun _ _ => id) ConGen.Rel.of
Congruence Relation is its Own Smallest Generator
Informal description
For any congruence relation $c$ on a multiplicative structure $M$, the smallest congruence relation containing $c$ is equal to $c$ itself, i.e., $\operatorname{conGen}(c) = c$.
Con.conGen_idem theorem
(r : M → M → Prop) : conGen (conGen r) = conGen r
Full source 
/-- The map sending a binary relation to the smallest congruence relation in which it is
    contained is idempotent. -/
@[to_additive addConGen_idem "The map sending a binary relation to the smallest additive
congruence relation in which it is contained is idempotent."]
theorem conGen_idem (r : M → M → Prop) : conGen (conGen r) = conGen r := by simp
Idempotence of the Congruence Relation Generator
Informal description
For any binary relation $r$ on a multiplicative structure $M$, the smallest congruence relation containing $r$ is idempotent, i.e., $\operatorname{conGen}(\operatorname{conGen}(r)) = \operatorname{conGen}(r)$.
Con.sup_eq_conGen theorem
(c d : Con M) : c ⊔ d = conGen fun x y => c x y ∨ d x y
Full source 
/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
    the binary relation '`x` is related to `y` by `c` or `d`'. -/
@[to_additive sup_eq_addConGen "The supremum of additive congruence relations `c, d` equals the
smallest additive congruence relation containing the binary relation '`x` is related to `y`
by `c` or `d`'."]
theorem sup_eq_conGen (c d : Con M) : c ⊔ d = conGen fun x y => c x y ∨ d x y := by
  rw [conGen_eq]
  apply congr_arg sInf
  simp only [le_def, or_imp, ← forall_and]
Supremum of Congruence Relations as Generated Relation
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, the supremum $c \sqcup d$ is equal to the smallest congruence relation containing the binary relation defined by $x \sim y$ if and only if $x \sim_c y$ or $x \sim_d y$.
Con.sup_def theorem
{c d : Con M} : c ⊔ d = conGen (⇑c ⊔ ⇑d)
Full source 
/-- The supremum of two congruence relations equals the smallest congruence relation containing
    the supremum of the underlying binary operations. -/
@[to_additive "The supremum of two additive congruence relations equals the smallest additive
congruence relation containing the supremum of the underlying binary operations."]
theorem sup_def {c d : Con M} : c ⊔ d = conGen (⇑c ⊔ ⇑d) := by rw [sup_eq_conGen]; rfl
Supremum of Congruence Relations as Generated Relation from Pointwise Supremum
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$, the supremum $c \sqcup d$ is equal to the smallest congruence relation containing the pointwise supremum of the relations $c$ and $d$.
Con.sSup_eq_conGen theorem
(S : Set (Con M)) : sSup S = conGen fun x y => ∃ c : Con M, c ∈ S ∧ c x y
Full source 
/-- The supremum of a set of congruence relations `S` equals the smallest congruence relation
    containing the binary relation 'there exists `c ∈ S` such that `x` is related to `y` by
    `c`'. -/
@[to_additive sSup_eq_addConGen "The supremum of a set of additive congruence relations `S` equals
the smallest additive congruence relation containing the binary relation 'there exists `c ∈ S`
such that `x` is related to `y` by `c`'."]
theorem sSup_eq_conGen (S : Set (Con M)) :
    sSup S = conGen fun x y => ∃ c : Con M, c ∈ S ∧ c x y := by
  rw [conGen_eq]
  apply congr_arg sInf
  ext
  exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩
Supremum of Congruence Relations as Generated Relation
Informal description
For any set $S$ of congruence relations on a multiplicative structure $M$, the supremum of $S$ is equal to the smallest congruence relation containing the binary relation defined by: $x \sim y$ if and only if there exists a congruence relation $c \in S$ such that $c(x, y)$ holds.
Con.sSup_def theorem
{S : Set (Con M)} : sSup S = conGen (sSup ((⇑) '' S))
Full source 
/-- The supremum of a set of congruence relations is the same as the smallest congruence relation
    containing the supremum of the set's image under the map to the underlying binary relation. -/
@[to_additive "The supremum of a set of additive congruence relations is the same as the smallest
additive congruence relation containing the supremum of the set's image under the map to the
underlying binary relation."]
theorem sSup_def {S : Set (Con M)} :
    sSup S = conGen (sSup ((⇑) '' S)) := by
  rw [sSup_eq_conGen, sSup_image]
  congr with (x y)
  simp only [sSup_image, iSup_apply, iSup_Prop_eq, exists_prop, rel_eq_coe]
Supremum of Congruence Relations as Generated Supremum of Binary Relations
Informal description
For any set $S$ of congruence relations on a multiplicative structure $M$, the supremum of $S$ is equal to the smallest congruence relation containing the supremum of the image of $S$ under the coercion map to binary relations. In other words, $\bigvee S = \text{conGen}(\bigvee \{c \mid c \in S\})$, where $\bigvee$ denotes the supremum operation.
Con.gi definition
: @GaloisInsertion (M → M → Prop) (Con M) _ _ conGen DFunLike.coe
Full source 
/-- There is a Galois insertion of congruence relations on a type with a multiplication `M` into
    binary relations on `M`. -/
@[to_additive "There is a Galois insertion of additive congruence relations on a type with
an addition `M` into binary relations on `M`."]
protected def gi : @GaloisInsertion (M → M → Prop) (Con M) _ _ conGen DFunLike.coe where
  choice r _ := conGen r
  gc _ c := ⟨fun H _ _ h => H <| ConGen.Rel.of _ _ h, @fun H => conGen_of_con c ▸ conGen_mono H⟩
  le_l_u x := (conGen_of_con x).symm ▸ le_refl x
  choice_eq _ _ := rfl
Galois insertion between binary relations and congruence relations on a multiplicative structure
Informal description
There is a Galois insertion between the set of binary relations on a multiplicative structure $M$ and the set of congruence relations on $M$. The insertion is given by the function `conGen`, which maps a binary relation to the smallest congruence relation containing it, and the coercion function that maps a congruence relation back to its underlying binary relation. Specifically, for any binary relation $r$ on $M$, `conGen r` is the smallest congruence relation containing $r$, and for any congruence relation $c$ on $M$, the underlying binary relation of $c$ is $c$ itself. The Galois insertion satisfies the following properties: 1. For any binary relation $r$ and congruence relation $c$, `conGen r ≤ c` if and only if $r ≤ c$ as binary relations. 2. The composition of the coercion followed by `conGen` is the identity on congruence relations. 3. The composition of `conGen` followed by the coercion is extensive, meaning $r ≤ \text{conGen}(r)$ for any binary relation $r$.
Con.comap definition
(f : M → N) (H : ∀ x y, f (x * y) = f x * f y) (c : Con N) : Con M
Full source 
/-- Given types with multiplications `M, N` and a congruence relation `c` on `N`, a
    multiplication-preserving map `f : M → N` induces a congruence relation on `f`'s domain
    defined by '`x ≈ y` iff `f(x)` is related to `f(y)` by `c`.' -/
@[to_additive "Given types with additions `M, N` and an additive congruence relation `c` on `N`,
an addition-preserving map `f : M → N` induces an additive congruence relation on `f`'s domain
defined by '`x ≈ y` iff `f(x)` is related to `f(y)` by `c`.' "]
def comap (f : M → N) (H : ∀ x y, f (x * y) = f x * f y) (c : Con N) : Con M :=
  { c.toSetoid.comap f with
    mul' := @fun w x y z h1 h2 => show c (f (w * y)) (f (x * z)) by rw [H, H]; exact c.mul h1 h2 }
Pullback of a congruence relation along a multiplicative map
Informal description
Given types $M$ and $N$ with multiplication operations, a congruence relation $c$ on $N$, and a multiplication-preserving map $f : M \to N$ (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), the congruence relation $\text{comap}\, f\, H\, c$ on $M$ is defined by $x \sim y$ if and only if $f(x) \sim f(y)$ under $c$.
Con.comap_rel theorem
{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)
Full source 
@[to_additive (attr := simp)]
theorem comap_rel {f : M → N} (H : ∀ x y, f (x * y) = f x * f y) {c : Con N} {x y : M} :
    comapcomap f H c x y ↔ c (f x) (f y) :=
  Iff.rfl
Characterization of Pullback Congruence Relation via Multiplicative Map
Informal description
Let $M$ and $N$ be types with multiplication operations, $f : M \to N$ be a multiplicative map (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), and $c$ be a congruence relation on $N$. For any $x, y \in M$, the relation $\text{comap}\, f\, H\, c$ holds between $x$ and $y$ if and only if $c$ holds between $f(x)$ and $f(y)$. In other words, $x \sim y$ under $\text{comap}\, f\, H\, c$ if and only if $f(x) \sim f(y)$ under $c$.
Con.mulOneClass instance
: MulOneClass c.Quotient
Full source 
/-- The quotient of a monoid by a congruence relation is a monoid. -/
@[to_additive "The quotient of an `AddMonoid` by an additive congruence relation is
an `AddMonoid`."]
instance mulOneClass : MulOneClass c.Quotient where
  one := ((1 : M) : c.Quotient)
  mul_one x := Quotient.inductionOn' x fun _ => congr_arg ((↑) : M → c.Quotient) <| mul_one _
  one_mul x := Quotient.inductionOn' x fun _ => congr_arg ((↑) : M → c.Quotient) <| one_mul _
Monoid Structure on Quotient by Congruence Relation
Informal description
The quotient $M/c$ of a monoid $M$ by a congruence relation $c$ inherits a monoid structure, where the multiplication is defined by $[x] \cdot [y] = [x \cdot y]$ and the identity element is $[1]$.
Con.coe_one theorem
: ((1 : M) : c.Quotient) = 1
Full source 
/-- The 1 of the quotient of a monoid by a congruence relation is the equivalence class of the
    monoid's 1. -/
@[to_additive (attr := simp) "The 0 of the quotient of an `AddMonoid` by an additive congruence
relation is the equivalence class of the `AddMonoid`'s 0."]
theorem coe_one : ((1 : M) : c.Quotient) = 1 :=
  rfl
Identity Preservation in Quotient Monoid: $[1] = 1$
Informal description
For a monoid $M$ with a congruence relation $c$, the equivalence class of the multiplicative identity $1$ in $M$ is equal to the multiplicative identity in the quotient monoid $M/c$, i.e., $[1] = 1$.
Con.Quotient.inhabited instance
: Inhabited c.Quotient
Full source 
/-- There exists an element of the quotient of a monoid by a congruence relation (namely 1). -/
@[to_additive "There exists an element of the quotient of an `AddMonoid` by a congruence relation
(namely 0)."]
instance Quotient.inhabited : Inhabited c.Quotient :=
  ⟨((1 : M) : c.Quotient)⟩
Quotient by Congruence Relation is Inhabited
Informal description
For any monoid $M$ with a congruence relation $c$, the quotient $M/c$ is inhabited (i.e., it has at least one element).
Con.pow theorem
{M : Type*} [Monoid M] (c : Con M) : ∀ (n : ℕ) {w x}, c w x → c (w ^ n) (x ^ n)
Full source 
/-- Multiplicative congruence relations preserve natural powers. -/
@[to_additive "Additive congruence relations preserve natural scaling."]
protected theorem pow {M : Type*} [Monoid M] (c : Con M) :
    ∀ (n : ℕ) {w x}, c w x → c (w ^ n) (x ^ n)
  | 0, w, x, _ => by simpa using c.refl _
  | Nat.succ n, w, x, h => by simpa [pow_succ] using c.mul (Con.pow c n h) h
Congruence Relations Preserve Natural Powers in Monoids
Informal description
Let $M$ be a monoid with a congruence relation $c$. For any natural number $n$ and any elements $w, x \in M$ such that $w \sim x$ under $c$, we have $w^n \sim x^n$ under $c$.
Con.one instance
[MulOneClass M] (c : Con M) : One c.Quotient
Full source 
@[to_additive]
instance one [MulOneClass M] (c : Con M) : One c.Quotient where
  -- Using Quotient.mk'' here instead of c.toQuotient
  -- since c.toQuotient is not reducible.
  -- This would lead to non-defeq diamonds since this instance ends up in
  -- quotients modulo ideals.
  one := Quotient.mk'' (1 : M)
Identity Element in the Quotient by a Congruence Relation
Informal description
For any multiplicative monoid $M$ with a congruence relation $c$, the quotient $M/c$ has a canonical identity element.
AddCon.Quotient.nsmul instance
{M : Type*} [AddMonoid M] (c : AddCon M) : SMul ℕ c.Quotient
Full source 
instance _root_.AddCon.Quotient.nsmul {M : Type*} [AddMonoid M] (c : AddCon M) :
    SMul ℕ c.Quotient where
  smul n := (Quotient.map' (n • ·)) fun _ _ => c.nsmul n
Natural Scalar Multiplication on the Quotient of an Additive Monoid by a Congruence Relation
Informal description
For any additive monoid $M$ with a congruence relation $c$, the quotient $M/c$ has a canonical scalar multiplication by natural numbers, where $n \cdot [x] = [n \cdot x]$ for any $n \in \mathbb{N}$ and $x \in M$.
Con.instPowQuotientNat instance
{M : Type*} [Monoid M] (c : Con M) : Pow c.Quotient ℕ
Full source 
@[to_additive existing AddCon.Quotient.nsmul]
instance {M : Type*} [Monoid M] (c : Con M) : Pow c.Quotient ℕ where
  pow x n := Quotient.map' (fun x => x ^ n) (fun _ _ => c.pow n) x
Natural Power Operation on Quotient by Congruence Relation
Informal description
For any monoid $M$ with a congruence relation $c$, the quotient $M/c$ is equipped with a natural power operation, where for any equivalence class $[x] \in M/c$ and natural number $n$, we define $[x]^n = [x^n]$.
Con.semigroup instance
{M : Type*} [Semigroup M] (c : Con M) : Semigroup c.Quotient
Full source 
/-- The quotient of a semigroup by a congruence relation is a semigroup. -/
@[to_additive "The quotient of an `AddSemigroup` by an additive congruence relation is
an `AddSemigroup`."]
instance semigroup {M : Type*} [Semigroup M] (c : Con M) : Semigroup c.Quotient := fast_instance%
  Function.Surjective.semigroup _ Quotient.mk''_surjective fun _ _ => rfl
Semigroup Structure on the Quotient by a Congruence Relation
Informal description
For any semigroup $M$ and congruence relation $c$ on $M$, the quotient $M/c$ inherits a semigroup structure where the multiplication is defined by $[x] \cdot [y] = [x \cdot y]$ for $x, y \in M$.
Con.commSemigroup instance
{M : Type*} [CommSemigroup M] (c : Con M) : CommSemigroup c.Quotient
Full source 
/-- The quotient of a commutative semigroup by a congruence relation is a semigroup. -/
@[to_additive "The quotient of an `AddCommSemigroup` by an additive congruence relation is
an `AddCommSemigroup`."]
instance commSemigroup {M : Type*} [CommSemigroup M] (c : Con M) : CommSemigroup c.Quotient :=
  Function.Surjective.commSemigroup _ Quotient.mk''_surjective fun _ _ => rfl
Quotient of a Commutative Semigroup by a Congruence Relation is a Commutative Semigroup
Informal description
For any commutative semigroup $M$ and congruence relation $c$ on $M$, the quotient $M/c$ inherits a commutative semigroup structure where the multiplication is defined by $[x] \cdot [y] = [x \cdot y]$ for $x, y \in M$.
Con.monoid instance
{M : Type*} [Monoid M] (c : Con M) : Monoid c.Quotient
Full source 
/-- The quotient of a monoid by a congruence relation is a monoid. -/
@[to_additive "The quotient of an `AddMonoid` by an additive congruence relation is
an `AddMonoid`."]
instance monoid {M : Type*} [Monoid M] (c : Con M) : Monoid c.Quotient := fast_instance%
  Function.Surjective.monoid _ Quotient.mk''_surjective rfl (fun _ _ => rfl) fun _ _ => rfl
Monoid Structure on the Quotient by a Congruence Relation
Informal description
For any monoid $M$ and congruence relation $c$ on $M$, the quotient $M/c$ inherits a monoid structure where the multiplication is defined by $[x] \cdot [y] = [x \cdot y]$ for $x, y \in M$, and the identity element is $[1]$.
Con.commMonoid instance
{M : Type*} [CommMonoid M] (c : Con M) : CommMonoid c.Quotient
Full source 
/-- The quotient of a `CommMonoid` by a congruence relation is a `CommMonoid`. -/
@[to_additive "The quotient of an `AddCommMonoid` by an additive congruence
relation is an `AddCommMonoid`."]
instance commMonoid {M : Type*} [CommMonoid M] (c : Con M) : CommMonoid c.Quotient := fast_instance%
  fast_instance% Function.Surjective.commMonoid _ Quotient.mk''_surjective rfl
    (fun _ _ => rfl) fun _ _ => rfl
Quotient of a Commutative Monoid by a Congruence Relation is a Commutative Monoid
Informal description
For any commutative monoid $M$ and congruence relation $c$ on $M$, the quotient $M/c$ inherits a commutative monoid structure where the multiplication is defined by $[x] \cdot [y] = [x \cdot y]$ for $x, y \in M$, and the identity element is $[1]$.
Con.map_of_mul_left_rel_one theorem
[Monoid M] (c : Con M) (f : M → M) (hf : ∀ x, c (f x * x) 1) {x y} (h : c x y) : c (f x) (f y)
Full source 
/-- Sometimes, a group is defined as a quotient of a monoid by a congruence relation.
Usually, the inverse operation is defined as `Setoid.map f _` for some `f`.
This lemma allows to avoid code duplication in the definition of the inverse operation:
instead of proving both `∀ x y, c x y → c (f x) (f y)` (to define the operation)
and `∀ x, c (f x * x) 1` (to prove the group laws), one can only prove the latter. -/
@[to_additive "Sometimes, an additive group is defined as a quotient of a monoid
  by an additive congruence relation.
  Usually, the inverse operation is defined as `Setoid.map f _` for some `f`.
  This lemma allows to avoid code duplication in the definition of the inverse operation:
  instead of proving both `∀ x y, c x y → c (f x) (f y)` (to define the operation)
  and `∀ x, c (f x + x) 0` (to prove the group laws), one can only prove the latter."]
theorem map_of_mul_left_rel_one [Monoid M] (c : Con M)
    (f : M → M) (hf : ∀ x, c (f x * x) 1) {x y} (h : c x y) : c (f x) (f y) := by
  simp only [← Con.eq, coe_one, coe_mul] at *
  have hf' : ∀ x : M, (x : c.Quotient) * f x = 1 := fun x ↦
    calc
      (x : c.Quotient) * f x = f (f x) * f x * (x * f x) := by simp [hf]
      _ = f (f x) * (f x * x) * f x := by ac_rfl
      _ = 1 := by simp [hf]
  have : (⟨_, _, hf' x, hf x⟩ : c.Quotientˣ) = ⟨_, _, hf' y, hf y⟩ := Units.ext h
  exact congr_arg Units.inv this
Congruence Preservation under Left Multiplication Condition
Informal description
Let $M$ be a monoid with a congruence relation $c$, and let $f : M \to M$ be a function such that for every $x \in M$, the relation $c(f(x) \cdot x, 1)$ holds. Then for any $x, y \in M$ with $c(x, y)$, we have $c(f(x), f(y))$.
Con.inv theorem
{x y} (h : c x y) : c x⁻¹ y⁻¹
Full source 
/-- Multiplicative congruence relations preserve inversion. -/
@[to_additive "Additive congruence relations preserve negation."]
protected theorem inv {x y} (h : c x y) : c x⁻¹ y⁻¹ :=
  c.map_of_mul_left_rel_one Inv.inv (fun x => by simp only [inv_mul_cancel, c.refl 1]) h
Congruence Relations Preserve Inverses
Informal description
For any congruence relation $c$ on a multiplicative structure $M$ and any elements $x, y \in M$, if $x \sim y$ under $c$, then their inverses satisfy $x^{-1} \sim y^{-1}$ under $c$.
Con.div theorem
: ∀ {w x y z}, c w x → c y z → c (w / y) (x / z)
Full source 
/-- Multiplicative congruence relations preserve division. -/
@[to_additive "Additive congruence relations preserve subtraction."]
protected theorem div : ∀ {w x y z}, c w x → c y z → c (w / y) (x / z) := @fun w x y z h1 h2 => by
  simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2)
Division Preservation under Congruence Relations
Informal description
For any congruence relation $c$ on a multiplicative structure $M$ and any elements $w, x, y, z \in M$, if $w \sim x$ and $y \sim z$ under $c$, then $w / y \sim x / z$ under $c$.
Con.zpow theorem
: ∀ (n : ℤ) {w x}, c w x → c (w ^ n) (x ^ n)
Full source 
/-- Multiplicative congruence relations preserve integer powers. -/
@[to_additive "Additive congruence relations preserve integer scaling."]
protected theorem zpow : ∀ (n : ℤ) {w x}, c w x → c (w ^ n) (x ^ n)
  | Int.ofNat n, w, x, h => by simpa only [zpow_natCast, Int.ofNat_eq_coe] using c.pow n h
  | Int.negSucc n, w, x, h => by simpa only [zpow_negSucc] using c.inv (c.pow _ h)
Congruence Relations Preserve Integer Powers in Monoids
Informal description
Let $M$ be a monoid with a congruence relation $c$. For any integer $n$ and any elements $w, x \in M$ such that $w \sim x$ under $c$, we have $w^n \sim x^n$ under $c$.
Con.hasInv instance
: Inv c.Quotient
Full source 
/-- The inversion induced on the quotient by a congruence relation on a type with an
    inversion. -/
@[to_additive "The negation induced on the quotient by an additive congruence relation on a type
with a negation."]
instance hasInv : Inv c.Quotient :=
  ⟨(Quotient.map' Inv.inv) fun _ _ => c.inv⟩
Inversion on the Quotient by a Congruence Relation
Informal description
For any congruence relation $c$ on a multiplicative structure $M$ with an inversion operation, the quotient $M/c$ inherits an inversion operation defined by $\overline{x}^{-1} = \overline{x^{-1}}$ for any $x \in M$, where $\overline{x}$ denotes the equivalence class of $x$ under $c$.
Con.hasDiv instance
: Div c.Quotient
Full source 
/-- The division induced on the quotient by a congruence relation on a type with a
    division. -/
@[to_additive "The subtraction induced on the quotient by an additive congruence relation on a type
with a subtraction."]
instance hasDiv : Div c.Quotient :=
  ⟨(Quotient.map₂ (· / ·)) fun _ _ h₁ _ _ h₂ => c.div h₁ h₂⟩
Division Operation on the Quotient by a Congruence Relation
Informal description
For any congruence relation $c$ on a type $M$ with a division operation, the quotient $M/c$ inherits a division operation defined by $\overline{x} / \overline{y} = \overline{x / y}$ for any $x, y \in M$, where $\overline{x}$ denotes the equivalence class of $x$ under $c$.
AddCon.Quotient.zsmul instance
{M : Type*} [AddGroup M] (c : AddCon M) : SMul ℤ c.Quotient
Full source 
/-- The integer scaling induced on the quotient by a congruence relation on a type with a
    subtraction. -/
instance _root_.AddCon.Quotient.zsmul {M : Type*} [AddGroup M] (c : AddCon M) :
    SMul ℤ c.Quotient :=
  ⟨fun z => (Quotient.map' (z • ·)) fun _ _ => c.zsmul z⟩
$\mathbb{Z}$-scalar multiplication on the quotient by an additive congruence relation
Informal description
For any additive group $M$ with an additive congruence relation $c$, the quotient $M/c$ inherits a $\mathbb{Z}$-scalar multiplication operation defined by $n \cdot \overline{x} = \overline{n \cdot x}$ for any $n \in \mathbb{Z}$ and $x \in M$, where $\overline{x}$ denotes the equivalence class of $x$ under $c$.
Con.zpowinst instance
: Pow c.Quotient ℤ
Full source 
/-- The integer power induced on the quotient by a congruence relation on a type with a
    division. -/
@[to_additive existing AddCon.Quotient.zsmul]
instance zpowinst : Pow c.Quotient ℤ :=
  ⟨fun x z => Quotient.map' (fun x => x ^ z) (fun _ _ h => c.zpow z h) x⟩
Integer Power Operation on Quotient by Congruence Relation
Informal description
For a monoid $M$ with a congruence relation $c$, the quotient $M/c$ inherits a canonical integer power operation. Specifically, for any integer $n$ and equivalence class $[x] \in M/c$, the power $[x]^n$ is defined as $[x^n]$, where $x^n$ is the $n$-th power of $x$ in $M$.
Con.group instance
: Group c.Quotient
Full source 
/-- The quotient of a group by a congruence relation is a group. -/
@[to_additive "The quotient of an `AddGroup` by an additive congruence relation is
an `AddGroup`."]
instance group : Group c.Quotient := fast_instance%
  Function.Surjective.group Quotient.mk'' Quotient.mk''_surjective
    rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
Group Structure on the Quotient by a Congruence Relation
Informal description
For any group $G$ and congruence relation $c$ on $G$, the quotient $G/c$ inherits a group structure where the multiplication is defined by $[x] \cdot [y] = [x \cdot y]$ for $x, y \in G$, the identity element is $[1]$, and the inverse of $[x]$ is $[x^{-1}]$.
Con.commGroup instance
{M : Type*} [CommGroup M] (c : Con M) : CommGroup c.Quotient
Full source 
/-- The quotient of a `CommGroup` by a congruence relation is a `CommGroup`. -/
@[to_additive "The quotient of an `AddCommGroup` by an additive congruence
relation is an `AddCommGroup`."]
instance commGroup {M : Type*} [CommGroup M] (c : Con M) : CommGroup c.Quotient := fast_instance%
  Function.Surjective.commGroup _ Quotient.mk''_surjective rfl (fun _ _ => rfl) (fun _ => rfl)
      (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
Commutative Group Structure on Quotient by Congruence Relation
Informal description
For any commutative group $M$ and congruence relation $c$ on $M$, the quotient $M/c$ inherits a commutative group structure where the multiplication is defined by $[x] \cdot [y] = [x \cdot y]$ for $x, y \in M$, the identity element is $[1]$, and the inverse of $[x]$ is $[x^{-1}]$.
Con.liftOnUnits definition
(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') : α
Full source 
/-- In order to define a function `(Con.Quotient c)ˣ → α` on the units of `Con.Quotient c`,
where `c : Con M` is a multiplicative congruence on a monoid, it suffices to define a function `f`
that takes elements `x y : M` with proofs of `c (x * y) 1` and `c (y * x) 1`, and returns an element
of `α` provided that `f x y _ _ = f x' y' _ _` whenever `c x x'` and `c y y'`. -/
@[to_additive]
def liftOnUnits (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') : α := by
  refine
    Con.hrecOn₂ (cN := c) (φ := fun x y => x * y = 1 → y * x = 1 → α) (u : c.Quotient)
      (↑u⁻¹ : c.Quotient)
      (fun (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))
      (fun x y x' y' hx hy => ?_) u.3 u.4
  refine Function.hfunext ?_ ?_
  · rw [c.eq.2 hx, c.eq.2 hy]
  · rintro Hxy Hxy' -
    refine Function.hfunext ?_ ?_
    · rw [c.eq.2 hx, c.eq.2 hy]
    · rintro Hyx Hyx' -
      exact heq_of_eq (Hf _ _ _ _ _ _ _ _ hx hy)
Lifting a function to units of the quotient monoid by a congruence relation
Informal description
Given a monoid $M$ with a congruence relation $c$, a function $f \colon M \times M \to \alpha$ defined on pairs $(x, y)$ satisfying $c(x \cdot y, 1)$ and $c(y \cdot x, 1)$, and a proof that $f$ respects the congruence relation (i.e., $f(x, y, \_, \_) = f(x', y', \_, \_)$ whenever $c(x, x')$ and $c(y, y')$), the function `Con.liftOnUnits` lifts $f$ to a function defined on the units of the quotient monoid $M/c$. Specifically, for any unit $u \in (M/c)^\times$, `Con.liftOnUnits u f Hf` evaluates to $f(x, y, h_{xy}, h_{yx})$, where $x, y \in M$ are representatives of $u$ and $u^{-1}$ respectively, and $h_{xy}$, $h_{yx}$ are proofs that $x \cdot y$ and $y \cdot x$ are congruent to $1$ under $c$.
Con.liftOnUnits_mk theorem
(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') (x y : M) (hxy hyx) : liftOnUnits ⟨(x : c.Quotient), y, hxy, hyx⟩ f Hf = f x y (c.eq.1 hxy) (c.eq.1 hyx)
Full source 
@[to_additive (attr := simp)]
theorem liftOnUnits_mk (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')
    (x y : M) (hxy hyx) :
    liftOnUnits ⟨(x : c.Quotient), y, hxy, hyx⟩ f Hf = f x y (c.eq.1 hxy) (c.eq.1 hyx) :=
  rfl
Evaluation of Lifted Function on Units in Quotient Monoid by Congruence Relation
Informal description
Let $M$ be a monoid with a congruence relation $c$, and let $f \colon M \times M \to \alpha$ be a function defined on pairs $(x, y)$ such that $c(x \cdot y, 1)$ and $c(y \cdot x, 1)$. Suppose $f$ respects the congruence relation, i.e., for all $x, y, x', y' \in M$ with $c(x, x')$ and $c(y, y')$, we have $f(x, y, \_, \_) = f(x', y', \_, \_)$. Then, for any $x, y \in M$ and proofs $hxy \colon c(x \cdot y, 1)$, $hyx \colon c(y \cdot x, 1)$, the function `liftOnUnits` evaluated at the unit $\langle [x], [y], hxy, hyx \rangle$ in the quotient monoid $M/c$ satisfies \[ \text{liftOnUnits} \langle [x], [y], hxy, hyx \rangle f Hf = f(x, y, c(x \cdot y, 1), c(y \cdot x, 1)). \]
Con.induction_on_units theorem
{p : Units c.Quotient → Prop} (u : Units c.Quotient) (H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p ⟨x, y, c.eq.2 hxy, c.eq.2 hyx⟩) : p u
Full source 
@[to_additive (attr := elab_as_elim)]
theorem induction_on_units {p : Units c.Quotient → Prop} (u : Units c.Quotient)
    (H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p ⟨x, y, c.eq.2 hxy, c.eq.2 hyx⟩) :
    p u := by
  rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩
  exact H x y (c.eq.1 h₁) (c.eq.1 h₂)
Induction Principle for Units in Quotient Monoid by Congruence Relation
Informal description
Let $M$ be a monoid with a congruence relation $c$, and let $p$ be a predicate on the units of the quotient monoid $M/c$. For any unit $u$ in $M/c$, if for all $x, y \in M$ such that $c(x \cdot y, 1)$ and $c(y \cdot x, 1)$ the predicate $p$ holds for the unit $\langle [x], [y], hxy, hyx \rangle$ (where $hxy$ and $hyx$ are proofs that $[x \cdot y] = [1]$ and $[y \cdot x] = [1]$ respectively), then $p$ holds for $u$.