Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro

! This file was ported from Lean 3 source module order.rel_iso.basic
! leanprover-community/mathlib commit f29120f82f6e24a6f6579896dfa2de6769fec962
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.FunLike.Basic
import Mathlib.Logic.Embedding.Basic
import Mathlib.Order.RelClasses

/-!
# Relation homomorphisms, embeddings, isomorphisms

This file defines relation homomorphisms, embeddings, isomorphisms and order embeddings and
isomorphisms.

## Main declarations

* `RelHom`: Relation homomorphism. A `RelHom r s` is a function `f : α → β` such that
`r a b → s (f a) (f b)`.
* `RelEmbedding`: Relation embedding. A `RelEmbedding r s` is an embedding `f : α ↪ β` such that
`r a b ↔ s (f a) (f b)`.
* `RelIso`: Relation isomorphism. A `RelIso r s` is an equivalence `f : α ≃ β` such that
`r a b ↔ s (f a) (f b)`.
* `sumLexCongr`, `prodLexCongr`: Creates a relation homomorphism between two `Sum.Lex` or two
`Prod.Lex` from relation homomorphisms between their arguments.

## Notation

* `→r`: `RelHom`
* `↪r`: `RelEmbedding`
* `≃r`: `RelIso`
-/

open Function

universe u v w

variable {α: Type ?u.42948α β: Type ?u.26798β γ: Type ?u.42954γ δ: Type ?u.11δ : Type _: Type (?u.26798+1)Type _} {r: α → α → Propr : α: Type ?u.631α → α: Type ?u.631α → Prop: TypeProp} {s: β → β → Props : β: Type ?u.634β → β: Type ?u.634β → Prop: TypeProp}
{t: γ → γ → Propt : γ: Type ?u.18178γ → γ: Type ?u.28608γ → Prop: TypeProp} {u: δ → δ → Propu : δ: Type ?u.11δ → δ: Type ?u.640δ → Prop: TypeProp}

/-- A relation homomorphism with respect to a given pair of relations `r` and `s`
is a function `f : α → β` such that `r a b → s (f a) (f b)`. -/
structure RelHom: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)RelHom {α: Type ?u.74α β: Type ?u.77β : Type _: Type (?u.77+1)Type _} (r: α → α → Propr : α: Type ?u.74α → α: Type ?u.74α → Prop: TypeProp) (s: β → β → Props : β: Type ?u.77β → β: Type ?u.77β → Prop: TypeProp) where
/-- The underlying function of a `RelHom` -/
toFun: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → RelHom r s → α → βtoFun : α: Type ?u.74α → β: Type ?u.77β
/-- A `RelHom` sends related elements to related elements -/
map_rel': ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (self : RelHom r s) {a b : α},
r a b → s (RelHom.toFun self a) (RelHom.toFun self b)map_rel' : ∀ {a: ?m.99a b: ?m.102b}, r: α → α → Propr a: ?m.99a b: ?m.102b → s: β → β → Props (toFun: α → βtoFun a: ?m.99a) (toFun: α → βtoFun b: ?m.102b)
#align rel_hom RelHom: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)RelHom

/-- A relation homomorphism with respect to a given pair of relations `r` and `s`
is a function `f : α → β` such that `r a b → s (f a) (f b)`. -/
infixl:25 " →r " => RelHom: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)RelHom

section

/-- `RelHomClass F r s` asserts that `F` is a type of functions such that all `f : F`
satisfy `r a b → s (f a) (f b)`.

The relations `r` and `s` are `outParam`s since figuring them out from a goal is a higher-order
matching problem that Lean usually can't do unaided.
-/
class RelHomClass: {F : Type u_1} →
{α : outParam (Type u_2)} →
{β : outParam (Type u_3)} →
{r : outParam (α → α → Prop)} →
{s : outParam (β → β → Prop)} →
[toFunLike : FunLike F α fun x => β] → (∀ (f : F) {a b : α}, r a b → s (↑f a) (↑f b)) → RelHomClass F r sRelHomClass (F: Type ?u.8666F : Type _: Type (?u.8666+1)Type _) {α: outParam (Type ?u.8670)α β: outParam (Type ?u.8674)β : outParam: Sort ?u.8669 → Sort ?u.8669outParam <| Type _: Type (?u.8670+1)Type _} (r: outParam (α → α → Prop)r : outParam: Sort ?u.8677 → Sort ?u.8677outParam <| α: outParam (Type ?u.8670)α → α: outParam (Type ?u.8670)α → Prop: TypeProp)
(s: outParam (β → β → Prop)s : outParam: Sort ?u.8688 → Sort ?u.8688outParam <| β: outParam (Type ?u.8674)β → β: outParam (Type ?u.8674)β → Prop: TypeProp) extends FunLike: Sort ?u.8703 →
(α : outParam (Sort ?u.8702)) → outParam (α → Sort ?u.8701) → Sort (max(max(max1?u.8703)?u.8702)?u.8701)FunLike F: Type ?u.8666F α: outParam (Type ?u.8670)α fun _: ?m.8705_ => β: outParam (Type ?u.8674)β where
/-- A `RelHomClass` sends related elements to related elements -/
map_rel: ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {r : outParam (α → α → Prop)}
{s : outParam (β → β → Prop)} [self : RelHomClass F r s] (f : F) {a b : α}, r a b → s (↑f a) (↑f b)map_rel : ∀ (f: Ff : F: Type ?u.8666F) {a: ?m.8716a b: ?m.8719b}, r: outParam (α → α → Prop)r a: ?m.8716a b: ?m.8719b → s: outParam (β → β → Prop)s (f: Ff a: ?m.8716a) (f: Ff b: ?m.8719b)
#align rel_hom_class RelHomClass: Type u_1 →
{α : outParam (Type u_2)} →
{β : outParam (Type u_3)} → outParam (α → α → Prop) → outParam (β → β → Prop) → Type (max(maxu_1u_2)u_3)RelHomClass

export RelHomClass (map_rel)

end

namespace RelHomClass

variable {F: Type ?u.9277F : Type _: Type (?u.9277+1)Type _}

protected theorem isIrrefl: ∀ [inst : RelHomClass F r s], F → ∀ [inst : IsIrrefl β s], IsIrrefl α risIrrefl [RelHomClass: Type ?u.9000 →
{α : outParam (Type ?u.8999)} →
{β : outParam (Type ?u.8998)} →
outParam (α → α → Prop) → outParam (β → β → Prop) → Type (max(max?u.9000?u.8999)?u.8998)RelHomClass F: Type ?u.8995F r: α → α → Propr s: β → β → Props] (f: Ff : F: Type ?u.8995F) : ∀ [IsIrrefl: (α : Type ?u.9020) → (α → α → Prop) → PropIsIrrefl β: Type ?u.8962β s: β → β → Props], IsIrrefl: (α : Type ?u.9025) → (α → α → Prop) → PropIsIrrefl α: Type ?u.8959α r: α → α → Propr
| ⟨H: ∀ (a : β), ¬s a aH⟩ => ⟨fun _: ?m.9077_ h: ?m.9080h => H: ∀ (a : β), ¬s a aH _: β_ (map_rel: ∀ {F : Type ?u.9085} {α : outParam (Type ?u.9084)} {β : outParam (Type ?u.9083)} {r : outParam (α → α → Prop)}
{s : outParam (β → β → Prop)} [self : RelHomClass F r s] (f : F) {a b : α}, r a b → s (↑f a) (↑f b)map_rel f: Ff h: ?m.9080h)⟩
#align rel_hom_class.is_irrefl RelHomClass.isIrrefl: ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s],
F → ∀ [inst : IsIrrefl β s], IsIrrefl α rRelHomClass.isIrrefl

protected theorem isAsymm: ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s],
F → ∀ [inst : IsAsymm β s], IsAsymm α risAsymm [RelHomClass: Type ?u.9282 →
{α : outParam (Type ?u.9281)} →
{β : outParam (Type ?u.9280)} →
outParam (α → α → Prop) → outParam (β → β → Prop) → Type (max(max?u.9282?u.9281)?u.9280)RelHomClass F: Type ?u.9277F r: α → α → Propr s: β → β → Props] (f: Ff : F: Type ?u.9277F) : ∀ [IsAsymm: (α : Type ?u.9302) → (α → α → Prop) → PropIsAsymm β: Type ?u.9244β s: β → β → Props], IsAsymm: (α : Type ?u.9307) → (α → α → Prop) → PropIsAsymm α: Type ?u.9241α r: α → α → Propr
| ⟨H: ∀ (a b : β), s a b → ¬s b aH⟩ => ⟨fun _: ?m.9375_ _: ?m.9378_ h₁: ?m.9381h₁ h₂: ?m.9384h₂ => H: ∀ (a b : β), s a b → ¬s b aH _: β_ _: β_ (map_rel: ∀ {F : Type ?u.9390} {α : outParam (Type ?u.9389)} {β : outParam (Type ?u.9388)} {r : outParam (α → α → Prop)}
{s : outParam (β → β → Prop)} [self : RelHomClass F r s] (f : F) {a b : α}, r a b → s (↑f a) (↑f b)map_rel f: Ff h₁: ?m.9381h₁) (map_rel: ∀ {F : Type ?u.9449} {α : outParam (Type ?u.9448)} {β : outParam (Type ?u.9447)} {r : outParam (α → α → Prop)}
{s : outParam (β → β → Prop)} [self : RelHomClass F r s] (f : F) {a b : α}, r a b → s (↑f a) (↑f b)map_rel f: Ff h₂: ?m.9384h₂)⟩
#align rel_hom_class.is_asymm RelHomClass.isAsymm: ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s],
F → ∀ [inst : IsAsymm β s], IsAsymm α rRelHomClass.isAsymm

protected theorem acc: ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s] (f : F)
(a : α), Acc s (↑f a) → Acc r aacc [RelHomClass: Type ?u.9667 →
{α : outParam (Type ?u.9666)} →
{β : outParam (Type ?u.9665)} →
outParam (α → α → Prop) → outParam (β → β → Prop) → Type (max(max?u.9667?u.9666)?u.9665)RelHomClass F: Type ?u.9662F r: α → α → Propr s: β → β → Props] (f: Ff : F: Type ?u.9662F) (a: αa : α: Type ?u.9626α) : Acc: {α : Sort ?u.9689} → (α → α → Prop) → α → PropAcc s: β → β → Props (f: Ff a: αa) → Acc: {α : Sort ?u.9814} → (α → α → Prop) → α → PropAcc r: α → α → Propr a: αa := byGoals accomplished! 🐙
α: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa: αAcc s (↑f a) → Acc r ageneralize h : f: Ff a: αa = bα: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa: αb: βh: ↑f a = bAcc s b → Acc r a
α: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa: αAcc s (↑f a) → Acc r aintro ac: Acc s bacα: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa: αb: βh: ↑f a = bac: Acc s bAcc r a
α: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa: αAcc s (↑f a) → Acc r ainduction' ac: Acc s bac with _ H: ∀ (y : ?m.9970), ?m.9971 y x✝ → Acc ?m.9971 yH IH: ∀ (y : ?m.9970) (a : ?m.9971 y x✝), ?m.9972 y (_ : Acc ?m.9971 y)IH generalizing a: αaα: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa✝: αb: βh✝: ↑f a✝ = bx✝: βH: ∀ (y : β), s y x✝ → Acc s yIH: ∀ (y : β), s y x✝ → ∀ (a : α), ↑f a = y → Acc r aa: αh: ↑f a = x✝introAcc r a
α: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa: αAcc s (↑f a) → Acc r asubst h: ↑f a = x✝hα: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa✝: αb: βh: ↑f a✝ = ba: αH: ∀ (y : β), s y (↑f a) → Acc s yIH: ∀ (y : β), s y (↑f a) → ∀ (a : α), ↑f a = y → Acc r aintroAcc r a
α: Type u_2β: Type u_3γ: Type ?u.9632δ: Type ?u.9635r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → PropF: Type u_1inst✝: RelHomClass F r sf: Fa: αAcc s (↑f a) → Acc r aexact ⟨_: ?m.10023_, fun a': ?m.10034a' h: ?m.10037h => IH: ∀ (y : β), s y (↑f a) → ∀ (a : α), ↑f a = y → Acc r aIH (f: Ff a': ?m.10034a') (map_rel: ∀ {F : Type ?u.10127} {α : outParam (Type ?u.10126)} {β : outParam (Type ?u.10125)} {r : outParam (α → α → Prop)}
{s : outParam (β → β → Prop)} [self : RelHomClass F r s] (f : F) {a b : α}, r a b → s (↑f a) (↑f b)map_rel f: Ff h: ?m.10037h) _: α_ rfl: ∀ {α : Sort ?u.10178} {a : α}, a = arfl⟩Goals accomplished! 🐙
#align rel_hom_class.acc RelHomClass.acc: ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s] (f : F)
(a : α), Acc s (↑f a) → Acc r aRelHomClass.acc

protected theorem wellFounded: ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s],
F → WellFounded s → WellFounded rwellFounded [RelHomClass: Type ?u.10279 →
{α : outParam (Type ?u.10278)} →
{β : outParam (Type ?u.10277)} →
outParam (α → α → Prop) → outParam (β → β → Prop) → Type (max(max?u.10279?u.10278)?u.10277)RelHomClass F: Type ?u.10274F r: α → α → Propr s: β → β → Props] (f: Ff : F: Type ?u.10274F) : ∀ _: WellFounded s_ : WellFounded: {α : Sort ?u.10299} → (α → α → Prop) → PropWellFounded s: β → β → Props, WellFounded: {α : Sort ?u.10309} → (α → α → Prop) → PropWellFounded r: α → α → Propr
| ⟨H: ∀ (a : β), Acc s aH⟩ => ⟨fun _: ?m.10365_ => RelHomClass.acc: ∀ {α : Type ?u.10368} {β : Type ?u.10369} {r : α → α → Prop} {s : β → β → Prop} {F : Type ?u.10367}
[inst : RelHomClass F r s] (f : F) (a : α), Acc s (↑f a) → Acc r aRelHomClass.acc f: Ff _: ?m.10370_ (H: ∀ (a : β), Acc s aH _: β_)⟩
#align rel_hom_class.well_founded RelHomClass.wellFounded: ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_1} [inst : RelHomClass F r s],
F → WellFounded s → WellFounded rRelHomClass.wellFounded

end RelHomClass

namespace RelHom

instance: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → RelHomClass (r →r s) r sinstance : RelHomClass: Type ?u.10546 →
{α : outParam (Type ?u.10545)} →
{β : outParam (Type ?u.10544)} →
outParam (α → α → Prop) → outParam (β → β → Prop) → Type (max(max?u.10546?u.10545)?u.10544)RelHomClass (r: α → α → Propr →r s: β → β → Props) r: α → α → Propr s: β → β → Props where
coe o: ?m.10613o := o: ?m.10613o.toFun: {α : Type ?u.10616} → {β : Type ?u.10615} → {r : α → α → Prop} → {s : β → β → Prop} → r →r s → α → βtoFun
coe_injective' f: ?m.10640f g: ?m.10643g h: ?m.10646h := byGoals accomplished! 🐙
α: Type ?u.10508β: Type ?u.10511γ: Type ?u.10514δ: Type ?u.10517r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf, g: r →r sh: (fun o => o.toFun) f = (fun o => o.toFun) gf = gcases f: r →r sfα: Type ?u.10508β: Type ?u.10511γ: Type ?u.10514δ: Type ?u.10517r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propg: r →r stoFun✝: α → βmap_rel'✝: ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)h: (fun o => o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ } = (fun o => o.toFun) gmk{ toFun := toFun✝, map_rel' := map_rel'✝ } = g
α: Type ?u.10508β: Type ?u.10511γ: Type ?u.10514δ: Type ?u.10517r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf, g: r →r sh: (fun o => o.toFun) f = (fun o => o.toFun) gf = gcases g: r →r sgα: Type ?u.10508β: Type ?u.10511γ: Type ?u.10514δ: Type ?u.10517r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → ProptoFun✝¹: α → βmap_rel'✝¹: ∀ {a b : α}, r a b → s (toFun✝¹ a) (toFun✝¹ b)toFun✝: α → βmap_rel'✝: ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)h: (fun o => o.toFun) { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } =   (fun o => o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ }mk.mk{ toFun := toFun✝¹, map_rel' := map_rel'✝¹ } = { toFun := toFun✝, map_rel' := map_rel'✝ }
α: Type ?u.10508β: Type ?u.10511γ: Type ?u.10514δ: Type ?u.10517r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf, g: r →r sh: (fun o => o.toFun) f = (fun o => o.toFun) gf = gcongrGoals accomplished! 🐙
map_rel := map_rel': ∀ {α : Type ?u.10659} {β : Type ?u.10658} {r : α → α → Prop} {s : β → β → Prop} (self : r →r s) {a b : α},
r a b → s (toFun self a) (toFun self b)map_rel'

initialize_simps_projections RelHom: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)RelHom (toFun: {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → r →r s → α → βtoFun → apply: {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → r →r s → α → βapply)

protected theorem map_rel: ∀ (f : r →r s) {a b : α}, r a b → s (↑f a) (↑f b)map_rel (f: r →r sf : r: α → α → Propr →r s: β → β → Props) {a: αa b: ?m.11582b} : r: α → α → Propr a: ?m.11579a b: ?m.11582b → s: β → β → Props (f: r →r sf a: ?m.11579a) (f: r →r sf b: ?m.11582b) :=
f: r →r sf.map_rel': ∀ {α : Type ?u.11839} {β : Type ?u.11838} {r : α → α → Prop} {s : β → β → Prop} (self : r →r s) {a b : α},
r a b → s (toFun self a) (toFun self b)map_rel'
#align rel_hom.map_rel RelHom.map_rel: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) {a b : α}, r a b → s (↑f a) (↑f b)RelHom.map_rel

@[simp]
theorem coe_fn_toFun: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s), f.toFun = ↑fcoe_fn_toFun (f: r →r sf : r: α → α → Propr →r s: β → β → Props) : f: r →r sf.toFun: {α : Type ?u.11933} → {β : Type ?u.11932} → {r : α → α → Prop} → {s : β → β → Prop} → r →r s → α → βtoFun = (f: r →r sf : α: Type ?u.11877α → β: Type ?u.11880β) :=
rfl: ∀ {α : Sort ?u.12102} {a : α}, a = arfl
#align rel_hom.coe_fn_to_fun RelHom.coe_fn_toFun: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s), f.toFun = ↑fRelHom.coe_fn_toFun

/-- The map `coe_fn : (r →r s) → (α → β)` is injective. -/
theorem coe_fn_injective: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Injective fun f => ↑fcoe_fn_injective : Injective: {α : Sort ?u.12167} → {β : Sort ?u.12166} → (α → β) → PropInjective fun (f: r →r sf : r: α → α → Propr →r s: β → β → Props) => (f: r →r sf : α: Type ?u.12130α → β: Type ?u.12133β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.12345} {α : Sort ?u.12346} {β : α → Sort ?u.12347} [i : FunLike F α β], Injective fun f => ↑fFunLike.coe_injective
#align rel_hom.coe_fn_injective RelHom.coe_fn_injective: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Injective fun f => ↑fRelHom.coe_fn_injective

@[ext]
theorem ext: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r →r s⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext ⦃f: r →r sf g: r →r sg : r: α → α → Propr →r s: β → β → Props⦄ (h: ∀ (x : α), ↑f x = ↑g xh : ∀ x: ?m.12561x, f: r →r sf x: ?m.12561x = g: r →r sg x: ?m.12561x) : f: r →r sf = g: r →r sg :=
FunLike.ext: ∀ {F : Sort ?u.12823} {α : Sort ?u.12824} {β : α → Sort ?u.12822} [i : FunLike F α β] (f g : F),
(∀ (x : α), ↑f x = ↑g x) → f = gFunLike.ext f: r →r sf g: r →r sg h: ∀ (x : α), ↑f x = ↑g xh
#align rel_hom.ext RelHom.ext: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r →r s⦄, (∀ (x : α), ↑f x = ↑g x) → f = gRelHom.ext

theorem ext_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r →r s}, f = g ↔ ∀ (x : α), ↑f x = ↑g xext_iff {f: r →r sf g: r →r sg : r: α → α → Propr →r s: β → β → Props} : f: r →r sf = g: r →r sg ↔ ∀ x: ?m.13061x, f: r →r sf x: ?m.13061x = g: r →r sg x: ?m.13061x :=
FunLike.ext_iff: ∀ {F : Sort ?u.13310} {α : Sort ?u.13312} {β : α → Sort ?u.13311} [i : FunLike F α β] {f g : F},
f = g ↔ ∀ (x : α), ↑f x = ↑g xFunLike.ext_iff
#align rel_hom.ext_iff RelHom.ext_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r →r s}, f = g ↔ ∀ (x : α), ↑f x = ↑g xRelHom.ext_iff

/-- Identity map is a relation homomorphism. -/
@[refl, simps: ∀ {α : Type u_1} (r : α → α → Prop) (x : α), ↑(RelHom.id r) x = xsimps]
protected def id: {α : Type u_1} → (r : α → α → Prop) → r →r rid (r: α → α → Propr : α: Type ?u.13460α → α: Type ?u.13460α → Prop: TypeProp) : r: α → α → Propr →r r: α → α → Propr :=
⟨fun x: ?m.13545x => x: ?m.13545x, fun x: ?m.13552x => x: ?m.13552x⟩
#align rel_hom.id RelHom.id: {α : Type u_1} → (r : α → α → Prop) → r →r rRelHom.id
#align rel_hom.id_apply RelHom.id_apply: ∀ {α : Type u_1} (r : α → α → Prop) (x : α), ↑(RelHom.id r) x = xRelHom.id_apply

/-- Composition of two relation homomorphisms is a relation homomorphism. -/
@[simps: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (g : s →r t)
(f : r →r s) (x : α), ↑(RelHom.comp g f) x = ↑g (↑f x)simps]
protected def comp: s →r t → r →r s → r →r tcomp (g: s →r tg : s: β → β → Props →r t: γ → γ → Propt) (f: r →r sf : r: α → α → Propr →r s: β → β → Props) : r: α → α → Propr →r t: γ → γ → Propt :=
⟨fun x: ?m.13794x => g: s →r tg (f: r →r sf x: ?m.13794x), fun h: ?m.14079h => g: s →r tg.2: ∀ {α : Type ?u.14082} {β : Type ?u.14081} {r : α → α → Prop} {s : β → β → Prop} (self : r →r s) {a b : α},
r a b → s (toFun self a) (toFun self b)2 (f: r →r sf.2: ∀ {α : Type ?u.14116} {β : Type ?u.14115} {r : α → α → Prop} {s : β → β → Prop} (self : r →r s) {a b : α},
r a b → s (toFun self a) (toFun self b)2 h: ?m.14079h)⟩
#align rel_hom.comp RelHom.comp: {α : Type u_1} →
{β : Type u_2} →
{γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → s →r t → r →r s → r →r tRelHom.comp
#align rel_hom.comp_apply RelHom.comp_apply: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (g : s →r t)
(f : r →r s) (x : α), ↑(RelHom.comp g f) x = ↑g (↑f x)RelHom.comp_apply

/-- A relation homomorphism is also a relation homomorphism between dual relations. -/
protected def swap: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r →r s → swap r →r swap sswap (f: r →r sf : r: α → α → Propr →r s: β → β → Props) : swap: {α : Sort ?u.14528} →
{β : Sort ?u.14527} → {φ : α → β → Sort ?u.14526} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x yswap r: α → α → Propr →r swap: {α : Sort ?u.14554} →
{β : Sort ?u.14553} → {φ : α → β → Sort ?u.14552} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x yswap s: β → β → Props :=
⟨f: r →r sf, f: r →r sf.map_rel: ∀ {α : Type ?u.14747} {β : Type ?u.14748} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) {a b : α},
r a b → s (↑f a) (↑f b)map_rel⟩
#align rel_hom.swap RelHom.swap: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r →r s → swap r →r swap sRelHom.swap

/-- A function is a relation homomorphism from the preimage relation of `s` to `s`. -/
def preimage: (f : α → β) → (s : β → β → Prop) → f ⁻¹'o s →r spreimage (f: α → βf : α: Type ?u.14948α → β: Type ?u.14951β) (s: β → β → Props : β: Type ?u.14951β → β: Type ?u.14951β → Prop: TypeProp) : f: α → βf ⁻¹'o s: β → β → Props →r s: β → β → Props :=
⟨f: α → βf, id: ∀ {α : Sort ?u.15059}, α → αid⟩
#align rel_hom.preimage RelHom.preimage: {α : Type u_1} → {β : Type u_2} → (f : α → β) → (s : β → β → Prop) → f ⁻¹'o s →r sRelHom.preimage

end RelHom

/-- An increasing function is injective -/
theorem injective_of_increasing: ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsTrichotomous α r] [inst : IsIrrefl β s]
(f : α → β), (∀ {x y : α}, r x y → s (f x) (f y)) → Injective finjective_of_increasing (r: α → α → Propr : α: Type ?u.15156α → α: Type ?u.15156α → Prop: TypeProp) (s: β → β → Props : β: Type ?u.15159β → β: Type ?u.15159β → Prop: TypeProp) [IsTrichotomous: (α : Type ?u.15204) → (α → α → Prop) → PropIsTrichotomous α: Type ?u.15156α r: α → α → Propr]
[IsIrrefl: (α : Type ?u.15209) → (α → α → Prop) → PropIsIrrefl β: Type ?u.15159β s: β → β → Props] (f: α → βf : α: Type ?u.15156α → β: Type ?u.15159β) (hf: ∀ {x y : α}, r x y → s (f x) (f y)hf : ∀ {x: ?m.15219x y: ?m.15222y}, r: α → α → Propr x: ?m.15219x y: ?m.15222y → s: β → β → Props (f: α → βf x: ?m.15219x) (f: α → βf y: ?m.15222y)) : Injective: {α : Sort ?u.15230} → {β : Sort ?u.15229} → (α → β) → PropInjective f: α → βf := byGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)Injective fintro x: αx y: αy hxy: f x = f yhxyα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yx = y
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)Injective frcases trichotomous_of: ∀ {α : Type ?u.15260} (r : α → α → Prop) [inst : IsTrichotomous α r] (a b : α), r a b ∨ a = b ∨ r b atrichotomous_of r: α → α → Propr x: αx y: αy with (h | h | h): r x y ∨ x = y ∨ r y x(h: r x yhh | h | h: r x y ∨ x = y ∨ r y x | h: x = yhh | h | h: r x y ∨ x = y ∨ r y x | h: r y xh(h | h | h): r x y ∨ x = y ∨ r y x)α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x yinlx = yα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: x = yinr.inlx = yα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xinr.inrx = y
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)Injective f·α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x yinlx = y α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x yinlx = yα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: x = yinr.inlx = yα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xinr.inrx = yhave := hf: ∀ {x y : α}, r x y → s (f x) (f y)hf h: r x yhα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x ythis: s (f x) (f y)inlx = y
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x yinlx = yrw [α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x ythis: s (f x) (f y)inlx = yhxy: f x = f yhxyα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x ythis: s (f y) (f y)inlx = y]α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x ythis: s (f y) (f y)inlx = y at this: ?m.15335thisα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x ythis: s (f y) (f y)inlx = y
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x yinlx = yexfalsoα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x ythis: s (f y) (f y)inl.hFalse
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r x yinlx = yexact irrefl_of: ∀ {α : Type ?u.15379} (r : α → α → Prop) [inst : IsIrrefl α r] (a : α), ¬r a airrefl_of s: β → β → Props (f: α → βf y: αy) this: s (f y) (f y)thisGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)Injective f·α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: x = yinr.inlx = y α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: x = yinr.inlx = yα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xinr.inrx = yexact h: x = yhGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)Injective f·α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xinr.inrx = y α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xinr.inrx = yhave := hf: ∀ {x y : α}, r x y → s (f x) (f y)hf h: r y xhα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xthis: s (f y) (f x)inr.inrx = y
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xinr.inrx = yrw [α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xthis: s (f y) (f x)inr.inrx = yhxy: f x = f yhxyα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xthis: s (f y) (f y)inr.inrx = y]α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xthis: s (f y) (f y)inr.inrx = y at this: ?m.15398thisα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xthis: s (f y) (f y)inr.inrx = y
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xinr.inrx = yexfalsoα: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xthis: s (f y) (f y)inr.inr.hFalse
α: Type u_1β: Type u_2γ: Type ?u.15162δ: Type ?u.15165r✝: α → α → Props✝: β → β → Propt: γ → γ → Propu: δ → δ → Propr: α → α → Props: β → β → Propinst✝¹: IsTrichotomous α rinst✝: IsIrrefl β sf: α → βhf: ∀ {x y : α}, r x y → s (f x) (f y)x, y: αhxy: f x = f yh: r y xinr.inrx = yexact irrefl_of: ∀ {α : Type ?u.15437} (r : α → α → Prop) [inst : IsIrrefl α r] (a : α), ¬r a airrefl_of s: β → β → Props (f: α → βf y: αy) this: s (f y) (f y)thisGoals accomplished! 🐙
#align injective_of_increasing injective_of_increasing: ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [inst : IsTrichotomous α r] [inst : IsIrrefl β s]
(f : α → β), (∀ {x y : α}, r x y → s (f x) (f y)) → Injective finjective_of_increasing

/-- An increasing function is injective -/
theorem RelHom.injective_of_increasing: ∀ [inst : IsTrichotomous α r] [inst : IsIrrefl β s] (f : r →r s), Injective ↑fRelHom.injective_of_increasing [IsTrichotomous: (α : Type ?u.15512) → (α → α → Prop) → PropIsTrichotomous α: Type ?u.15476α r: α → α → Propr] [IsIrrefl: (α : Type ?u.15517) → (α → α → Prop) → PropIsIrrefl β: Type ?u.15479β s: β → β → Props] (f: r →r sf : r: α → α → Propr →r s: β → β → Props) :
Injective: {α : Sort ?u.15541} → {β : Sort ?u.15540} → (α → β) → PropInjective f: r →r sf :=
_root_.injective_of_increasing: ∀ {α : Type ?u.15700} {β : Type ?u.15701} (r : α → α → Prop) (s : β → β → Prop) [inst : IsTrichotomous α r]
[inst : IsIrrefl β s] (f : α → β), (∀ {x y : α}, r x y → s (f x) (f y)) → Injective f_root_.injective_of_increasing r: α → α → Propr s: β → β → Props f: r →r sf f: r →r sf.map_rel: ∀ {α : Type ?u.15886} {β : Type ?u.15887} {r : α → α → Prop} {s : β → β → Prop} (f : r →r s) {a b : α},
r a b → s (↑f a) (↑f b)map_rel
#align rel_hom.injective_of_increasing RelHom.injective_of_increasing: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrichotomous α r] [inst : IsIrrefl β s]
(f : r →r s), Injective ↑fRelHom.injective_of_increasing

-- TODO: define a `RelIffClass` so we don't have to do all the `convert` trickery?
theorem Surjective.wellFounded_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : α → β},
Surjective f → (∀ {a b : α}, r a b ↔ s (f a) (f b)) → (WellFounded r ↔ WellFounded s)Surjective.wellFounded_iff {f: α → βf : α: Type ?u.15942α → β: Type ?u.15945β} (hf: Surjective fhf : Surjective: {α : Sort ?u.15983} → {β : Sort ?u.15982} → (α → β) → PropSurjective f: α → βf)
(o: ∀ {a b : α}, r a b ↔ s (f a) (f b)o : ∀ {a: ?m.15993a b: ?m.15996b}, r: α → α → Propr a: ?m.15993a b: ?m.15996b ↔ s: β → β → Props (f: α → βf a: ?m.15993a) (f: α → βf b: ?m.15996b)) :
WellFounded: {α : Sort ?u.16001} → (α → α → Prop) → PropWellFounded r: α → α → Propr ↔ WellFounded: {α : Sort ?u.16009} → (α → α → Prop) → PropWellFounded s: β → β → Props :=
Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)Iff.intro
(byGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)WellFounded r → WellFounded srefine RelHomClass.wellFounded: ∀ {α : Type ?u.16188} {β : Type ?u.16189} {r : α → α → Prop} {s : β → β → Prop} {F : Type ?u.16187}
[inst : RelHomClass F r s], F → WellFounded s → WellFounded rRelHomClass.wellFounded (RelHom.mk: {α : Type ?u.16244} →
{β : Type ?u.16243} →
{r : α → α → Prop} → {s : β → β → Prop} → (toFun : α → β) → (∀ {a b : α}, r a b → s (toFun a) (toFun b)) → r →r sRelHom.mk ?_: ?m.16245 → ?m.16246?_ ?_: ∀ {a b : ?m.16245}, ?m.16247 a b → ?m.16248 (?refine_1 a) (?refine_1 b)?_ : s: β → β → Props →r r: α → α → Propr)α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)refine_1β → αα: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)refine_2∀ {a b : β}, s a b → r (?refine_1 a) (?refine_1 b)
α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)WellFounded r → WellFounded s·α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)refine_1β → α α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)refine_1β → αα: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)refine_2∀ {a b : β}, s a b → r (?refine_1 a) (?refine_1 b)exact Classical.choose: {α : Sort ?u.16314} → {p : α → Prop} → (∃ x, p x) → αClassical.choose hf: Surjective fhf.hasRightInverse: ∀ {α : Sort ?u.16319} {β : Sort ?u.16318} {f : α → β}, Surjective f → HasRightInverse fhasRightInverseGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)WellFounded r → WellFounded sintro a: ?m.16245a b: ?m.16245b h: ?m.16247 a bhα: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)a, b: βh: s a brefine_2r (Classical.choose (_ : HasRightInverse f) a) (Classical.choose (_ : HasRightInverse f) b)
α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)WellFounded r → WellFounded sapply o: ∀ {a b : α}, r a b ↔ s (f a) (f b)o.2: ∀ {a b : Prop}, (a ↔ b) → b → a2α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)a, b: βh: s a brefine_2s (f (Classical.choose (_ : HasRightInverse f) a)) (f (Classical.choose (_ : HasRightInverse f) b))
α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)WellFounded r → WellFounded sconvert h: ?m.16247 a bhα: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)a, b: βh: s a bh.e'_1f (Classical.choose (_ : HasRightInverse f) a) = aα: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)a, b: βh: s a bh.e'_2f (Classical.choose (_ : HasRightInverse f) b) = b
α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)WellFounded r → WellFounded siterate 2 α: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)a, b: βh: s a bh.e'_1f (Classical.choose (_ : HasRightInverse f) a) = aα: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)a, b: βh: s a bh.e'_2f (Classical.choose (_ : HasRightInverse f) b) = bapply Classical.choose_spec: ∀ {α : Sort ?u.17185} {p : α → Prop} (h : ∃ x, p x), p (Classical.choose h)Classical.choose_spec hf: Surjective fhf.hasRightInverse: ∀ {α : Sort ?u.17220} {β : Sort ?u.17219} {f : α → β}, Surjective f → HasRightInverse fhasRightInverseα: Type u_1β: Type u_2γ: Type ?u.15948δ: Type ?u.15951r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: α → βhf: Surjective fo: ∀ {a b : α}, r a b ↔ s (f a) (f b)a, b: βh: s a bh.e'_2f (Classical.choose (_ : HasRightInverse f) b) = b)
(RelHomClass.wellFounded: ∀ {α : Type ?u.16028} {β : Type ?u.16029} {r : α → α → Prop} {s : β → β → Prop} {F : Type ?u.16027}
[inst : RelHomClass F r s], F → WellFounded s → WellFounded rRelHomClass.wellFounded (⟨f: α → βf, o: ∀ {a b : α}, r a b ↔ s (f a) (f b)o.1: ∀ {a b : Prop}, (a ↔ b) → a → b1⟩ : r: α → α → Propr →r s: β → β → Props))
#align surjective.well_founded_iff Surjective.wellFounded_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : α → β},
Surjective f → (∀ {a b : α}, r a b ↔ s (f a) (f b)) → (WellFounded r ↔ WellFounded s)Surjective.wellFounded_iff

/-- A relation embedding with respect to a given pair of relations `r` and `s`
is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`. -/
structure RelEmbedding: {α : Type u_1} →
{β : Type u_2} →
{r : α → α → Prop} →
{s : β → β → Prop} →
(toEmbedding : α ↪ β) → (∀ {a b : α}, s (↑toEmbedding a) (↑toEmbedding b) ↔ r a b) → RelEmbedding r sRelEmbedding {α: Type ?u.17327α β: Type ?u.17330β : Type _: Type (?u.17327+1)Type _} (r: α → α → Propr : α: Type ?u.17327α → α: Type ?u.17327α → Prop: TypeProp) (s: β → β → Props : β: Type ?u.17330β → β: Type ?u.17330β → Prop: TypeProp) extends α: Type ?u.17327α ↪ β: Type ?u.17330β where
/-- Elements are related iff they are related after apply a `RelEmbedding` -/
map_rel_iff': ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (self : RelEmbedding r s) {a b : α},
s (↑self.toEmbedding a) (↑self.toEmbedding b) ↔ r a bmap_rel_iff' : ∀ {a: ?m.17354a b: ?m.17357b}, s: β → β → Props (toEmbedding: α ↪ βtoEmbedding a: ?m.17354a) (toEmbedding: α ↪ βtoEmbedding b: ?m.17357b) ↔ r: α → α → Propr a: ?m.17354a b: ?m.17357b
#align rel_embedding RelEmbedding: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)RelEmbedding

/-- A relation embedding with respect to a given pair of relations `r` and `s`
is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`. -/
infixl:25 " ↪r " => RelEmbedding: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)RelEmbedding

/-- The induced relation on a subtype is an embedding under the natural inclusion. -/
def Subtype.relEmbedding: {X : Type ?u.26060} → (r : X → X → Prop) → (p : X → Prop) → val ⁻¹'o r ↪r rSubtype.relEmbedding {X: Type ?u.26060X : Type _: Type (?u.26060+1)Type _} (r: X → X → Propr : X: Type ?u.26060X → X: Type ?u.26060X → Prop: TypeProp) (p: X → Propp : X: Type ?u.26060X → Prop: TypeProp) :
(Subtype.val: {α : Sort ?u.26093} → {p : α → Prop} → Subtype p → αSubtype.val : Subtype: {α : Sort ?u.26087} → (α → Prop) → Sort (max1?u.26087)Subtype p: X → Propp → X: Type ?u.26060X) ⁻¹'o r: X → X → Propr ↪r r: X → X → Propr :=
⟨Embedding.subtype: {α : Sort ?u.26150} → (p : α → Prop) → Subtype p ↪ αEmbedding.subtype p: X → Propp, Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl⟩
#align subtype.rel_embedding Subtype.relEmbedding: {X : Type u_1} → (r : X → X → Prop) → (p : X → Prop) → Subtype.val ⁻¹'o r ↪r rSubtype.relEmbedding

theorem preimage_equivalence: ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) {s : β → β → Prop}, Equivalence s → Equivalence (f ⁻¹'o s)preimage_equivalence {α: ?m.26329α β: Sort u_2β} (f: α → βf : α: ?m.26329α → β: ?m.26332β) {s: β → β → Props : β: ?m.26332β → β: ?m.26332β → Prop: TypeProp} (hs: Equivalence shs : Equivalence: {α : Sort ?u.26345} → (α → α → Prop) → PropEquivalence s: β → β → Props) :
Equivalence: {α : Sort ?u.26355} → (α → α → Prop) → PropEquivalence (f: α → βf ⁻¹'o s: β → β → Props) :=
⟨fun _: ?m.26401_ => hs: Equivalence shs.1: ∀ {α : Sort ?u.26403} {r : α → α → Prop}, Equivalence r → ∀ (x : α), r x x1 _: ?m.26404_, fun h: ?m.26420h => hs: Equivalence shs.2: ∀ {α : Sort ?u.26422} {r : α → α → Prop}, Equivalence r → ∀ {x y : α}, r x y → r y x2 h: ?m.26420h, fun h₁: ?m.26441h₁ h₂: ?m.26444h₂ => hs: Equivalence shs.3: ∀ {α : Sort ?u.26446} {r : α → α → Prop}, Equivalence r → ∀ {x y z : α}, r x y → r y z → r x z3 h₁: ?m.26441h₁ h₂: ?m.26444h₂⟩
#align preimage_equivalence preimage_equivalence: ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) {s : β → β → Prop}, Equivalence s → Equivalence (f ⁻¹'o s)preimage_equivalence

namespace RelEmbedding

/-- A relation embedding is also a relation homomorphism -/
def toRelHom: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → r →r stoRelHom (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) : r: α → α → Propr →r s: β → β → Props where
toFun := f: r ↪r sf.toEmbedding: {α : Type ?u.26577} → {β : Type ?u.26576} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → α ↪ βtoEmbedding.toFun: {α : Sort ?u.26595} → {β : Sort ?u.26594} → (α ↪ β) → α → βtoFun
map_rel' := (map_rel_iff': ∀ {α : Type ?u.26606} {β : Type ?u.26605} {r : α → α → Prop} {s : β → β → Prop} (self : r ↪r s) {a b : α},
s (↑self.toEmbedding a) (↑self.toEmbedding b) ↔ r a bmap_rel_iff' f: r ↪r sf).mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr
#align rel_embedding.to_rel_hom RelEmbedding.toRelHom: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → r →r sRelEmbedding.toRelHom

instance: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → Coe (r ↪r s) (r →r s)instance : Coe: semiOutParam (Sort ?u.26832) → Sort ?u.26831 → Sort (max(max1?u.26832)?u.26831)Coe (r: α → α → Propr ↪r s: β → β → Props) (r: α → α → Propr →r s: β → β → Props) :=
⟨toRelHom: {α : Type ?u.26876} → {β : Type ?u.26875} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → r →r stoRelHom⟩

--Porting note: removed
-- see Note [function coercion]
-- instance : CoeFun (r ↪r s) fun _ => α → β :=
--   ⟨fun o => o.toEmbedding⟩

-- TODO: define and instantiate a `RelEmbeddingClass` when `EmbeddingLike` is defined
instance: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → RelHomClass (r ↪r s) r sinstance : RelHomClass: Type ?u.27108 →
{α : outParam (Type ?u.27107)} →
{β : outParam (Type ?u.27106)} →
outParam (α → α → Prop) → outParam (β → β → Prop) → Type (max(max?u.27108?u.27107)?u.27106)RelHomClass (r: α → α → Propr ↪r s: β → β → Props) r: α → α → Propr s: β → β → Props where
coe := fun x: ?m.27175x => x: ?m.27175x.toFun: {α : Sort ?u.27196} → {β : Sort ?u.27195} → (α ↪ β) → α → βtoFun
coe_injective' f: ?m.27208f g: ?m.27211g h: ?m.27214h := byGoals accomplished! 🐙
α: Type ?u.27070β: Type ?u.27073γ: Type ?u.27076δ: Type ?u.27079r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf, g: r ↪r sh: (fun x => x.toFun) f = (fun x => x.toFun) gf = grcases f: r ↪r sf with ⟨⟨⟩⟩: r ↪r s⟨⟨⟩: α ↪ β⟨⟩⟨⟨⟩⟩: r ↪r s⟩α: Type ?u.27070β: Type ?u.27073γ: Type ?u.27076δ: Type ?u.27079r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propg: r ↪r stoFun✝: α → βinj'✝: Injective toFun✝map_rel_iff'✝: ∀ {a b : α}, s (↑{ toFun := toFun✝, inj' := inj'✝ } a) (↑{ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a bh: (fun x => x.toFun) { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ } =   (fun x => x.toFun) gmk.mk{ toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ } = g
α: Type ?u.27070β: Type ?u.27073γ: Type ?u.27076δ: Type ?u.27079r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf, g: r ↪r sh: (fun x => x.toFun) f = (fun x => x.toFun) gf = grcases g: r ↪r sg with ⟨⟨⟩⟩: r ↪r s⟨⟨⟩: α ↪ β⟨⟩⟨⟨⟩⟩: r ↪r s⟩α: Type ?u.27070β: Type ?u.27073γ: Type ?u.27076δ: Type ?u.27079r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → ProptoFun✝¹: α → βinj'✝¹: Injective toFun✝¹map_rel_iff'✝¹: ∀ {a b : α}, s (↑{ toFun := toFun✝¹, inj' := inj'✝¹ } a) (↑{ toFun := toFun✝¹, inj' := inj'✝¹ } b) ↔ r a btoFun✝: α → βinj'✝: Injective toFun✝map_rel_iff'✝: ∀ {a b : α}, s (↑{ toFun := toFun✝, inj' := inj'✝ } a) (↑{ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a bh: (fun x => x.toFun) { toEmbedding := { toFun := toFun✝¹, inj' := inj'✝¹ }, map_rel_iff' := map_rel_iff'✝¹ } =   (fun x => x.toFun) { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ }mk.mk.mk.mk{ toEmbedding := { toFun := toFun✝¹, inj' := inj'✝¹ }, map_rel_iff' := map_rel_iff'✝¹ } =   { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ }
α: Type ?u.27070β: Type ?u.27073γ: Type ?u.27076δ: Type ?u.27079r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf, g: r ↪r sh: (fun x => x.toFun) f = (fun x => x.toFun) gf = gcongrGoals accomplished! 🐙
map_rel f: ?m.27227f a: ?m.27230a b: ?m.27233b := Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr (map_rel_iff': ∀ {α : Type ?u.27240} {β : Type ?u.27239} {r : α → α → Prop} {s : β → β → Prop} (self : r ↪r s) {a b : α},
s (↑self.toEmbedding a) (↑self.toEmbedding b) ↔ r a bmap_rel_iff' f: ?m.27227f)

/-- See Note [custom simps projection]. We specify this explicitly because we have a coercion not
given by the `FunLike` instance. Todo: remove that instance?
-/
def Simps.apply: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → α → βSimps.apply (h: r ↪r sh : r: α → α → Propr ↪r s: β → β → Props) : α: Type ?u.28062α → β: Type ?u.28065β :=
h: r ↪r sh

initialize_simps_projections RelEmbedding: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)RelEmbedding (toFun: {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → r ↪r s → α → βtoFun → apply: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → α → βapply)

@[simp]
theorem coe_toEmbedding: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : r ↪r s}, ↑f.toEmbedding = ↑fcoe_toEmbedding : ((f: ?m.28660f : r: α → α → Propr ↪r s: β → β → Props).toEmbedding: {α : Type ?u.28693} → {β : Type ?u.28692} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → α ↪ βtoEmbedding : α: Type ?u.28602α → β: Type ?u.28605β)  = f: ?m.28660f :=
rfl: ∀ {α : Sort ?u.29211} {a : α}, a = arfl
#align rel_embedding.coe_fn_to_embedding RelEmbedding.coe_toEmbedding: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : r ↪r s}, ↑f.toEmbedding = ↑fRelEmbedding.coe_toEmbedding

@[simp]
theorem coe_toRelHom: ∀ {f : r ↪r s}, ↑(toRelHom f) = ↑fcoe_toRelHom : ((f: ?m.29309f : r: α → α → Propr ↪r s: β → β → Props).toRelHom: {α : Type ?u.29342} → {β : Type ?u.29341} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → r →r stoRelHom : α: Type ?u.29251α → β: Type ?u.29254β) = f: ?m.29309f :=
rfl: ∀ {α : Sort ?u.29882} {a : α}, a = arfl

theorem injective: ∀ (f : r ↪r s), Injective ↑finjective (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) : Injective: {α : Sort ?u.29992} → {β : Sort ?u.29991} → (α → β) → PropInjective f: r ↪r sf :=
f: r ↪r sf.inj': ∀ {α : Sort ?u.30166} {β : Sort ?u.30165} (self : α ↪ β), Injective self.toFuninj'
#align rel_embedding.injective RelEmbedding.injective: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), Injective ↑fRelEmbedding.injective

theorem inj: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α}, ↑f a = ↑f b ↔ a = binj (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) {a: αa b: αb} : f: r ↪r sf a: ?m.30239a = f: r ↪r sf b: ?m.30242b ↔ a: ?m.30239a = b: ?m.30242b :=
f: r ↪r sf.injective: ∀ {α : Type ?u.30501} {β : Type ?u.30502} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), Injective ↑finjective.eq_iff: ∀ {α : Sort ?u.30519} {β : Sort ?u.30520} {f : α → β}, Injective f → ∀ {a b : α}, f a = f b ↔ a = beq_iff
#align rel_embedding.inj RelEmbedding.inj: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α}, ↑f a = ↑f b ↔ a = bRelEmbedding.inj

theorem map_rel_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α}, s (↑f a) (↑f b) ↔ r a bmap_rel_iff (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) {a: αa b: αb} : s: β → β → Props (f: r ↪r sf a: ?m.30621a) (f: r ↪r sf b: ?m.30624b) ↔ r: α → α → Propr a: ?m.30621a b: ?m.30624b :=
f: r ↪r sf.map_rel_iff': ∀ {α : Type ?u.30879} {β : Type ?u.30878} {r : α → α → Prop} {s : β → β → Prop} (self : r ↪r s) {a b : α},
s (↑self.toEmbedding a) (↑self.toEmbedding b) ↔ r a bmap_rel_iff'
#align rel_embedding.map_rel_iff RelEmbedding.map_rel_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α}, s (↑f a) (↑f b) ↔ r a bRelEmbedding.map_rel_iff

@[simp]
theorem coe_mk: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : α ↪ β}
{h : ∀ {a b : α}, s (↑f a) (↑f b) ↔ r a b}, ↑{ toEmbedding := f, map_rel_iff' := h } = ↑fcoe_mk : ⇑(⟨f: ?m.31007f, h: ?m.31049h⟩ : r: α → α → Propr ↪r s: β → β → Props) = f: ?m.31007f :=
rfl: ∀ {α : Sort ?u.31583} {a : α}, a = arfl
#align rel_embedding.coe_fn_mk RelEmbedding.coe_mk: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : α ↪ β}
{h : ∀ {a b : α}, s (↑f a) (↑f b) ↔ r a b}, ↑{ toEmbedding := f, map_rel_iff' := h } = ↑fRelEmbedding.coe_mk

/-- The map `coe_fn : (r ↪r s) → (α → β)` is injective. -/
theorem coe_fn_injective: Injective fun f => ↑fcoe_fn_injective : Injective: {α : Sort ?u.31685} → {β : Sort ?u.31684} → (α → β) → PropInjective fun f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props => (f: r ↪r sf : α: Type ?u.31648α → β: Type ?u.31651β) :=
FunLike.coe_injective: ∀ {F : Sort ?u.31863} {α : Sort ?u.31864} {β : α → Sort ?u.31865} [i : FunLike F α β], Injective fun f => ↑fFunLike.coe_injective
#align rel_embedding.coe_fn_injective RelEmbedding.coe_fn_injective: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Injective fun f => ↑fRelEmbedding.coe_fn_injective

@[ext]
theorem ext: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ↪r s⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext ⦃f: r ↪r sf g: r ↪r sg : r: α → α → Propr ↪r s: β → β → Props⦄ (h: ∀ (x : α), ↑f x = ↑g xh : ∀ x: ?m.32079x, f: r ↪r sf x: ?m.32079x = g: r ↪r sg x: ?m.32079x) : f: r ↪r sf = g: r ↪r sg :=
FunLike.ext: ∀ {F : Sort ?u.32341} {α : Sort ?u.32342} {β : α → Sort ?u.32340} [i : FunLike F α β] (f g : F),
(∀ (x : α), ↑f x = ↑g x) → f = gFunLike.ext _: ?m.32343_ _: ?m.32343_ h: ∀ (x : α), ↑f x = ↑g xh
#align rel_embedding.ext RelEmbedding.ext: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ↪r s⦄, (∀ (x : α), ↑f x = ↑g x) → f = gRelEmbedding.ext

theorem ext_iff: ∀ {f g : r ↪r s}, f = g ↔ ∀ (x : α), ↑f x = ↑g xext_iff {f: r ↪r sf g: r ↪r sg : r: α → α → Propr ↪r s: β → β → Props} : f: r ↪r sf = g: r ↪r sg ↔ ∀ x: ?m.32593x, f: r ↪r sf x: ?m.32593x = g: r ↪r sg x: ?m.32593x :=
FunLike.ext_iff: ∀ {F : Sort ?u.32842} {α : Sort ?u.32844} {β : α → Sort ?u.32843} [i : FunLike F α β] {f g : F},
f = g ↔ ∀ (x : α), ↑f x = ↑g xFunLike.ext_iff
#align rel_embedding.ext_iff RelEmbedding.ext_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r ↪r s}, f = g ↔ ∀ (x : α), ↑f x = ↑g xRelEmbedding.ext_iff

/-- Identity map is a relation embedding. -/
@[refl, simps!]
protected def refl: (r : α → α → Prop) → r ↪r rrefl (r: α → α → Propr : α: Type ?u.32992α → α: Type ?u.32992α → Prop: TypeProp) : r: α → α → Propr ↪r r: α → α → Propr :=
⟨Embedding.refl: (α : Sort ?u.33076) → α ↪ αEmbedding.refl _: Sort ?u.33076_, Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl⟩
#align rel_embedding.refl RelEmbedding.refl: {α : Type u_1} → (r : α → α → Prop) → r ↪r rRelEmbedding.refl
#align rel_embedding.refl_apply RelEmbedding.refl_apply: ∀ {α : Type u_1} (r : α → α → Prop) (a : α), ↑(RelEmbedding.refl r) a = aRelEmbedding.refl_apply

/-- Composition of two relation embeddings is a relation embedding. -/
protected def trans: {α : Type u_1} →
{β : Type u_2} →
{γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r ttrans (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) (g: s ↪r tg : s: β → β → Props ↪r t: γ → γ → Propt) : r: α → α → Propr ↪r t: γ → γ → Propt :=
⟨f: r ↪r sf.1: {α : Type ?u.33321} → {β : Type ?u.33320} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → α ↪ β1.trans: {α : Sort ?u.33340} → {β : Sort ?u.33339} → {γ : Sort ?u.33338} → (α ↪ β) → (β ↪ γ) → α ↪ γtrans g: s ↪r tg.1: {α : Type ?u.33354} → {β : Type ?u.33353} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → α ↪ β1, byGoals accomplished! 🐙 α: Type ?u.33205β: Type ?u.33208γ: Type ?u.33211δ: Type ?u.33214r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: r ↪r sg: s ↪r t∀ {a b : α},
t (↑(Embedding.trans f.toEmbedding g.toEmbedding) a) (↑(Embedding.trans f.toEmbedding g.toEmbedding) b) ↔ r a bsimp [f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.33376} {β : Type ?u.33377} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff, g: s ↪r tg.map_rel_iff: ∀ {α : Type ?u.33428} {β : Type ?u.33429} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff]Goals accomplished! 🐙⟩
#align rel_embedding.trans RelEmbedding.trans: {α : Type u_1} →
{β : Type u_2} →
{γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r tRelEmbedding.trans

instance: {α : Type u_1} → (r : α → α → Prop) → Inhabited (r ↪r r)instance (r: α → α → Propr : α: Type ?u.34885α → α: Type ?u.34885α → Prop: TypeProp) : Inhabited: Sort ?u.34927 → Sort (max1?u.34927)Inhabited (r: α → α → Propr ↪r r: α → α → Propr) :=
⟨RelEmbedding.refl: {α : Type ?u.34951} → (r : α → α → Prop) → r ↪r rRelEmbedding.refl _: ?m.34952 → ?m.34952 → Prop_⟩

theorem trans_apply: ∀ (f : r ↪r s) (g : s ↪r t) (a : α), ↑(RelEmbedding.trans f g) a = ↑g (↑f a)trans_apply (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) (g: s ↪r tg : s: β → β → Props ↪r t: γ → γ → Propt) (a: αa : α: Type ?u.35056α) : (f: r ↪r sf.trans: {α : Type ?u.35133} →
{β : Type ?u.35132} →
{γ : Type ?u.35131} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r ttrans g: s ↪r tg) a: αa = g: s ↪r tg (f: r ↪r sf a: αa) :=
rfl: ∀ {α : Sort ?u.35609} {a : α}, a = arfl
#align rel_embedding.trans_apply RelEmbedding.trans_apply: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ↪r s)
(g : s ↪r t) (a : α), ↑(RelEmbedding.trans f g) a = ↑g (↑f a)RelEmbedding.trans_apply

@[simp]
theorem coe_trans: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ↪r s)
(g : s ↪r t), ↑(RelEmbedding.trans f g) = ↑g ∘ ↑fcoe_trans (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) (g: s ↪r tg : s: β → β → Props ↪r t: γ → γ → Propt) : (f: r ↪r sf.trans: {α : Type ?u.35710} →
{β : Type ?u.35709} →
{γ : Type ?u.35708} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r ttrans g: s ↪r tg) = g: s ↪r tg ∘ f: r ↪r sf :=
rfl: ∀ {α : Sort ?u.36637} {a : α}, a = arfl
#align rel_embedding.coe_trans RelEmbedding.coe_trans: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ↪r s)
(g : s ↪r t), ↑(RelEmbedding.trans f g) = ↑g ∘ ↑fRelEmbedding.coe_trans

/-- A relation embedding is also a relation embedding between dual relations. -/
protected def swap: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → swap r ↪r swap sswap (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) : swap: {α : Sort ?u.36772} →
{β : Sort ?u.36771} → {φ : α → β → Sort ?u.36770} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x yswap r: α → α → Propr ↪r swap: {α : Sort ?u.36798} →
{β : Sort ?u.36797} → {φ : α → β → Sort ?u.36796} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x yswap s: β → β → Props :=
⟨f: r ↪r sf.toEmbedding: {α : Type ?u.36849} → {β : Type ?u.36848} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → α ↪ βtoEmbedding, f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.36862} {β : Type ?u.36863} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff⟩
#align rel_embedding.swap RelEmbedding.swap: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → swap r ↪r swap sRelEmbedding.swap

/-- If `f` is injective, then it is a relation embedding from the
preimage relation of `s` to `s`. -/
def preimage: {α : Type u_1} → {β : Type u_2} → (f : α ↪ β) → (s : β → β → Prop) → ↑f ⁻¹'o s ↪r spreimage (f: α ↪ βf : α: Type ?u.37053α ↪ β: Type ?u.37056β) (s: β → β → Props : β: Type ?u.37056β → β: Type ?u.37056β → Prop: TypeProp) : f: α ↪ βf ⁻¹'o s: β → β → Props ↪r s: β → β → Props :=
⟨f: α ↪ βf, Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl⟩
#align rel_embedding.preimage RelEmbedding.preimage: {α : Type u_1} → {β : Type u_2} → (f : α ↪ β) → (s : β → β → Prop) → ↑f ⁻¹'o s ↪r sRelEmbedding.preimage

theorem eq_preimage: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), r = ↑f ⁻¹'o seq_preimage (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) : r: α → α → Propr = f: r ↪r sf ⁻¹'o s: β → β → Props := byGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.37374δ: Type ?u.37377r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: r ↪r sr = ↑f ⁻¹'o sext (a: ?αa b: ?αb)α: Type u_1β: Type u_2γ: Type ?u.37374δ: Type ?u.37377r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: r ↪r sa, b: αh.h.ar a b ↔ (↑f ⁻¹'o s) a b
α: Type u_1β: Type u_2γ: Type ?u.37374δ: Type ?u.37377r: α → α → Props: β → β → Propt: γ → γ → Propu: δ → δ → Propf: r ↪r sr = ↑f ⁻¹'o sexact f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.37687} {β : Type ?u.37688} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symmGoals accomplished! 🐙
#align rel_embedding.eq_preimage RelEmbedding.eq_preimage: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s), r = ↑f ⁻¹'o sRelEmbedding.eq_preimage

protected theorem isIrrefl: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsIrrefl β s], IsIrrefl α risIrrefl (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) [IsIrrefl: (α : Type ?u.37787) → (α → α → Prop) → PropIsIrrefl β: Type ?u.37736β s: β → β → Props] : IsIrrefl: (α : Type ?u.37792) → (α → α → Prop) → PropIsIrrefl α: Type ?u.37733α r: α → α → Propr :=
⟨fun a: ?m.37812a => mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬amt f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.37818} {β : Type ?u.37819} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 (irrefl: ∀ {α : Type ?u.37847} {r : α → α → Prop} [inst : IsIrrefl α r] (a : α), ¬r a airrefl (f: r ↪r sf a: ?m.37812a))⟩
#align rel_embedding.is_irrefl RelEmbedding.isIrrefl: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsIrrefl β s], IsIrrefl α rRelEmbedding.isIrrefl

protected theorem isRefl: r ↪r s → ∀ [inst : IsRefl β s], IsRefl α risRefl (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) [IsRefl: (α : Type ?u.38088) → (α → α → Prop) → PropIsRefl β: Type ?u.38037β s: β → β → Props] : IsRefl: (α : Type ?u.38093) → (α → α → Prop) → PropIsRefl α: Type ?u.38034α r: α → α → Propr :=
⟨fun _: ?m.38112_ => f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.38114} {β : Type ?u.38115} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 <| refl: ∀ {α : Type ?u.38140} {r : α → α → Prop} [inst : IsRefl α r] (a : α), r a arefl _: ?m.38141_⟩
#align rel_embedding.is_refl RelEmbedding.isRefl: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsRefl β s], IsRefl α rRelEmbedding.isRefl

protected theorem isSymm: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsSymm β s], IsSymm α risSymm (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) [IsSymm: (α : Type ?u.38247) → (α → α → Prop) → PropIsSymm β: Type ?u.38196β s: β → β → Props] : IsSymm: (α : Type ?u.38252) → (α → α → Prop) → PropIsSymm α: Type ?u.38193α r: α → α → Propr :=
⟨fun _: ?m.38271_ _: ?m.38274_ => imp_imp_imp: ∀ {a b c d : Prop}, (c → a) → (b → d) → (a → b) → c → dimp_imp_imp f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.38282} {β : Type ?u.38283} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.38311} {β : Type ?u.38312} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 symm: ∀ {α : Type ?u.38328} {r : α → α → Prop} [inst : IsSymm α r] {a b : α}, r a b → r b asymm⟩
#align rel_embedding.is_symm RelEmbedding.isSymm: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsSymm β s], IsSymm α rRelEmbedding.isSymm

protected theorem isAsymm: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsAsymm β s], IsAsymm α risAsymm (f: r ↪r sf : r: α → α → Propr ↪r s: β → β → Props) [IsAsymm: (α : Type ?u.38433) → (α → α → Prop) → PropIsAsymm β: Type ?u.38382β s: β → β → Props] : IsAsymm: (α : Type ?u.38438) → (α → α → Prop) → PropIsAsymm α: Type ?u.38379α r: α → α → Propr :=
⟨fun _: ?m.38460_ _: ?m.38463_ h₁: ?m.38466h₁ h₂: ?m.38469h₂ => asymm: ∀ {α : Type ?u.38471} {r : α → α → Prop} [inst : IsAsymm α r] {a b : α}, r a b → ¬r b aasymm (f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.38477} {β : Type ?u.38478} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h₁: ?m.38466h₁) (f: r ↪r sf.map_rel_iff: ∀ {α : Type ?u.38518} {β : Type ?u.38519} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) {a b : α},
s (↑f a) (↑f b) ↔ r a bmap_rel_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h₂: ?m.38469h₂)⟩
#align rel_embedding.is_asymm RelEmbedding.isAsymm: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsAsymm β s], IsAsymm α rRelEmbedding.isAsymm

protected theorem isAntisymm: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsAntisymm β s], IsAntisymm α risAntisymm : ∀ (_: r ↪r s_ : r: α → α → Propr ↪r s: β → β → Props) [IsAntisymm: (α : Type ?u.38621) → (α → α → Prop) → PropIsAntisymm β: Type ?u.38569β s: β → β → Props], IsAntisymm: (α : Type ?u.38626) → (α → α → Prop) → PropIsAntisymm α: Type ?u.38566α r: α → α → Propr
| ⟨f: α ↪ βf, o: ∀ {a b : α}, s (↑f a) (↑f b) ↔ r a bo⟩, ⟨H: ∀ (a b : β), s a b → s b a → a = bH⟩ => ⟨fun _: ?m.38749_ _: ?m.38752_ h₁: ?m.38755h₁ h₂: ?m.38758h₂ => f: α ↪ βf.inj': ∀ {α : Sort ?u.38761} {β : Sort ?u.38760} (self : α ↪ β), Injective self.toFuninj' (H: ∀ (a b : β), s a b → s b a → a = bH _: β_ _: β_ (o: ∀ {a b : α}, s (↑f a) (↑f b) ↔ r a bo.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h₁: ?m.38755h₁) (o: ∀ {a b : α}, s (↑f a) (↑f b) ↔ r a bo.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h₂: ?m.38758h₂))⟩
#align rel_embedding.is_antisymm RelEmbedding.isAntisymm: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsAntisymm β s], IsAntisymm α rRelEmbedding.isAntisymm

protected theorem isTrans: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsTrans β s], IsTrans α risTrans : ∀ (_: r ↪r s_ : r: α → α → Propr ↪r s: β → β → Props) [IsTrans: (α : Type ?u.39026) → (α → α → Prop) → PropIsTrans β: Type ?u.38974β s: β → β → Props], IsTrans: (α : Type ?u.39031) → (α → α → Prop) → PropIsTrans α: Type ?u.38971α r: α → α → Propr
| ⟨_, o: ∀ {a b : α}, s (↑toEmbedding✝ a) (↑toEmbedding✝ b) ↔ r a bo⟩, ⟨H: ∀ (a b c : β), s a b → s b c → s a cH⟩ => ⟨fun _: ?m.39165_ _: ?m.39168_ _: ?m.39171_ h₁: ?m.39174h₁ h₂: ?m.39177h₂ => o: ∀ {a b : α}, s (↑toEmbedding✝ a) (↑toEmbedding✝ b) ↔ r a bo.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 (H: ∀ (a b c : β), s a b → s b c → s a cH _: β_ _: β_ _: β_ (o: ∀ {a b : α}, s (↑toEmbedding✝ a) (↑toEmbedding✝ b) ↔ r a bo.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h₁: ?m.39174h₁) (o: ∀ {a b : α}, s (↑toEmbedding✝ a) (↑toEmbedding✝ b) ↔ r a bo.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h₂: ?m.39177h₂))⟩
#align rel_embedding.is_trans RelEmbedding.isTrans: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsTrans β s], IsTrans α rRelEmbedding.isTrans

protected theorem isTotal: r ↪r s → ∀ [inst : IsTotal β s], IsTotal α risTotal : ∀ (_: r ↪r s_ : r: α → α → Propr ↪r s: β → β → Props) [IsTotal: (α : Type ?u.39454) → (α → α → Prop) → PropIsTotal β: Type ?u.39402β s: β → β → Props], IsTotal: (α : Type ?u.39459) → (α → α → Prop) → PropIsTotal α: Type ?u.39399α r: α → α → Propr
| ⟨_, o: ∀ {a b : α}, s (↑toEmbedding✝ a) (↑toEmbedding✝ b) ↔ r a bo⟩, ⟨H: ∀ (a b : β), s a b ∨ s b aH⟩ => ⟨fun _: ?m.39586_ _: ?m.39589_ => (or_congr: ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∨ b ↔ c ∨ d)or_congr o: ∀ {a b : α}, s (↑toEmbedding✝ a) (↑toEmbedding✝ b) ↔ r a bo o: ∀ {a b : α}, s (↑toEmbedding✝ a) (↑toEmbedding✝ b) ↔ r a bo).1: ∀ {a b : Prop}, (a ↔ b) → a → b1 (H: ∀ (a b : β), s a b ∨ s b aH _: β_ _: β_)⟩
#align rel_embedding.is_total RelEmbedding.isTotal: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, r ↪r s → ∀ [inst : IsTotal β s], IsTotal α rRelEmbedding.isTotal

protected theorem isPreorder: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsPreorder β s], IsPreorder α risPreorder : ∀ (_: r ↪r s_ : r: α → α → Propr ↪r s: β → β → Props) [IsPreorder: (α : Type ?u.39834) → (α → α → Prop) → PropIsPreorder β: Type ?u.39782β s: β → β → Props], IsPreorder: (α : Type ?u.39839) → (α → α → Prop) → PropIsPreorder α: Type ?u.39779α r: α → α → Propr
| f: r ↪r sf, _ => { f.isRefl, f.isTrans with }: IsPreorder ?m.40049 ?m.40050{ f: r ↪r sf{ f.isRefl, f.isTrans with }: IsPreorder ?m.40049 ?m.40050.isRefl: ∀ {α : Type ?u.39867} {β : Type ?u.39868} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsRefl β s], IsRefl α risRefl{ f.isRefl, f.isTrans with }: IsPreorder ?m.40049 ?m.40050, f: r ↪r sf{ f.isRefl, f.isTrans with }: IsPreorder ?m.40049 ?m.40050.isTrans: ∀ {α : Type ?u.39926} {β : Type ?u.39927} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsTrans β s], IsTrans α risTrans{ f.isRefl, f.isTrans with }: IsPreorder ?m.40049 ?m.40050 { f.isRefl, f.isTrans with }: IsPreorder ?m.40049 ?m.40050with{ f.isRefl, f.isTrans with }: IsPreorder ?m.40049 ?m.40050 }
#align rel_embedding.is_preorder RelEmbedding.isPreorder: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsPreorder β s], IsPreorder α rRelEmbedding.isPreorder

protected theorem isPartialOrder: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsPartialOrder β s], IsPartialOrder α risPartialOrder : ∀ (_: r ↪r s_ : r: α → α → Propr ↪r s: β → β → Props) [IsPartialOrder: (α : Type ?u.40226) → (α → α → Prop) → PropIsPartialOrder β: Type ?u.40174β s: β → β → Props], IsPartialOrder: (α : Type ?u.40231) → (α → α → Prop) → PropIsPartialOrder α: Type ?u.40171α r: α → α → Propr
| f: r ↪r sf, _ => { f.isPreorder, f.isAntisymm with }: IsPartialOrder ?m.40361 ?m.40362{ f: r ↪r sf{ f.isPreorder, f.isAntisymm with }: IsPartialOrder ?m.40361 ?m.40362.isPreorder: ∀ {α : Type ?u.40259} {β : Type ?u.40260} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsPreorder β s], IsPreorder α risPreorder{ f.isPreorder, f.isAntisymm with }: IsPartialOrder ?m.40361 ?m.40362, f: r ↪r sf{ f.isPreorder, f.isAntisymm with }: IsPartialOrder ?m.40361 ?m.40362.isAntisymm: ∀ {α : Type ?u.40322} {β : Type ?u.40323} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsAntisymm β s], IsAntisymm α risAntisymm{ f.isPreorder, f.isAntisymm with }: IsPartialOrder ?m.40361 ?m.40362 { f.isPreorder, f.isAntisymm with }: IsPartialOrder ?m.40361 ?m.40362with{ f.isPreorder, f.isAntisymm with }: IsPartialOrder ?m.40361 ?m.40362 }
#align rel_embedding.is_partial_order RelEmbedding.isPartialOrder: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop},
r ↪r s → ∀ [inst : IsPartialOrder β s], IsPartialOrder α rRelEmbedding.isPartialOrder

protected theorem isLinearOrder: r ↪r s → ∀ [inst : IsLinearOrder β s], IsLinearOrder α risLinearOrder : ∀ (_: r ↪r s_ : r: α → α → Propr ↪r s: β → β → Props) [IsLinearOrder: (α : Type ?u.40548) → (α → α → Prop) → PropIsLinearOrder β: Type ?u.40496β s: β → β → Props], IsLinearOrder: (α : Type ?u.40553) → (α → α → Prop) → PropIsLinearOrder α: Type ?u.40493α r: α → α → Propr
| f: r ↪r sf, _ => { f.isPartialOrder, f.isTotal wit```