/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module order.rel_iso.group
! leanprover-community/mathlib commit 62a5626868683c104774de8d85b9855234ac807c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Defs
import Mathlib.Order.RelIso.Basic

/-!
# Relation isomorphisms form a group
-/


variable {
α: Type ?u.11
α : 
Type _: Type (?u.2929+1)
Type _} {
r: α → α → Prop
r : 
α: Type ?u.2
α → 
α: Type ?u.2
α → 
Prop: Type
Prop}

namespace RelIso

instance: {α : Type u_1} → {r : α → α → Prop} → Group (r ≃r r)
instance : 
Group: Type ?u.20 → Type ?u.20
Group (
r: α → α → Prop
r ≃r 
r: α → α → Prop
r) where
  one := 
RelIso.refl: {α : Type ?u.191} → (r : α → α → Prop) → r ≃r r
RelIso.refl 
r: α → α → Prop
r
  mul 
f₁: ?m.54
f₁ 
f₂: ?m.57
f₂ := 
f₂: ?m.57
f₂.
trans: {α : Type ?u.61} →
  {β : Type ?u.60} →
    {γ : Type ?u.59} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≃r s → s ≃r t → r ≃r t
trans 
f₁: ?m.54
f₁
  inv := 
RelIso.symm: {α : Type ?u.273} → {β : Type ?u.272} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → s ≃r r
RelIso.symm
  mul_assoc 
f₁: ?m.95
f₁ 
f₂: ?m.98
f₂ 
f₃: ?m.101
f₃ := 
rfl: ∀ {α : Sort ?u.103} {a : α}, a = a
rfl
  one_mul 
f: ?m.200
f := 
ext: ∀ {α : Type ?u.202} {β : Type ?u.203} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ≃r s⦄,
  (∀ (x : α), ↑f x = ↑g x) → f = g
ext fun 
_: ?m.223
_ => 
rfl: ∀ {α : Sort ?u.225} {a : α}, a = a
rfl
  mul_one 
f: ?m.233
f := 
ext: ∀ {α : Type ?u.235} {β : Type ?u.236} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ≃r s⦄,
  (∀ (x : α), ↑f x = ↑g x) → f = g
ext fun 
_: ?m.256
_ => 
rfl: ∀ {α : Sort ?u.258} {a : α}, a = a
rfl
  mul_left_inv 
f: ?m.327
f := 
ext: ∀ {α : Type ?u.329} {β : Type ?u.330} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ≃r s⦄,
  (∀ (x : α), ↑f x = ↑g x) → f = g
ext 
f: ?m.327
f.
symm_apply_apply: ∀ {α : Type ?u.349} {β : Type ?u.350} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : α),
  ↑(RelIso.symm e) (↑e x) = x
symm_apply_apply

@[simp]
theorem 
coe_one: ↑1 = id
coe_one : ((
1: ?m.1714
1 : 
r: α → α → Prop
r ≃r 
r: α → α → Prop
r) : 
α: Type ?u.1683
α → 
α: Type ?u.1683
α) = 
id: {α : Sort ?u.1821} → α → α
id :=
  
rfl: ∀ {α : Sort ?u.1862} {a : α}, a = a
rfl
#align rel_iso.coe_one 
RelIso.coe_one: ∀ {α : Type u_1} {r : α → α → Prop}, ↑1 = id
RelIso.coe_one

@[simp]
theorem 
coe_mul: ∀ (e₁ e₂ : r ≃r r), ↑(e₁ * e₂) = ↑e₁ ∘ ↑e₂
coe_mul (
e₁: r ≃r r
e₁ 
e₂: r ≃r r
e₂ : 
r: α → α → Prop
r ≃r 
r: α → α → Prop
r) : ((
e₁: r ≃r r
e₁ * 
e₂: r ≃r r
e₂) : 
α: Type ?u.1901
α → 
α: Type ?u.1901
α) = 
e₁: r ≃r r
e₁ ∘ 
e₂: r ≃r r
e₂ :=
  
rfl: ∀ {α : Sort ?u.2880} {a : α}, a = a
rfl
#align rel_iso.coe_mul 
RelIso.coe_mul: ∀ {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r), ↑(e₁ * e₂) = ↑e₁ ∘ ↑e₂
RelIso.coe_mul

theorem 
mul_apply: ∀ {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) (x : α), ↑(e₁ * e₂) x = ↑e₁ (↑e₂ x)
mul_apply (
e₁: r ≃r r
e₁ 
e₂: r ≃r r
e₂ : 
r: α → α → Prop
r ≃r 
r: α → α → Prop
r) (
x: α
x : 
α: Type ?u.2929
α) : (
e₁: r ≃r r
e₁ * 
e₂: r ≃r r
e₂) 
x: α
x = 
e₁: r ≃r r
e₁ (
e₂: r ≃r r
e₂ 
x: α
x) :=
  
rfl: ∀ {α : Sort ?u.3188} {a : α}, a = a
rfl
#align rel_iso.mul_apply 
RelIso.mul_apply: ∀ {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) (x : α), ↑(e₁ * e₂) x = ↑e₁ (↑e₂ x)
RelIso.mul_apply

@[simp]
theorem 
inv_apply_self: ∀ {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α), ↑e⁻¹ (↑e x) = x
inv_apply_self (
e: r ≃r r
e : 
r: α → α → Prop
r ≃r 
r: α → α → Prop
r) (
x: α
x) : 
e: r ≃r r
e⁻¹ (
e: r ≃r r
e 
x: ?m.3231
x) = 
x: ?m.3231
x :=
  
e: r ≃r r
e.
symm_apply_apply: ∀ {α : Type ?u.3356} {β : Type ?u.3357} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : α),
  ↑(RelIso.symm e) (↑e x) = x
symm_apply_apply 
x: α
x
#align rel_iso.inv_apply_self 
RelIso.inv_apply_self: ∀ {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α), ↑e⁻¹ (↑e x) = x
RelIso.inv_apply_self

@[simp]
theorem 
apply_inv_self: ∀ {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α), ↑e (↑e⁻¹ x) = x
apply_inv_self (
e: r ≃r r
e : 
r: α → α → Prop
r ≃r 
r: α → α → Prop
r) (
x: α
x) : 
e: r ≃r r
e (
e: r ≃r r
e⁻¹ 
x: ?m.3444
x) = 
x: ?m.3444
x :=
  
e: r ≃r r
e.
apply_symm_apply: ∀ {α : Type ?u.3569} {β : Type ?u.3570} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : β),
  ↑e (↑(RelIso.symm e) x) = x
apply_symm_apply 
x: α
x
#align rel_iso.apply_inv_self 
RelIso.apply_inv_self: ∀ {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α), ↑e (↑e⁻¹ x) = x
RelIso.apply_inv_self

end RelIso