/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Floris van Doorn

! This file was ported from Lean 3 source module order.initial_seg
! leanprover-community/mathlib commit 730c6d4cab72b9d84fcfb9e95e8796e9cd8f40ba
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.RelIso.Set
import Mathlib.Order.WellFounded
/-!
# Initial and principal segments

This file defines initial and principal segments.

## Main definitions

* `InitialSeg r s`: type of order embeddings of `r` into `s` for which the range is an initial
  segment (i.e., if `b` belongs to the range, then any `b' < b` also belongs to the range).
  It is denoted by `r ≼i s`.
* `PrincipalSeg r s`: Type of order embeddings of `r` into `s` for which the range is a principal
  segment, i.e., an interval of the form `(-∞, top)` for some element `top`. It is denoted by
  `r ≺i s`.

## Notations

These notations belong to the `InitialSeg` locale.

* `r ≼i s`: the type of initial segment embeddings of `r` into `s`.
* `r ≺i s`: the type of principal segment embeddings of `r` into `s`.
-/


/-!
### Initial segments

Order embeddings whose range is an initial segment of `s` (i.e., if `b` belongs to the range, then
any `b' < b` also belongs to the range). The type of these embeddings from `r` to `s` is called
`InitialSeg r s`, and denoted by `r ≼i s`.
-/


variable {α: Type ?u.2
α : Type _: Type (?u.25605+1)
Type _} {β: Type ?u.23711
β : Type _: Type (?u.5+1)
Type _} {γ: Type ?u.66065
γ : Type _: Type (?u.66413+1)
Type _} {r: α → α → Prop
r : α: Type ?u.16733
α → α: Type ?u.1135
α → Prop: Type
Prop} {s: β → β → Prop
s : β: Type ?u.1138
β → β: Type ?u.1138
β → Prop: Type
Prop}
  {t: γ → γ → Prop
t : γ: Type ?u.71753
γ → γ: Type ?u.1141
γ → Prop: Type
Prop}

open Function

/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≼i s` is an order
embedding whose range is an initial segment. That is, whenever `b < f a` in `β` then `b` is in the
range of `f`. -/
structure InitialSeg: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)
InitialSeg {α: Type ?u.56
α β: Type ?u.59
β : Type _: Type (?u.56+1)
Type _} (r: α → α → Prop
r : α: Type ?u.56
α → α: Type ?u.56
α → Prop: Type
Prop) (s: β → β → Prop
s : β: Type ?u.59
β → β: Type ?u.59
β → Prop: Type
Prop) extends r: α → α → Prop
r ↪r s: β → β → Prop
s where
  /-- The order embedding is an initial segment -/
  init': ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (self : InitialSeg r s) (a : α) (b : β),
  s b (↑self.toRelEmbedding a) → ∃ a', ↑self.toRelEmbedding a' = b
init' : ∀ a: ?m.99
a b: ?m.102
b, s: β → β → Prop
s b: ?m.102
b (toRelEmbedding: r ↪r s
toRelEmbedding a: ?m.99
a) → ∃ a': ?m.257
a', toRelEmbedding: r ↪r s
toRelEmbedding a': ?m.257
a' = b: ?m.102
b
#align initial_seg InitialSeg: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)
InitialSeg

-- Porting notes: Deleted `scoped[InitialSeg]`
/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≼i s` is an order
embedding whose range is an initial segment. That is, whenever `b < f a` in `β` then `b` is in the
range of `f`. -/
infixl:25 " ≼i " => InitialSeg: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)
InitialSeg

namespace InitialSeg

instance: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → Coe (r ≼i s) (r ↪r s)
instance : Coe: semiOutParam (Sort ?u.9117) → Sort ?u.9116 → Sort (max(max1?u.9117)?u.9116)
Coe (r: α → α → Prop
r ≼i s: β → β → Prop
s) (r: α → α → Prop
r ↪r s: β → β → Prop
s) :=
  ⟨InitialSeg.toRelEmbedding: {α : Type ?u.9161} → {β : Type ?u.9160} → {r : α → α → Prop} → {s : β → β → Prop} → r ≼i s → r ↪r s
InitialSeg.toRelEmbedding⟩

instance: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → EmbeddingLike (r ≼i s) α β
instance : EmbeddingLike: Sort ?u.9480 → outParam (Sort ?u.9479) → outParam (Sort ?u.9478) → Sort (max(max(max1?u.9480)?u.9479)?u.9478)
EmbeddingLike (r: α → α → Prop
r ≼i s: β → β → Prop
s) α: Type ?u.9451
α β: Type ?u.9454
β :=
  { coe := fun f: ?m.9521
f => f: ?m.9521
f.toFun: {α : Sort ?u.9560} → {β : Sort ?u.9559} → (α ↪ β) → α → β
toFun
    coe_injective' := by
Goals accomplished! 🐙
      α: Type ?u.9451

β: Type ?u.9454

γ: Type ?u.9457

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

Injective fun f => f.toFunrintro ⟨f, hf⟩: r ≼i s
⟨f: r ↪r s
f⟨f, hf⟩: r ≼i s
, hf: ∀ (a : α) (b : β), s b (↑f a) → ∃ a', ↑f a' = b
hf⟨f, hf⟩: r ≼i s
⟩ ⟨g, hg⟩: r ≼i s
⟨g: r ↪r s
g⟨g, hg⟩: r ≼i s
, hg: ∀ (a : α) (b : β), s b (↑g a) → ∃ a', ↑g a' = b
hg⟨g, hg⟩: r ≼i s
⟩ h: (fun f => f.toFun) { toRelEmbedding := f, init' := hf } = (fun f => f.toFun) { toRelEmbedding := g, init' := hg }
hα: Type ?u.9451

β: Type ?u.9454

γ: Type ?u.9457

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ↪r s

hf: ∀ (a : α) (b : β), s b (↑f a) → ∃ a', ↑f a' = b

g: r ↪r s

hg: ∀ (a : α) (b : β), s b (↑g a) → ∃ a', ↑g a' = b

h: (fun f => f.toFun) { toRelEmbedding := f, init' := hf } = (fun f => f.toFun) { toRelEmbedding := g, init' := hg }

mk.mk{ toRelEmbedding := f, init' := hf } = { toRelEmbedding := g, init' := hg }
      α: Type ?u.9451

β: Type ?u.9454

γ: Type ?u.9457

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

Injective fun f => f.toFuncongr with x: ?α
xα: Type ?u.9451

β: Type ?u.9454

γ: Type ?u.9457

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ↪r s

hf: ∀ (a : α) (b : β), s b (↑f a) → ∃ a', ↑f a' = b

g: r ↪r s

hg: ∀ (a : α) (b : β), s b (↑g a) → ∃ a', ↑g a' = b

h: (fun f => f.toFun) { toRelEmbedding := f, init' := hf } = (fun f => f.toFun) { toRelEmbedding := g, init' := hg }

x: α

mk.mk.e_toRelEmbedding.h↑f x = ↑g x
      α: Type ?u.9451

β: Type ?u.9454

γ: Type ?u.9457

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

Injective fun f => f.toFunexact congr_fun: ∀ {α : Sort ?u.9928} {β : α → Sort ?u.9927} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_fun h: (fun f => f.toFun) { toRelEmbedding := f, init' := hf } = (fun f => f.toFun) { toRelEmbedding := g, init' := hg }
h x: ?α
x
Goals accomplished! 🐙,
    injective' := fun f: ?m.9573
f => f: ?m.9573
f.inj': ∀ {α : Sort ?u.9596} {β : Sort ?u.9595} (self : α ↪ β), Injective self.toFun
inj' }

@[ext] lemma ext: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r ≼i s}, (∀ (x : α), ↑f x = ↑g x) → f = g
ext {f: r ≼i s
f g: r ≼i s
g : r: α → α → Prop
r ≼i s: β → β → Prop
s} (h: ∀ (x : α), ↑f x = ↑g x
h : ∀ x: ?m.10417
x, f: r ≼i s
f x: ?m.10417
x = g: r ≼i s
g x: ?m.10417
x) : f: r ≼i s
f = g: r ≼i s
g :=
  FunLike.ext: ∀ {F : Sort ?u.10642} {α : Sort ?u.10643} {β : α → Sort ?u.10641} [i : FunLike F α β] (f g : F),
  (∀ (x : α), ↑f x = ↑g x) → f = g
FunLike.ext f: r ≼i s
f g: r ≼i s
g h: ∀ (x : α), ↑f x = ↑g x
h
#align initial_seg.ext InitialSeg.ext: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f g : r ≼i s}, (∀ (x : α), ↑f x = ↑g x) → f = g
InitialSeg.ext

@[simp]
theorem coe_coe_fn: ∀ (f : r ≼i s), ↑f.toRelEmbedding = ↑f
coe_coe_fn (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) : ((f: r ≼i s
f : r: α → α → Prop
r ↪r s: β → β → Prop
s) : α: Type ?u.10766
α → β: Type ?u.10769
β) = f: r ≼i s
f :=
  rfl: ∀ {α : Sort ?u.11440} {a : α}, a = a
rfl
#align initial_seg.coe_coe_fn InitialSeg.coe_coe_fn: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s), ↑f.toRelEmbedding = ↑f
InitialSeg.coe_coe_fn

theorem init: ∀ (f : r ≼i s) {a : α} {b : β}, s b (↑f a) → ∃ a', ↑f a' = b
init (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) {a: α
a : α: Type ?u.11486
α} {b: β
b : β: Type ?u.11489
β} : s: β → β → Prop
s b: β
b (f: r ≼i s
f a: α
a) → ∃ a': ?m.11656
a', f: r ≼i s
f a': ?m.11656
a' = b: β
b :=
  f: r ≼i s
f.init': ∀ {α : Type ?u.11762} {β : Type ?u.11761} {r : α → α → Prop} {s : β → β → Prop} (self : r ≼i s) (a : α) (b : β),
  s b (↑self.toRelEmbedding a) → ∃ a', ↑self.toRelEmbedding a' = b
init' _: ?m.11763
_ _: ?m.11764
_
#align initial_seg.init InitialSeg.init: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) → ∃ a', ↑f a' = b
InitialSeg.init

theorem map_rel_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : r ≼i s), s (↑f a) (↑f b) ↔ r a b
map_rel_iff (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) : s: β → β → Prop
s (f: r ≼i s
f a: ?m.11980
a) (f: r ≼i s
f b: ?m.12190
b) ↔ r: α → α → Prop
r a: ?m.11980
a b: ?m.12190
b :=
  f: r ≼i s
f.map_rel_iff': ∀ {α : Type ?u.12422} {β : Type ?u.12421} {r : α → α → Prop} {s : β → β → Prop} (self : r ↪r s) {a b : α},
  s (↑self.toEmbedding a) (↑self.toEmbedding b) ↔ r a b
map_rel_iff'
#align initial_seg.map_rel_iff InitialSeg.map_rel_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : r ≼i s), s (↑f a) (↑f b) ↔ r a b
InitialSeg.map_rel_iff

theorem init_iff: ∀ (f : r ≼i s) {a : α} {b : β}, s b (↑f a) ↔ ∃ a', ↑f a' = b ∧ r a' a
init_iff (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) {a: α
a : α: Type ?u.12471
α} {b: β
b : β: Type ?u.12474
β} : s: β → β → Prop
s b: β
b (f: r ≼i s
f a: α
a) ↔ ∃ a': ?m.12639
a', f: r ≼i s
f a': ?m.12639
a' = b: β
b ∧ r: α → α → Prop
r a': ?m.12639
a' a: α
a :=
  ⟨fun h: ?m.12753
h => by
Goals accomplished! 🐙
    α: Type u_1

β: Type u_2

γ: Type ?u.12477

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

a: α

b: β

h: s b (↑f a)

∃ a', ↑f a' = b ∧ r a' arcases f: r ≼i s
f.init: ∀ {α : Type ?u.13014} {β : Type ?u.13015} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) → ∃ a', ↑f a' = b
init h: s b (↑f a)
h with ⟨a', rfl⟩: ∃ a', ↑f a' = b
⟨a': α
a'⟨a', rfl⟩: ∃ a', ↑f a' = b
, rfl: ↑f a' = b
rfl⟨a', rfl⟩: ∃ a', ↑f a' = b
⟩α: Type u_1

β: Type u_2

γ: Type ?u.12477

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

a, a': α

h: s (↑f a') (↑f a)

intro∃ a'_1, ↑f a'_1 = ↑f a' ∧ r a'_1 a
    α: Type u_1

β: Type u_2

γ: Type ?u.12477

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

a: α

b: β

h: s b (↑f a)

∃ a', ↑f a' = b ∧ r a' aexact ⟨a': α
a', rfl: ∀ {α : Sort ?u.13130} {a : α}, a = a
rfl, f: r ≼i s
f.map_rel_iff: ∀ {α : Type ?u.13136} {β : Type ?u.13137} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : r ≼i s),
  s (↑f a) (↑f b) ↔ r a b
map_rel_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: s (↑f a') (↑f a)
h⟩
Goals accomplished! 🐙,
    fun ⟨a': α
a', e: ↑f a' = b
e, h: r a' a
h⟩ => e: ↑f a' = b
e ▸ f: r ≼i s
f.map_rel_iff: ∀ {α : Type ?u.12833} {β : Type ?u.12834} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : r ≼i s),
  s (↑f a) (↑f b) ↔ r a b
map_rel_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: r a' a
h⟩
#align initial_seg.init_iff InitialSeg.init_iff: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) ↔ ∃ a', ↑f a' = b ∧ r a' a
InitialSeg.init_iff

/-- An order isomorphism is an initial segment -/
def ofIso: r ≃r s → r ≼i s
ofIso (f: r ≃r s
f : r: α → α → Prop
r ≃r s: β → β → Prop
s) : r: α → α → Prop
r ≼i s: β → β → Prop
s :=
  ⟨f: r ≃r s
f, fun _: ?m.13441
_ b: ?m.13444
b _: ?m.13447
_ => ⟨f: r ≃r s
f.symm: {α : Type ?u.13462} → {β : Type ?u.13461} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → s ≃r r
symm b: ?m.13444
b, RelIso.apply_symm_apply: ∀ {α : Type ?u.13536} {β : Type ?u.13537} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : β),
  ↑e (↑(RelIso.symm e) x) = x
RelIso.apply_symm_apply f: r ≃r s
f _: ?m.13539
_⟩⟩
#align initial_seg.of_iso InitialSeg.ofIso: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → r ≼i s
InitialSeg.ofIso

/-- The identity function shows that `≼i` is reflexive -/
@[refl]
protected def refl: {α : Type u_1} → (r : α → α → Prop) → r ≼i r
refl (r: α → α → Prop
r : α: Type ?u.13762
α → α: Type ?u.13762
α → Prop: Type
Prop) : r: α → α → Prop
r ≼i r: α → α → Prop
r :=
  ⟨RelEmbedding.refl: {α : Type ?u.13837} → (r : α → α → Prop) → r ↪r r
RelEmbedding.refl _: ?m.13838 → ?m.13838 → Prop
_, fun _: ?m.13851
_ _: ?m.13854
_ _: ?m.13857
_ => ⟨_: ?m.13864
_, rfl: ∀ {α : Sort ?u.13872} {a : α}, a = a
rfl⟩⟩
#align initial_seg.refl InitialSeg.refl: {α : Type u_1} → (r : α → α → Prop) → r ≼i r
InitialSeg.refl

instance: {α : Type u_1} → (r : α → α → Prop) → Inhabited (r ≼i r)
instance (r: α → α → Prop
r : α: Type ?u.13986
α → α: Type ?u.13986
α → Prop: Type
Prop) : Inhabited: Sort ?u.14019 → Sort (max1?u.14019)
Inhabited (r: α → α → Prop
r ≼i r: α → α → Prop
r) :=
  ⟨InitialSeg.refl: {α : Type ?u.14043} → (r : α → α → Prop) → r ≼i r
InitialSeg.refl r: α → α → Prop
r⟩

/-- Composition of functions shows that `≼i` is transitive -/
@[trans]
protected def trans: {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≼i s → s ≼i t → r ≼i t
trans (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (g: s ≼i t
g : s: β → β → Prop
s ≼i t: γ → γ → Prop
t) : r: α → α → Prop
r ≼i t: γ → γ → Prop
t :=
  ⟨f: r ≼i s
f.1: {α : Type ?u.14276} → {β : Type ?u.14275} → {r : α → α → Prop} → {s : β → β → Prop} → r ≼i s → r ↪r s
1.trans: {α : Type ?u.14295} →
  {β : Type ?u.14294} →
    {γ : Type ?u.14293} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r t
trans g: s ≼i t
g.1: {α : Type ?u.14333} → {β : Type ?u.14332} → {r : α → α → Prop} → {s : β → β → Prop} → r ≼i s → r ↪r s
1, fun a: ?m.14359
a c: ?m.14362
c h: ?m.14365
h => by
Goals accomplished! 🐙
    α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

c: γ

h: t c (↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a)

∃ a', ↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a' = csimp at h: t c (↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a)
h⊢α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

c: γ

h: t c (↑g (↑f a))

∃ a', ↑g (↑f a') = c
    α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

c: γ

h: t c (↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a)

∃ a', ↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a' = crcases g: s ≼i t
g.2: ∀ {α : Type ?u.16161} {β : Type ?u.16160} {r : α → α → Prop} {s : β → β → Prop} (self : r ≼i s) (a : α) (b : β),
  s b (↑self.toRelEmbedding a) → ∃ a', ↑self.toRelEmbedding a' = b
2 _: ?m.16162
_ _: ?m.16163
_ h: t c (↑g (↑f a))
h with ⟨b, rfl⟩: ∃ a', ↑g.toRelEmbedding a' = c
⟨b: β
b⟨b, rfl⟩: ∃ a', ↑g.toRelEmbedding a' = c
, rfl: ↑g.toRelEmbedding b = c
rfl⟨b, rfl⟩: ∃ a', ↑g.toRelEmbedding a' = c
⟩α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

b: β

h: t (↑g.toRelEmbedding b) (↑g (↑f a))

intro∃ a', ↑g (↑f a') = ↑g.toRelEmbedding b;α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

b: β

h: t (↑g.toRelEmbedding b) (↑g (↑f a))

intro∃ a', ↑g (↑f a') = ↑g.toRelEmbedding b α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

c: γ

h: t c (↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a)

∃ a', ↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a' = chave h: ?m.16269
h := g: s ≼i t
g.map_rel_iff: ∀ {α : Type ?u.16270} {β : Type ?u.16271} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : r ≼i s),
  s (↑f a) (↑f b) ↔ r a b
map_rel_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: t (↑g.toRelEmbedding b) (↑g (↑f a))
hα: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

b: β

h✝: t (↑g.toRelEmbedding b) (↑g (↑f a))

h: s b (↑f a)

intro∃ a', ↑g (↑f a') = ↑g.toRelEmbedding b
    α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

c: γ

h: t c (↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a)

∃ a', ↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a' = crcases f: r ≼i s
f.2: ∀ {α : Type ?u.16292} {β : Type ?u.16291} {r : α → α → Prop} {s : β → β → Prop} (self : r ≼i s) (a : α) (b : β),
  s b (↑self.toRelEmbedding a) → ∃ a', ↑self.toRelEmbedding a' = b
2 _: ?m.16293
_ _: ?m.16294
_ h: ?m.16269
h with ⟨a', rfl⟩: ∃ a', ↑f.toRelEmbedding a' = b
⟨a': α
a'⟨a', rfl⟩: ∃ a', ↑f.toRelEmbedding a' = b
, rfl: ↑f.toRelEmbedding a' = b
rfl⟨a', rfl⟩: ∃ a', ↑f.toRelEmbedding a' = b
⟩α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a, a': α

h✝: t (↑g.toRelEmbedding (↑f.toRelEmbedding a')) (↑g (↑f a))

h: s (↑f.toRelEmbedding a') (↑f a)

intro.intro∃ a'_1, ↑g (↑f a'_1) = ↑g.toRelEmbedding (↑f.toRelEmbedding a');α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a, a': α

h✝: t (↑g.toRelEmbedding (↑f.toRelEmbedding a')) (↑g (↑f a))

h: s (↑f.toRelEmbedding a') (↑f a)

intro.intro∃ a'_1, ↑g (↑f a'_1) = ↑g.toRelEmbedding (↑f.toRelEmbedding a') α: Type ?u.14169

β: Type ?u.14172

γ: Type ?u.14175

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

g: s ≼i t

a: α

c: γ

h: t c (↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a)

∃ a', ↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a' = cexact ⟨a': α
a', rfl: ∀ {α : Sort ?u.16405} {a : α}, a = a
rfl⟩
Goals accomplished! 🐙⟩
#align initial_seg.trans InitialSeg.trans: {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≼i s → s ≼i t → r ≼i t
InitialSeg.trans

@[simp]
theorem refl_apply: ∀ (x : α), ↑(InitialSeg.refl r) x = x
refl_apply (x: α
x : α: Type ?u.16733
α) : InitialSeg.refl: {α : Type ?u.16763} → (r : α → α → Prop) → r ≼i r
InitialSeg.refl r: α → α → Prop
r x: α
x = x: α
x :=
  rfl: ∀ {α : Sort ?u.16888} {a : α}, a = a
rfl
#align initial_seg.refl_apply InitialSeg.refl_apply: ∀ {α : Type u_1} {r : α → α → Prop} (x : α), ↑(InitialSeg.refl r) x = x
InitialSeg.refl_apply

@[simp]
theorem trans_apply: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≼i s)
  (g : s ≼i t) (a : α), ↑(InitialSeg.trans f g) a = ↑g (↑f a)
trans_apply (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (g: s ≼i t
g : s: β → β → Prop
s ≼i t: γ → γ → Prop
t) (a: α
a : α: Type ?u.16929
α) : (f: r ≼i s
f.trans: {α : Type ?u.16997} →
  {β : Type ?u.16996} →
    {γ : Type ?u.16995} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≼i s → s ≼i t → r ≼i t
trans g: s ≼i t
g) a: α
a = g: s ≼i t
g (f: r ≼i s
f a: α
a) :=
  rfl: ∀ {α : Sort ?u.17380} {a : α}, a = a
rfl
#align initial_seg.trans_apply InitialSeg.trans_apply: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≼i s)
  (g : s ≼i t) (a : α), ↑(InitialSeg.trans f g) a = ↑g (↑f a)
InitialSeg.trans_apply

instance subsingleton_of_trichotomous_of_irrefl: ∀ [inst : IsTrichotomous β s] [inst : IsIrrefl β s] [inst : IsWellFounded α r], Subsingleton (r ≼i s)
subsingleton_of_trichotomous_of_irrefl [IsTrichotomous: (α : Type ?u.17481) → (α → α → Prop) → Prop
IsTrichotomous β: Type ?u.17457
β s: β → β → Prop
s] [IsIrrefl: (α : Type ?u.17486) → (α → α → Prop) → Prop
IsIrrefl β: Type ?u.17457
β s: β → β → Prop
s]
    [IsWellFounded: (α : Type ?u.17491) → (α → α → Prop) → Prop
IsWellFounded α: Type ?u.17454
α r: α → α → Prop
r] : Subsingleton: Sort ?u.17496 → Prop
Subsingleton (r: α → α → Prop
r ≼i s: β → β → Prop
s) :=
  ⟨fun f: ?m.17523
f g: ?m.17526
g => by
Goals accomplished! 🐙
    α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

f = gext a: ?α
aα: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

a: α

h↑f a = ↑g a
    α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

f = grefine' IsWellFounded.induction: ∀ {α : Type ?u.17594} (r : α → α → Prop) [inst : IsWellFounded α r] {C : α → Prop} (a : α),
  (∀ (x : α), (∀ (y : α), r y x → C y) → C x) → C a
IsWellFounded.induction r: α → α → Prop
r a: ?α
a fun b: ?m.17611
b IH: ?m.17614
IH =>
      extensional_of_trichotomous_of_irrefl: ∀ {α : Type ?u.17618} (r : α → α → Prop) [inst : IsTrichotomous α r] [inst : IsIrrefl α r] {a b : α},
  (∀ (x : α), r x a ↔ r x b) → a = b
extensional_of_trichotomous_of_irrefl s: β → β → Prop
s fun x: ?m.17654
x => _: s x ?m.17628 ↔ s x ?m.17629
_α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

a, b: α

IH: ∀ (y : α), r y b → ↑f y = ↑g y

x: β

hs x (↑f b) ↔ s x (↑g b)
    α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

f = grw [α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

a, b: α

IH: ∀ (y : α), r y b → ↑f y = ↑g y

x: β

hs x (↑f b) ↔ s x (↑g b)f: r ≼i s
f.init_iff: ∀ {α : Type ?u.17674} {β : Type ?u.17675} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) ↔ ∃ a', ↑f a' = b ∧ r a' a
init_iff,α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

a, b: α

IH: ∀ (y : α), r y b → ↑f y = ↑g y

x: β

h(∃ a', ↑f a' = x ∧ r a' b) ↔ s x (↑g b) α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

a, b: α

IH: ∀ (y : α), r y b → ↑f y = ↑g y

x: β

hs x (↑f b) ↔ s x (↑g b)g: r ≼i s
g.init_iff: ∀ {α : Type ?u.17728} {β : Type ?u.17729} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) ↔ ∃ a', ↑f a' = b ∧ r a' a
init_iffα: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

a, b: α

IH: ∀ (y : α), r y b → ↑f y = ↑g y

x: β

h(∃ a', ↑f a' = x ∧ r a' b) ↔ ∃ a', ↑g a' = x ∧ r a' b]α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

a, b: α

IH: ∀ (y : α), r y b → ↑f y = ↑g y

x: β

h(∃ a', ↑f a' = x ∧ r a' b) ↔ ∃ a', ↑g a' = x ∧ r a' b
    α: Type ?u.17454

β: Type ?u.17457

γ: Type ?u.17460

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝²: IsTrichotomous β s

inst✝¹: IsIrrefl β s

inst✝: IsWellFounded α r

f, g: r ≼i s

f = gexact exists_congr: ∀ {α : Sort ?u.17783} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃ a, p a) ↔ ∃ a, q a)
exists_congr fun x: ?m.17797
x => and_congr_left: ∀ {c a b : Prop}, (c → (a ↔ b)) → (a ∧ c ↔ b ∧ c)
and_congr_left fun hx: ?m.17805
hx => IH: ?m.17614
IH _: α
_ hx: ?m.17805
hx ▸ Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
Goals accomplished! 🐙⟩
#align initial_seg.subsingleton_of_trichotomous_of_irrefl InitialSeg.subsingleton_of_trichotomous_of_irrefl: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrichotomous β s] [inst : IsIrrefl β s]
  [inst : IsWellFounded α r], Subsingleton (r ≼i s)
InitialSeg.subsingleton_of_trichotomous_of_irrefl

instance: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s], Subsingleton (r ≼i s)
instance [IsWellOrder: (α : Type ?u.17932) → (α → α → Prop) → Prop
IsWellOrder β: Type ?u.17908
β s: β → β → Prop
s] : Subsingleton: Sort ?u.17937 → Prop
Subsingleton (r: α → α → Prop
r ≼i s: β → β → Prop
s) :=
  ⟨fun a: ?m.17962
a => by
Goals accomplished! 🐙 α: Type ?u.17905

β: Type ?u.17908

γ: Type ?u.17911

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

a: r ≼i s

∀ (b : r ≼i s), a = blet _ := a: r ≼i s
a.isWellFounded: ∀ {α : Type ?u.17994} {β : Type ?u.17995} {r : α → α → Prop} {s : β → β → Prop},
  r ↪r s → ∀ [inst : IsWellFounded β s], IsWellFounded α r
isWellFoundedα: Type ?u.17905

β: Type ?u.17908

γ: Type ?u.17911

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

a: r ≼i s

x✝:= RelEmbedding.isWellFounded a.toRelEmbedding: IsWellFounded α r

∀ (b : r ≼i s), a = b;α: Type ?u.17905

β: Type ?u.17908

γ: Type ?u.17911

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

a: r ≼i s

x✝:= RelEmbedding.isWellFounded a.toRelEmbedding: IsWellFounded α r

∀ (b : r ≼i s), a = b α: Type ?u.17905

β: Type ?u.17908

γ: Type ?u.17911

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

a: r ≼i s

∀ (b : r ≼i s), a = bexact Subsingleton.elim: ∀ {α : Sort ?u.18051} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim a: r ≼i s
a
Goals accomplished! 🐙⟩

protected theorem eq: ∀ [inst : IsWellOrder β s] (f g : r ≼i s) (a : α), ↑f a = ↑g a
eq [IsWellOrder: (α : Type ?u.18226) → (α → α → Prop) → Prop
IsWellOrder β: Type ?u.18202
β s: β → β → Prop
s] (f: r ≼i s
f g: r ≼i s
g : r: α → α → Prop
r ≼i s: β → β → Prop
s) (a: ?m.18267
a) : f: r ≼i s
f a: ?m.18267
a = g: r ≼i s
g a: ?m.18267
a := by
Goals accomplished! 🐙
  α: Type u_2

β: Type u_1

γ: Type ?u.18205

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f, g: r ≼i s

a: α

↑f a = ↑g arw [α: Type u_2

β: Type u_1

γ: Type ?u.18205

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f, g: r ≼i s

a: α

↑f a = ↑g aSubsingleton.elim: ∀ {α : Sort ?u.18490} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim f: r ≼i s
f g: r ≼i s
gα: Type u_2

β: Type u_1

γ: Type ?u.18205

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f, g: r ≼i s

a: α

↑g a = ↑g a]
Goals accomplished! 🐙
#align initial_seg.eq InitialSeg.eq: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f g : r ≼i s) (a : α),
  ↑f a = ↑g a
InitialSeg.eq

theorem Antisymm.aux: ∀ [inst : IsWellOrder α r] (f : r ≼i s) (g : s ≼i r), LeftInverse ↑g ↑f
Antisymm.aux [IsWellOrder: (α : Type ?u.18591) → (α → α → Prop) → Prop
IsWellOrder α: Type ?u.18564
α r: α → α → Prop
r] (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (g: s ≼i r
g : s: β → β → Prop
s ≼i r: α → α → Prop
r) : LeftInverse: {α : Sort ?u.18633} → {β : Sort ?u.18632} → (β → α) → (α → β) → Prop
LeftInverse g: s ≼i r
g f: r ≼i s
f :=
  InitialSeg.eq: ∀ {α : Type ?u.18877} {β : Type ?u.18876} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f g : r ≼i s)
  (a : α), ↑f a = ↑g a
InitialSeg.eq (f: r ≼i s
f.trans: {α : Type ?u.18885} →
  {β : Type ?u.18884} →
    {γ : Type ?u.18883} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≼i s → s ≼i t → r ≼i t
trans g: s ≼i r
g) (InitialSeg.refl: {α : Type ?u.18950} → (r : α → α → Prop) → r ≼i r
InitialSeg.refl _: ?m.18951 → ?m.18951 → Prop
_)
#align initial_seg.antisymm.aux InitialSeg.Antisymm.aux: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] (f : r ≼i s)
  (g : s ≼i r), LeftInverse ↑g ↑f
InitialSeg.Antisymm.aux

/-- If we have order embeddings between `α` and `β` whose images are initial segments, and `β`
is a well-order then `α` and `β` are order-isomorphic. -/
def antisymm: [inst : IsWellOrder β s] → r ≼i s → s ≼i r → r ≃r s
antisymm [IsWellOrder: (α : Type ?u.19007) → (α → α → Prop) → Prop
IsWellOrder β: Type ?u.18983
β s: β → β → Prop
s] (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (g: s ≼i r
g : s: β → β → Prop
s ≼i r: α → α → Prop
r) : r: α → α → Prop
r ≃r s: β → β → Prop
s :=
  haveI := f: r ≼i s
f.toRelEmbedding: {α : Type ?u.19071} → {β : Type ?u.19070} → {r : α → α → Prop} → {s : β → β → Prop} → r ≼i s → r ↪r s
toRelEmbedding.isWellOrder: ∀ {α : Type ?u.19088} {β : Type ?u.19089} {r : α → α → Prop} {s : β → β → Prop},
  r ↪r s → ∀ [inst : IsWellOrder β s], IsWellOrder α r
isWellOrder
  ⟨⟨f: r ≼i s
f, g: s ≼i r
g, Antisymm.aux: ∀ {α : Type ?u.19377} {β : Type ?u.19378} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] (f : r ≼i s)
  (g : s ≼i r), LeftInverse ↑g ↑f
Antisymm.aux f: r ≼i s
f g: s ≼i r
g, Antisymm.aux: ∀ {α : Type ?u.19413} {β : Type ?u.19414} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] (f : r ≼i s)
  (g : s ≼i r), LeftInverse ↑g ↑f
Antisymm.aux g: s ≼i r
g f: r ≼i s
f⟩, f: r ≼i s
f.map_rel_iff': ∀ {α : Type ?u.19458} {β : Type ?u.19457} {r : α → α → Prop} {s : β → β → Prop} (self : r ↪r s) {a b : α},
  s (↑self.toEmbedding a) (↑self.toEmbedding b) ↔ r a b
map_rel_iff'⟩
#align initial_seg.antisymm InitialSeg.antisymm: {α : Type u_1} →
  {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → [inst : IsWellOrder β s] → r ≼i s → s ≼i r → r ≃r s
InitialSeg.antisymm

@[simp]
theorem antisymm_toFun: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ≼i s)
  (g : s ≼i r), ↑(antisymm f g) = ↑f
antisymm_toFun [IsWellOrder: (α : Type ?u.19650) → (α → α → Prop) → Prop
IsWellOrder β: Type ?u.19626
β s: β → β → Prop
s] (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (g: s ≼i r
g : s: β → β → Prop
s ≼i r: α → α → Prop
r) : (antisymm: {α : Type ?u.19696} →
  {β : Type ?u.19695} → {r : α → α → Prop} → {s : β → β → Prop} → [inst : IsWellOrder β s] → r ≼i s → s ≼i r → r ≃r s
antisymm f: r ≼i s
f g: s ≼i r
g : α: Type ?u.19623
α → β: Type ?u.19626
β) = f: r ≼i s
f :=
  rfl: ∀ {α : Sort ?u.20160} {a : α}, a = a
rfl
#align initial_seg.antisymm_to_fun InitialSeg.antisymm_toFun: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ≼i s)
  (g : s ≼i r), ↑(antisymm f g) = ↑f
InitialSeg.antisymm_toFun

@[simp]
theorem antisymm_symm: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r]
  [inst_1 : IsWellOrder β s] (f : r ≼i s) (g : s ≼i r), RelIso.symm (antisymm f g) = antisymm g f
antisymm_symm [IsWellOrder: (α : Type ?u.20251) → (α → α → Prop) → Prop
IsWellOrder α: Type ?u.20224
α r: α → α → Prop
r] [IsWellOrder: (α : Type ?u.20256) → (α → α → Prop) → Prop
IsWellOrder β: Type ?u.20227
β s: β → β → Prop
s] (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (g: s ≼i r
g : s: β → β → Prop
s ≼i r: α → α → Prop
r) :
    (antisymm: {α : Type ?u.20299} →
  {β : Type ?u.20298} → {r : α → α → Prop} → {s : β → β → Prop} → [inst : IsWellOrder β s] → r ≼i s → s ≼i r → r ≃r s
antisymm f: r ≼i s
f g: s ≼i r
g).symm: {α : Type ?u.20344} → {β : Type ?u.20343} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → s ≃r r
symm = antisymm: {α : Type ?u.20367} →
  {β : Type ?u.20366} → {r : α → α → Prop} → {s : β → β → Prop} → [inst : IsWellOrder β s] → r ≼i s → s ≼i r → r ≃r s
antisymm g: s ≼i r
g f: r ≼i s
f :=
  RelIso.coe_fn_injective: ∀ {α : Type ?u.20409} {β : Type ?u.20410} {r : α → α → Prop} {s : β → β → Prop}, Injective fun f => ↑f
RelIso.coe_fn_injective rfl: ∀ {α : Sort ?u.20432} {a : α}, a = a
rfl
#align initial_seg.antisymm_symm InitialSeg.antisymm_symm: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r]
  [inst_1 : IsWellOrder β s] (f : r ≼i s) (g : s ≼i r), RelIso.symm (antisymm f g) = antisymm g f
InitialSeg.antisymm_symm

theorem eq_or_principal: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ≼i s),
  Surjective ↑f ∨ ∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x
eq_or_principal [IsWellOrder: (α : Type ?u.20519) → (α → α → Prop) → Prop
IsWellOrder β: Type ?u.20495
β s: β → β → Prop
s] (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) :
    Surjective: {α : Sort ?u.20543} → {β : Sort ?u.20542} → (α → β) → Prop
Surjective f: r ≼i s
f ∨ ∃ b: ?m.20667
b, ∀ x: ?m.20670
x, s: β → β → Prop
s x: ?m.20670
x b: ?m.20667
b ↔ ∃ y: ?m.20676
y, f: r ≼i s
f y: ?m.20676
y = x: ?m.20670
x :=
  or_iff_not_imp_right: ∀ {a b : Prop}, a ∨ b ↔ ¬b → a
or_iff_not_imp_right.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun h: ?m.20794
h b: ?m.20797
b =>
    Acc.recOn: ∀ {α : Sort ?u.20799} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort ?u.20800} {a : α} (t : Acc r a),
  (∀ (x : α) (h : ∀ (y : α), r y x → Acc r y),
      (∀ (y : α) (a : r y x), motive y (_ : Acc r y)) → motive x (_ : Acc r x)) →
    motive a t
Acc.recOn (IsWellFounded.wf: ∀ {α : Type ?u.20837} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded r
IsWellFounded.wf.apply: ∀ {α : Sort ?u.20864} {r : α → α → Prop}, WellFounded r → ∀ (a : α), Acc r a
apply b: ?m.20797
b : Acc: {α : Sort ?u.20829} → (α → α → Prop) → α → Prop
Acc s: β → β → Prop
s b: ?m.20797
b) fun x: ?m.20931
x _: ?m.20934
_ IH: ?m.20939
IH =>
      not_forall_not: ∀ {α : Sort ?u.20943} {p : α → Prop}, (¬∀ (x : α), ¬p x) ↔ ∃ x, p x
not_forall_not.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 fun hn: ?m.20955
hn =>
        h: ?m.20794
h
          ⟨x: ?m.20931
x, fun y: ?m.20973
y =>
            ⟨IH: ?m.20939
IH _: β
_, fun ⟨a: α
a, e: ↑f a = y
e⟩ => by
Goals accomplished! 🐙
              α: Type u_2

β: Type u_1

γ: Type ?u.20498

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f: r ≼i s

h: ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x

b, x: β

x✝¹: ∀ (y : β), s y x → Acc s y

IH: ∀ (y : β), s y x → ∃ a, ↑f a = y

hn: ∀ (x_1 : α), ¬↑f x_1 = x

y: β

x✝: ∃ y_1, ↑f y_1 = y

a: α

e: ↑f a = y

s y xrw [α: Type u_2

β: Type u_1

γ: Type ?u.20498

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f: r ≼i s

h: ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x

b, x: β

x✝¹: ∀ (y : β), s y x → Acc s y

IH: ∀ (y : β), s y x → ∃ a, ↑f a = y

hn: ∀ (x_1 : α), ¬↑f x_1 = x

y: β

x✝: ∃ y_1, ↑f y_1 = y

a: α

e: ↑f a = y

s y x← e: ↑f a = y
eα: Type u_2

β: Type u_1

γ: Type ?u.20498

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f: r ≼i s

h: ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x

b, x: β

x✝¹: ∀ (y : β), s y x → Acc s y

IH: ∀ (y : β), s y x → ∃ a, ↑f a = y

hn: ∀ (x_1 : α), ¬↑f x_1 = x

y: β

x✝: ∃ y_1, ↑f y_1 = y

a: α

e: ↑f a = y

s (↑f a) x]α: Type u_2

β: Type u_1

γ: Type ?u.20498

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f: r ≼i s

h: ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x

b, x: β

x✝¹: ∀ (y : β), s y x → Acc s y

IH: ∀ (y : β), s y x → ∃ a, ↑f a = y

hn: ∀ (x_1 : α), ¬↑f x_1 = x

y: β

x✝: ∃ y_1, ↑f y_1 = y

a: α

e: ↑f a = y

s (↑f a) x;α: Type u_2

β: Type u_1

γ: Type ?u.20498

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f: r ≼i s

h: ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x

b, x: β

x✝¹: ∀ (y : β), s y x → Acc s y

IH: ∀ (y : β), s y x → ∃ a, ↑f a = y

hn: ∀ (x_1 : α), ¬↑f x_1 = x

y: β

x✝: ∃ y_1, ↑f y_1 = y

a: α

e: ↑f a = y

s (↑f a) x
                α: Type u_2

β: Type u_1

γ: Type ?u.20498

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

inst✝: IsWellOrder β s

f: r ≼i s

h: ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x

b, x: β

x✝¹: ∀ (y : β), s y x → Acc s y

IH: ∀ (y : β), s y x → ∃ a, ↑f a = y

hn: ∀ (x_1 : α), ¬↑f x_1 = x

y: β

x✝: ∃ y_1, ↑f y_1 = y

a: α

e: ↑f a = y

s y xexact
                  (trichotomous: ∀ {α : Type ?u.21172} {r : α → α → Prop} [inst : IsTrichotomous α r] (a b : α), r a b ∨ a = b ∨ r b a
trichotomous _: ?m.21173
_ _: ?m.21173
_).resolve_right: ∀ {a b : Prop}, a ∨ b → ¬b → a
resolve_right
                    (not_or_of_not: ∀ {a b : Prop}, ¬a → ¬b → ¬(a ∨ b)
not_or_of_not (hn: ∀ (x_1 : α), ¬↑f x_1 = x
hn a: α
a) fun hl: ?m.21215
hl => not_exists: ∀ {α : Sort ?u.21217} {p : α → Prop}, (¬∃ x, p x) ↔ ∀ (x : α), ¬p x
not_exists.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hn: ∀ (x_1 : α), ¬↑f x_1 = x
hn (f: r ≼i s
f.init: ∀ {α : Type ?u.21228} {β : Type ?u.21229} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) → ∃ a', ↑f a' = b
init hl: ?m.21215
hl))
Goals accomplished! 🐙⟩⟩
#align initial_seg.eq_or_principal InitialSeg.eq_or_principal: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ≼i s),
  Surjective ↑f ∨ ∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x
InitialSeg.eq_or_principal

/-- Restrict the codomain of an initial segment -/
def codRestrict: {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} → {s : β → β → Prop} → (p : Set β) → (f : r ≼i s) → (∀ (a : α), ↑f a ∈ p) → r ≼i Subrel s p
codRestrict (p: Set β
p : Set: Type ?u.21373 → Type ?u.21373
Set β: Type ?u.21349
β) (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (H: ∀ (a : α), ↑f a ∈ p
H : ∀ a: ?m.21395
a, f: r ≼i s
f a: ?m.21395
a ∈ p: Set β
p) : r: α → α → Prop
r ≼i Subrel: {α : Type ?u.21554} → (α → α → Prop) → (p : Set α) → ↑p → ↑p → Prop
Subrel s: β → β → Prop
s p: Set β
p :=
  ⟨RelEmbedding.codRestrict: {α : Type ?u.21594} →
  {β : Type ?u.21593} →
    {r : α → α → Prop} → {s : β → β → Prop} → (p : Set β) → (f : r ↪r s) → (∀ (a : α), ↑f a ∈ p) → r ↪r Subrel s p
RelEmbedding.codRestrict p: Set β
p f: r ≼i s
f H: ∀ (a : α), ↑f a ∈ p
H, fun a: ?m.21726
a ⟨b: β
b, m: b ∈ p
m⟩ h: ?m.21732
h =>
    let ⟨a': α
a', e: ↑f a' = ↑{ val := b, property := m }
e⟩ := f: r ≼i s
f.init: ∀ {α : Type ?u.21830} {β : Type ?u.21831} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) → ∃ a', ↑f a' = b
init h: Subrel s p { val := b, property := m } (↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a)
h
    ⟨a': α
a', by
Goals accomplished! 🐙 α: Type ?u.21346

β: Type ?u.21349

γ: Type ?u.21352

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

p: Set β

f: r ≼i s

H: ∀ (a : α), ↑f a ∈ p

a: α

x✝: ↑p

b: β

m: b ∈ p

h: Subrel s p { val := b, property := m } (↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a)

a': α

e: ↑f a' = ↑{ val := b, property := m }

↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a' = { val := b, property := m }subst e: ↑f a' = ↑{ val := b, property := m }
eα: Type ?u.21346

β: Type ?u.21349

γ: Type ?u.21352

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

p: Set β

f: r ≼i s

H: ∀ (a : α), ↑f a ∈ p

a: α

x✝: ↑p

a': α

m: ↑f a' ∈ p

h: Subrel s p { val := ↑f a', property := m } (↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a)

↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a' = { val := ↑f a', property := m };α: Type ?u.21346

β: Type ?u.21349

γ: Type ?u.21352

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

p: Set β

f: r ≼i s

H: ∀ (a : α), ↑f a ∈ p

a: α

x✝: ↑p

a': α

m: ↑f a' ∈ p

h: Subrel s p { val := ↑f a', property := m } (↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a)

↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a' = { val := ↑f a', property := m } α: Type ?u.21346

β: Type ?u.21349

γ: Type ?u.21352

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

p: Set β

f: r ≼i s

H: ∀ (a : α), ↑f a ∈ p

a: α

x✝: ↑p

b: β

m: b ∈ p

h: Subrel s p { val := b, property := m } (↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a)

a': α

e: ↑f a' = ↑{ val := b, property := m }

↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a' = { val := b, property := m }rfl
Goals accomplished! 🐙⟩⟩
#align initial_seg.cod_restrict InitialSeg.codRestrict: {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} → {s : β → β → Prop} → (p : Set β) → (f : r ≼i s) → (∀ (a : α), ↑f a ∈ p) → r ≼i Subrel s p
InitialSeg.codRestrict

@[simp]
theorem codRestrict_apply: ∀ (p : Set β) (f : r ≼i s) (H : ∀ (a : α), ↑f a ∈ p) (a : α),
  ↑(codRestrict p f H) a = { val := ↑f a, property := (_ : ↑f a ∈ p) }
codRestrict_apply (p: ?m.22557
p) (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (H: ∀ (a : α), ↑f a ∈ p
H a: α
a) : codRestrict: {α : Type ?u.22586} →
  {β : Type ?u.22585} →
    {r : α → α → Prop} → {s : β → β → Prop} → (p : Set β) → (f : r ≼i s) → (∀ (a : α), ↑f a ∈ p) → r ≼i Subrel s p
codRestrict p: ?m.22557
p f: r ≼i s
f H: ?m.22578
H a: ?m.22581
a = ⟨f: r ≼i s
f a: ?m.22581
a, H: ?m.22578
H a: ?m.22581
a⟩ :=
  rfl: ∀ {α : Sort ?u.22841} {a : α}, a = a
rfl
#align initial_seg.cod_restrict_apply InitialSeg.codRestrict_apply: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : r ≼i s) (H : ∀ (a : α), ↑f a ∈ p)
  (a : α), ↑(codRestrict p f H) a = { val := ↑f a, property := (_ : ↑f a ∈ p) }
InitialSeg.codRestrict_apply

/-- Initial segment from an empty type. -/
def ofIsEmpty: {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → [inst : IsEmpty α] → r ≼i s
ofIsEmpty (r: α → α → Prop
r : α: Type ?u.22927
α → α: Type ?u.22927
α → Prop: Type
Prop) (s: β → β → Prop
s : β: Type ?u.22930
β → β: Type ?u.22930
β → Prop: Type
Prop) [IsEmpty: Sort ?u.22966 → Prop
IsEmpty α: Type ?u.22927
α] : r: α → α → Prop
r ≼i s: β → β → Prop
s :=
  ⟨RelEmbedding.ofIsEmpty: {α : Type ?u.23014} → {β : Type ?u.23013} → (r : α → α → Prop) → (s : β → β → Prop) → [inst : IsEmpty α] → r ↪r s
RelEmbedding.ofIsEmpty r: α → α → Prop
r s: β → β → Prop
s, isEmptyElim: ∀ {α : Sort ?u.23041} [inst : IsEmpty α] {p : α → Sort ?u.23040} (a : α), p a
isEmptyElim⟩
#align initial_seg.of_is_empty InitialSeg.ofIsEmpty: {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → [inst : IsEmpty α] → r ≼i s
InitialSeg.ofIsEmpty

/-- Initial segment embedding of an order `r` into the disjoint union of `r` and `s`. -/
def leAdd: {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → r ≼i Sum.Lex r s
leAdd (r: α → α → Prop
r : α: Type ?u.23176
α → α: Type ?u.23176
α → Prop: Type
Prop) (s: β → β → Prop
s : β: Type ?u.23179
β → β: Type ?u.23179
β → Prop: Type
Prop) : r: α → α → Prop
r ≼i Sum.Lex: {α : Type ?u.23226} → {β : Type ?u.23225} → (α → α → Prop) → (β → β → Prop) → α ⊕ β → α ⊕ β → Prop
Sum.Lex r: α → α → Prop
r s: β → β → Prop
s :=
  ⟨⟨⟨Sum.inl: {α : Type ?u.23315} → {β : Type ?u.23314} → α → α ⊕ β
Sum.inl, fun _: ?m.23322
_ _: ?m.23325
_ => Sum.inl.inj: ∀ {α : Type ?u.23328} {β : Type ?u.23327} {val val_1 : α}, Sum.inl val = Sum.inl val_1 → val = val_1
Sum.inl.inj⟩, Sum.lex_inl_inl: ∀ {α : Type ?u.23352} {β : Type ?u.23351} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α},
  Sum.Lex r s (Sum.inl a₁) (Sum.inl a₂) ↔ r a₁ a₂
Sum.lex_inl_inl⟩, fun a: ?m.23380
a b: ?m.23383
b => by
Goals accomplished! 🐙
    α: Type ?u.23176

β: Type ?u.23179

γ: Type ?u.23182

r✝: α → α → Prop

s✝: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

s: β → β → Prop

a: α

b: α ⊕ β

Sum.Lex r s b
    (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
          map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
      a) →
  ∃ a',
    ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a' =       bcases b: α ⊕ β
bα: Type ?u.23176

β: Type ?u.23179

γ: Type ?u.23182

r✝: α → α → Prop

s✝: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

s: β → β → Prop

a, val✝: α

inlSum.Lex r s (Sum.inl val✝)
    (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
          map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
      a) →
  ∃ a',
    ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a' =       Sum.inl val✝
α: Type ?u.23176

β: Type ?u.23179

γ: Type ?u.23182

r✝: α → α → Prop

s✝: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

s: β → β → Prop

a: α

val✝: β

inrSum.Lex r s (Sum.inr val✝)
    (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
          map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
      a) →
  ∃ a',
    ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a' =       Sum.inr val✝ <;> [α: Type ?u.23176

β: Type ?u.23179

γ: Type ?u.23182

r✝: α → α → Prop

s✝: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

s: β → β → Prop

a: α

b: α ⊕ β

Sum.Lex r s b
    (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
          map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
      a) →
  ∃ a',
    ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a' =       bexact fun _: ?m.23474
_ => ⟨_: ?m.23481
_, rfl: ∀ {α : Sort ?u.23486} {a : α}, a = a
rfl⟩
Goals accomplished! 🐙; α: Type ?u.23176

β: Type ?u.23179

γ: Type ?u.23182

r✝: α → α → Prop

s✝: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

s: β → β → Prop

a: α

b: α ⊕ β

Sum.Lex r s b
    (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
          map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
      a) →
  ∃ a',
    ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a' =       bexact False.elim: ∀ {C : Sort ?u.23502}, False → C
False.elim ∘ Sum.lex_inr_inl: ∀ {α : Type ?u.23508} {β : Type ?u.23507} {r : α → α → Prop} {s : β → β → Prop} {a : α} {b : β},
  ¬Sum.Lex r s (Sum.inr b) (Sum.inl a)
Sum.lex_inr_inl
Goals accomplished! 🐙]
Goals accomplished! 🐙⟩
#align initial_seg.le_add InitialSeg.leAdd: {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → r ≼i Sum.Lex r s
InitialSeg.leAdd

@[simp]
theorem leAdd_apply: ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (a : α), ↑(leAdd r s) a = Sum.inl a
leAdd_apply (r: α → α → Prop
r : α: Type ?u.23708
α → α: Type ?u.23708
α → Prop: Type
Prop) (s: β → β → Prop
s : β: Type ?u.23711
β → β: Type ?u.23711
β → Prop: Type
Prop) (a: ?m.23747
a) : leAdd: {α : Type ?u.23752} → {β : Type ?u.23751} → (r : α → α → Prop) → (s : β → β → Prop) → r ≼i Sum.Lex r s
leAdd r: α → α → Prop
r s: β → β → Prop
s a: ?m.23747
a = Sum.inl: {α : Type ?u.23892} → {β : Type ?u.23891} → α → α ⊕ β
Sum.inl a: ?m.23747
a :=
  rfl: ∀ {α : Sort ?u.23936} {a : α}, a = a
rfl
#align initial_seg.le_add_apply InitialSeg.leAdd_apply: ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (a : α), ↑(leAdd r s) a = Sum.inl a
InitialSeg.leAdd_apply

protected theorem acc: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) (a : α), Acc r a ↔ Acc s (↑f a)
acc (f: r ≼i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) (a: α
a : α: Type ?u.23999
α) : Acc: {α : Sort ?u.24046} → (α → α → Prop) → α → Prop
Acc r: α → α → Prop
r a: α
a ↔ Acc: {α : Sort ?u.24054} → (α → α → Prop) → α → Prop
Acc s: β → β → Prop
s (f: r ≼i s
f a: α
a) :=
  ⟨by
Goals accomplished! 🐙
    α: Type u_1

β: Type u_2

γ: Type ?u.24005

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

a: α

Acc r a → Acc s (↑f a)refine' fun h: ?m.24248
h => Acc.recOn: ∀ {α : Sort ?u.24250} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort ?u.24251} {a : α} (t : Acc r a),
  (∀ (x : α) (h : ∀ (y : α), r y x → Acc r y),
      (∀ (y : α) (a : r y x), motive y (_ : Acc r y)) → motive x (_ : Acc r x)) →
    motive a t
Acc.recOn h: ?m.24248
h fun a: ?m.24293
a _: ?m.24296
_ ha: ?m.24301
ha => Acc.intro: ∀ {α : Sort ?u.24305} {r : α → α → Prop} (x : α), (∀ (y : α), r y x → Acc r y) → Acc r x
Acc.intro _: ?m.24306
_ fun b: ?m.24312
b hb: ?m.24315
hb => _: Acc ?m.24307 b
_α: Type u_1

β: Type u_2

γ: Type ?u.24005

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

a✝: α

h: Acc r a✝

a: α

x✝: ∀ (y : α), r y a → Acc r y

ha: ∀ (y : α), r y a → Acc s (↑f y)

b: β

hb: s b (↑f a)

Acc s b
    α: Type u_1

β: Type u_2

γ: Type ?u.24005

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

a: α

Acc r a → Acc s (↑f a)obtain ⟨a', rfl⟩: ∃ a', ↑f a' = b
⟨a': α
a'⟨a', rfl⟩: ∃ a', ↑f a' = b
, rfl: ↑f a' = b
rfl⟨a', rfl⟩: ∃ a', ↑f a' = b
⟩ := f: r ≼i s
f.init: ∀ {α : Type ?u.24331} {β : Type ?u.24332} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) → ∃ a', ↑f a' = b
init hb: ?m.24315
hbα: Type u_1

β: Type u_2

γ: Type ?u.24005

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

a✝: α

h: Acc r a✝

a: α

x✝: ∀ (y : α), r y a → Acc r y

ha: ∀ (y : α), r y a → Acc s (↑f y)

a': α

hb: s (↑f a') (↑f a)

introAcc s (↑f a')
    α: Type u_1

β: Type u_2

γ: Type ?u.24005

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≼i s

a: α

Acc r a → Acc s (↑f a)exact ha: ?m.24301
ha _: α
_ (f: r ≼i s
f.map_rel_iff: ∀ {α : Type ?u.24418} {β : Type ?u.24419} {r : α → α → Prop} {s : β → β → Prop} {a b : α} (f : r ≼i s),
  s (↑f a) (↑f b) ↔ r a b
map_rel_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp hb: s (↑f a') (↑f a)
hb)
Goals accomplished! 🐙, f: r ≼i s
f.toRelEmbedding: {α : Type ?u.24191} → {β : Type ?u.24190} → {r : α → α → Prop} → {s : β → β → Prop} → r ≼i s → r ↪r s
toRelEmbedding.acc: ∀ {α : Type ?u.24208} {β : Type ?u.24209} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (a : α),
  Acc s (↑f a) → Acc r a
acc a: α
a⟩
#align initial_seg.acc InitialSeg.acc: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) (a : α), Acc r a ↔ Acc s (↑f a)
InitialSeg.acc

end InitialSeg

/-!
### Principal segments

Order embeddings whose range is a principal segment of `s` (i.e., an interval of the form
`(-∞, top)` for some element `top` of `β`). The type of these embeddings from `r` to `s` is called
`PrincipalSeg r s`, and denoted by `r ≺i s`. Principal segments are in particular initial
segments.
-/


/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≺i s` is an order
embedding whose range is an open interval `(-∞, top)` for some element `top` of `β`. Such order
embeddings are called principal segments -/
structure PrincipalSeg: {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        (toRelEmbedding : r ↪r s) → (top : β) → (∀ (b : β), s b top ↔ ∃ a, ↑toRelEmbedding a = b) → PrincipalSeg r s
PrincipalSeg {α: Type ?u.24493
α β: Type ?u.24496
β : Type _: Type (?u.24493+1)
Type _} (r: α → α → Prop
r : α: Type ?u.24493
α → α: Type ?u.24493
α → Prop: Type
Prop) (s: β → β → Prop
s : β: Type ?u.24496
β → β: Type ?u.24496
β → Prop: Type
Prop) extends r: α → α → Prop
r ↪r s: β → β → Prop
s where
  /-- The supremum of the principal segment -/
  top: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → PrincipalSeg r s → β
top : β: Type ?u.24496
β
  /-- The image of the order embedding is the set of elements `b` such that `s b top` -/
  down': ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (self : PrincipalSeg r s) (b : β),
  s b self.top ↔ ∃ a, ↑self.toRelEmbedding a = b
down' : ∀ b: ?m.24538
b, s: β → β → Prop
s b: ?m.24538
b top: β
top ↔ ∃ a: ?m.24544
a, toRelEmbedding: r ↪r s
toRelEmbedding a: ?m.24544
a = b: ?m.24538
b
#align principal_seg PrincipalSeg: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)
PrincipalSeg

-- Porting notes: deleted `scoped[InitialSeg]`
/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≺i s` is an order
embedding whose range is an open interval `(-∞, top)` for some element `top` of `β`. Such order
embeddings are called principal segments -/
infixl:25 " ≺i " => PrincipalSeg: {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → Type (maxu_1u_2)
PrincipalSeg

namespace PrincipalSeg

instance: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → CoeOut (r ≺i s) (r ↪r s)
instance : CoeOut: Sort ?u.33440 → semiOutParam (Sort ?u.33439) → Sort (max(max1?u.33440)?u.33439)
CoeOut (r: α → α → Prop
r ≺i s: β → β → Prop
s) (r: α → α → Prop
r ↪r s: β → β → Prop
s) :=
  ⟨PrincipalSeg.toRelEmbedding: {α : Type ?u.33484} → {β : Type ?u.33483} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → r ↪r s
PrincipalSeg.toRelEmbedding⟩

instance: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → CoeFun (r ≺i s) fun x => α → β
instance : CoeFun: (α : Sort ?u.33762) → outParam (α → Sort ?u.33761) → Sort (max(max1?u.33762)?u.33761)
CoeFun (r: α → α → Prop
r ≺i s: β → β → Prop
s) fun _: ?m.33780
_ => α: Type ?u.33734
α → β: Type ?u.33737
β :=
  ⟨fun f: ?m.33815
f => f: ?m.33815
f⟩

@[simp]
theorem coe_fn_mk: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (t : β)
  (o : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b), ↑{ toRelEmbedding := f, top := t, down' := o }.toRelEmbedding = ↑f
coe_fn_mk (f: r ↪r s
f : r: α → α → Prop
r ↪r s: β → β → Prop
s) (t: β
t o: ?m.34517
o) : (@PrincipalSeg.mk: {α : Type ?u.34525} →
  {β : Type ?u.34524} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        (toRelEmbedding : r ↪r s) → (top : β) → (∀ (b : β), s b top ↔ ∃ a, ↑toRelEmbedding a = b) → r ≺i s
PrincipalSeg.mk _: Type ?u.34525
_ _: Type ?u.34524
_ r: α → α → Prop
r s: β → β → Prop
s f: r ↪r s
f t: ?m.34514
t o: ?m.34517
o : α: Type ?u.34469
α → β: Type ?u.34472
β) = f: r ↪r s
f :=
  rfl: ∀ {α : Sort ?u.35020} {a : α}, a = a
rfl
#align principal_seg.coe_fn_mk PrincipalSeg.coe_fn_mk: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (t : β)
  (o : ∀ (b : β), s b t ↔ ∃ a, ↑f a = b), ↑{ toRelEmbedding := f, top := t, down' := o }.toRelEmbedding = ↑f
PrincipalSeg.coe_fn_mk

theorem down: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) {b : β},
  s b f.top ↔ ∃ a, ↑f.toRelEmbedding a = b
down (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) : ∀ {b: β
b : β: Type ?u.35091
β}, s: β → β → Prop
s b: β
b f: r ≺i s
f.top: {α : Type ?u.35137} → {β : Type ?u.35136} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top ↔ ∃ a: ?m.35157
a, f: r ≺i s
f a: ?m.35157
a = b: β
b :=
  f: r ≺i s
f.down': ∀ {α : Type ?u.35213} {β : Type ?u.35212} {r : α → α → Prop} {s : β → β → Prop} (self : r ≺i s) (b : β),
  s b self.top ↔ ∃ a, ↑self.toRelEmbedding a = b
down' _: ?m.35215
_
#align principal_seg.down PrincipalSeg.down: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) {b : β},
  s b f.top ↔ ∃ a, ↑f.toRelEmbedding a = b
PrincipalSeg.down

theorem lt_top: ∀ (f : r ≺i s) (a : α), s (↑f.toRelEmbedding a) f.top
lt_top (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) (a: α
a : α: Type ?u.35251
α) : s: β → β → Prop
s (f: r ≺i s
f a: α
a) f: r ≺i s
f.top: {α : Type ?u.35352} → {β : Type ?u.35351} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top :=
  f: r ≺i s
f.down: ∀ {α : Type ?u.35364} {β : Type ?u.35365} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) {b : β},
  s b f.top ↔ ∃ a, ↑f.toRelEmbedding a = b
down.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨_: ?m.35394
_, rfl: ∀ {α : Sort ?u.35402} {a : α}, a = a
rfl⟩
#align principal_seg.lt_top PrincipalSeg.lt_top: ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) (a : α),
  s (↑f.toRelEmbedding a) f.top
PrincipalSeg.lt_top

theorem init: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s) {a : α} {b : β},
  s b (↑f.toRelEmbedding a) → ∃ a', ↑f.toRelEmbedding a' = b
init [IsTrans: (α : Type ?u.35458) → (α → α → Prop) → Prop
IsTrans β: Type ?u.35434
β s: β → β → Prop
s] (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) {a: α
a : α: Type ?u.35431
α} {b: β
b : β: Type ?u.35434
β} (h: s b (↑f.toRelEmbedding a)
h : s: β → β → Prop
s b: β
b (f: r ≺i s
f a: α
a)) : ∃ a': ?m.35543
a', f: r ≺i s
f a': ?m.35543
a' = b: β
b :=
  f: r ≺i s
f.down: ∀ {α : Type ?u.35589} {β : Type ?u.35590} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) {b : β},
  s b f.top ↔ ∃ a, ↑f.toRelEmbedding a = b
down.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 <| _root_.trans: ∀ {α : Type ?u.35619} {r : α → α → Prop} [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
_root_.trans h: s b (↑f.toRelEmbedding a)
h <| f: r ≺i s
f.lt_top: ∀ {α : Type ?u.35654} {β : Type ?u.35655} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) (a : α),
  s (↑f.toRelEmbedding a) f.top
lt_top _: ?m.35662
_
#align principal_seg.init PrincipalSeg.init: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s) {a : α} {b : β},
  s b (↑f.toRelEmbedding a) → ∃ a', ↑f.toRelEmbedding a' = b
PrincipalSeg.init

/-- A principal segment is in particular an initial segment. -/
instance hasCoeInitialSeg: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → [inst : IsTrans β s] → Coe (r ≺i s) (r ≼i s)
hasCoeInitialSeg [IsTrans: (α : Type ?u.35734) → (α → α → Prop) → Prop
IsTrans β: Type ?u.35710
β s: β → β → Prop
s] : Coe: semiOutParam (Sort ?u.35740) → Sort ?u.35739 → Sort (max(max1?u.35740)?u.35739)
Coe (r: α → α → Prop
r ≺i s: β → β → Prop
s) (r: α → α → Prop
r ≼i s: β → β → Prop
s) :=
  ⟨fun f: ?m.35785
f => ⟨f: ?m.35785
f.toRelEmbedding: {α : Type ?u.35812} → {β : Type ?u.35811} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → r ↪r s
toRelEmbedding, fun _: ?m.35838
_ _: ?m.35841
_ => f: ?m.35785
f.init: ∀ {α : Type ?u.35844} {β : Type ?u.35843} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s)
  {a : α} {b : β}, s b (↑f.toRelEmbedding a) → ∃ a', ↑f.toRelEmbedding a' = b
init⟩⟩
#align principal_seg.has_coe_initial_seg PrincipalSeg.hasCoeInitialSeg: {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → [inst : IsTrans β s] → Coe (r ≺i s) (r ≼i s)
PrincipalSeg.hasCoeInitialSeg

theorem coe_coe_fn': ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s),
  ↑{ toRelEmbedding := f.toRelEmbedding,
        init' := (_ : ∀ (x : α) (x_1 : β), s x_1 (↑f.toRelEmbedding x) → ∃ a', ↑f.toRelEmbedding a' = x_1) } =     ↑f.toRelEmbedding
coe_coe_fn' [IsTrans: (α : Type ?u.36046) → (α → α → Prop) → Prop
IsTrans β: Type ?u.36022
β s: β → β → Prop
s] (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) : ((f: r ≺i s
f : r: α → α → Prop
r ≼i s: β → β → Prop
s) : α: Type ?u.36019
α → β: Type ?u.36022
β) = f: r ≺i s
f :=
  rfl: ∀ {α : Sort ?u.36735} {a : α}, a = a
rfl
#align principal_seg.coe_coe_fn' PrincipalSeg.coe_coe_fn': ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s),
  ↑{ toRelEmbedding := f.toRelEmbedding,
        init' := (_ : ∀ (x : α) (x_1 : β), s x_1 (↑f.toRelEmbedding x) → ∃ a', ↑f.toRelEmbedding a' = x_1) } =     ↑f.toRelEmbedding
PrincipalSeg.coe_coe_fn'

theorem init_iff: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s) {a : α} {b : β},
  s b (↑f.toRelEmbedding a) ↔ ∃ a', ↑f.toRelEmbedding a' = b ∧ r a' a
init_iff [IsTrans: (α : Type ?u.36787) → (α → α → Prop) → Prop
IsTrans β: Type ?u.36763
β s: β → β → Prop
s] (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) {a: α
a : α: Type ?u.36760
α} {b: β
b : β: Type ?u.36763
β} : s: β → β → Prop
s b: β
b (f: r ≺i s
f a: α
a) ↔ ∃ a': ?m.36870
a', f: r ≺i s
f a': ?m.36870
a' = b: β
b ∧ r: α → α → Prop
r a': ?m.36870
a' a: α
a :=
  @InitialSeg.init_iff: ∀ {α : Type ?u.36915} {β : Type ?u.36916} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) ↔ ∃ a', ↑f a' = b ∧ r a' a
InitialSeg.init_iff α: Type ?u.36760
α β: Type ?u.36763
β r: α → α → Prop
r s: β → β → Prop
s f: r ≺i s
f a: α
a b: β
b
#align principal_seg.init_iff PrincipalSeg.init_iff: ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsTrans β s] (f : r ≺i s) {a : α} {b : β},
  s b (↑f.toRelEmbedding a) ↔ ∃ a', ↑f.toRelEmbedding a' = b ∧ r a' a
PrincipalSeg.init_iff

theorem irrefl: ∀ {r : α → α → Prop} [inst : IsWellOrder α r], r ≺i r → False
irrefl {r: α → α → Prop
r : α: Type ?u.37081
α → α: Type ?u.37081
α → Prop: Type
Prop} [IsWellOrder: (α : Type ?u.37114) → (α → α → Prop) → Prop
IsWellOrder α: Type ?u.37081
α r: α → α → Prop
r] (f: r ≺i r
f : r: α → α → Prop
r ≺i r: α → α → Prop
r) : False: Prop
False := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.37084

γ: Type ?u.37087

r✝: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

inst✝: IsWellOrder α r

f: r ≺i r

Falsehave h: ?m.37144
h := f: r ≺i r
f.lt_top: ∀ {α : Type ?u.37145} {β : Type ?u.37146} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) (a : α),
  s (↑f.toRelEmbedding a) f.top
lt_top f: r ≺i r
f.top: {α : Type ?u.37170} → {β : Type ?u.37169} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
topα: Type u_1

β: Type ?u.37084

γ: Type ?u.37087

r✝: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

inst✝: IsWellOrder α r

f: r ≺i r

h: r (↑f.toRelEmbedding f.top) f.top

False
  α: Type u_1

β: Type ?u.37084

γ: Type ?u.37087

r✝: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

inst✝: IsWellOrder α r

f: r ≺i r

Falserw [α: Type u_1

β: Type ?u.37084

γ: Type ?u.37087

r✝: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

inst✝: IsWellOrder α r

f: r ≺i r

h: r (↑f.toRelEmbedding f.top) f.top

Falseshow f: r ≺i r
f f: r ≺i r
f.top: {α : Type ?u.37229} → {β : Type ?u.37228} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top = f: r ≺i r
f.top: {α : Type ?u.37239} → {β : Type ?u.37238} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top from InitialSeg.eq: ∀ {α : Type ?u.37253} {β : Type ?u.37252} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f g : r ≼i s)
  (a : α), ↑f a = ↑g a
InitialSeg.eq (↑f: r ≺i r
f) (InitialSeg.refl: {α : Type ?u.37359} → (r : α → α → Prop) → r ≼i r
InitialSeg.refl r: α → α → Prop
r) f: r ≺i r
f.top: {α : Type ?u.37388} → {β : Type ?u.37387} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
topα: Type u_1

β: Type ?u.37084

γ: Type ?u.37087

r✝: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

inst✝: IsWellOrder α r

f: r ≺i r

h: r f.top f.top

False]α: Type u_1

β: Type ?u.37084

γ: Type ?u.37087

r✝: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

inst✝: IsWellOrder α r

f: r ≺i r

h: r f.top f.top

False at h: ?m.37144
hα: Type u_1

β: Type ?u.37084

γ: Type ?u.37087

r✝: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

inst✝: IsWellOrder α r

f: r ≺i r

h: r f.top f.top

False
  α: Type u_1

β: Type ?u.37084

γ: Type ?u.37087

r✝: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

r: α → α → Prop

inst✝: IsWellOrder α r

f: r ≺i r

Falseexact _root_.irrefl: ∀ {α : Type ?u.37603} {r : α → α → Prop} [inst : IsIrrefl α r] (a : α), ¬r a a
_root_.irrefl _: ?m.37604
_ h: r f.top f.top
h
Goals accomplished! 🐙
#align principal_seg.irrefl PrincipalSeg.irrefl: ∀ {α : Type u_1} {r : α → α → Prop} [inst : IsWellOrder α r], r ≺i r → False
PrincipalSeg.irrefl

instance: ∀ {α : Type u_1} (r : α → α → Prop) [inst : IsWellOrder α r], IsEmpty (r ≺i r)
instance (r: α → α → Prop
r : α: Type ?u.37695
α → α: Type ?u.37695
α → Prop: Type
Prop) [IsWellOrder: (α : Type ?u.37728) → (α → α → Prop) → Prop
IsWellOrder α: Type ?u.37695
α r: α → α → Prop
r] : IsEmpty: Sort ?u.37733 → Prop
IsEmpty (r: α → α → Prop
r ≺i r: α → α → Prop
r) :=
  ⟨fun f: ?m.37759
f => f: ?m.37759
f.irrefl: ∀ {α : Type ?u.37761} {r : α → α → Prop} [inst : IsWellOrder α r], r ≺i r → False
irrefl⟩

/-- Composition of a principal segment with an initial segment, as a principal segment -/
def ltLe: r ≺i s → s ≼i t → r ≺i t
ltLe (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) (g: s ≼i t
g : s: β → β → Prop
s ≼i t: γ → γ → Prop
t) : r: α → α → Prop
r ≺i t: γ → γ → Prop
t :=
  ⟨@RelEmbedding.trans: {α : Type ?u.37927} →
  {β : Type ?u.37926} →
    {γ : Type ?u.37925} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r t
RelEmbedding.trans _: Type ?u.37927
_ _: Type ?u.37926
_ _: Type ?u.37925
_ r: α → α → Prop
r s: β → β → Prop
s t: γ → γ → Prop
t f: r ≺i s
f g: s ≼i t
g, g: s ≼i t
g f: r ≺i s
f.top: {α : Type ?u.38556} → {β : Type ?u.38555} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top, fun a: ?m.38574
a => by
Goals accomplished! 🐙
    α: Type ?u.37818

β: Type ?u.37821

γ: Type ?u.37824

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≺i s

g: s ≼i t

a: γ

t a (↑g f.top) ↔ ∃ a_1, ↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a_1 = asimp only [g: s ≼i t
g.init_iff: ∀ {α : Type ?u.38595} {β : Type ?u.38596} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s) {a : α} {b : β},
  s b (↑f a) ↔ ∃ a', ↑f a' = b ∧ r a' a
init_iff, PrincipalSeg.down: ∀ {α : Type ?u.38652} {β : Type ?u.38653} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) {b : β},
  s b f.top ↔ ∃ a, ↑f.toRelEmbedding a = b
PrincipalSeg.down, exists_and_left: ∀ {α : Sort ?u.38677} {p : α → Prop} {b : Prop}, (∃ x, b ∧ p x) ↔ b ∧ ∃ x, p x
exists_and_left.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm, exists_swap: ∀ {α : Sort ?u.38713} {β : Sort ?u.38712} {p : α → β → Prop}, (∃ x y, p x y) ↔ ∃ y x, p x y
exists_swap,
        RelEmbedding.trans_apply: ∀ {α : Type ?u.38729} {β : Type ?u.38730} {γ : Type ?u.38731} {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, exists_eq_right': ∀ {α : Sort ?u.38781} {p : α → Prop} {a' : α}, (∃ a, p a ∧ a' = a) ↔ p a'
exists_eq_right', InitialSeg.coe_coe_fn: ∀ {α : Type ?u.38799} {β : Type ?u.38800} {r : α → α → Prop} {s : β → β → Prop} (f : r ≼i s), ↑f.toRelEmbedding = ↑f
InitialSeg.coe_coe_fn]
Goals accomplished! 🐙⟩
#align principal_seg.lt_le PrincipalSeg.ltLe: {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≺i s → s ≼i t → r ≺i t
PrincipalSeg.ltLe

@[simp]
theorem lt_le_apply: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i s)
  (g : s ≼i t) (a : α), ↑(ltLe f g).toRelEmbedding a = ↑g (↑f.toRelEmbedding a)
lt_le_apply (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) (g: s ≼i t
g : s: β → β → Prop
s ≼i t: γ → γ → Prop
t) (a: α
a : α: Type ?u.42811
α) : (f: r ≺i s
f.ltLe: {α : Type ?u.42879} →
  {β : Type ?u.42878} →
    {γ : Type ?u.42877} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≺i s → s ≼i t → r ≺i t
ltLe g: s ≼i t
g) a: α
a = g: s ≼i t
g (f: r ≺i s
f a: α
a) :=
  RelEmbedding.trans_apply: ∀ {α : Type ?u.43136} {β : Type ?u.43137} {γ : Type ?u.43138} {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 _: ?m.43142 ↪r ?m.43143
_ _: ?m.43143 ↪r ?m.43144
_ _: ?m.43139
_
#align principal_seg.lt_le_apply PrincipalSeg.lt_le_apply: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i s)
  (g : s ≼i t) (a : α), ↑(ltLe f g).toRelEmbedding a = ↑g (↑f.toRelEmbedding a)
PrincipalSeg.lt_le_apply

@[simp]
theorem lt_le_top: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i s)
  (g : s ≼i t), (ltLe f g).top = ↑g f.top
lt_le_top (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) (g: s ≼i t
g : s: β → β → Prop
s ≼i t: γ → γ → Prop
t) : (f: r ≺i s
f.ltLe: {α : Type ?u.43369} →
  {β : Type ?u.43368} →
    {γ : Type ?u.43367} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≺i s → s ≼i t → r ≺i t
ltLe g: s ≼i t
g).top: {α : Type ?u.43415} → {β : Type ?u.43414} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top = g: s ≼i t
g f: r ≺i s
f.top: {α : Type ?u.43541} → {β : Type ?u.43540} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top :=
  rfl: ∀ {α : Sort ?u.43554} {a : α}, a = a
rfl
#align principal_seg.lt_le_top PrincipalSeg.lt_le_top: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≺i s)
  (g : s ≼i t), (ltLe f g).top = ↑g f.top
PrincipalSeg.lt_le_top

/-- Composition of two principal segments as a principal segment -/
@[trans]
protected def trans: [inst : IsTrans γ t] → r ≺i s → s ≺i t → r ≺i t
trans [IsTrans: (α : Type ?u.43632) → (α → α → Prop) → Prop
IsTrans γ: Type ?u.43611
γ t: γ → γ → Prop
t] (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) (g: s ≺i t
g : s: β → β → Prop
s ≺i t: γ → γ → Prop
t) : r: α → α → Prop
r ≺i t: γ → γ → Prop
t :=
  ltLe: {α : Type ?u.43695} →
  {β : Type ?u.43694} →
    {γ : Type ?u.43693} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≺i s → s ≼i t → r ≺i t
ltLe f: r ≺i s
f g: s ≺i t
g
#align principal_seg.trans PrincipalSeg.trans: {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → [inst : IsTrans γ t] → r ≺i s → s ≺i t → r ≺i t
PrincipalSeg.trans

@[simp]
theorem trans_apply: ∀ [inst : IsTrans γ t] (f : r ≺i s) (g : s ≺i t) (a : α),
  ↑(PrincipalSeg.trans f g).toRelEmbedding a = ↑g.toRelEmbedding (↑f.toRelEmbedding a)
trans_apply [IsTrans: (α : Type ?u.44007) → (α → α → Prop) → Prop
IsTrans γ: Type ?u.43986
γ t: γ → γ → Prop
t] (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) (g: s ≺i t
g : s: β → β → Prop
s ≺i t: γ → γ → Prop
t) (a: α
a : α: Type ?u.43980
α) : (f: r ≺i s
f.trans: {α : Type ?u.44053} →
  {β : Type ?u.44052} →
    {γ : Type ?u.44051} →
      {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → [inst : IsTrans γ t] → r ≺i s → s ≺i t → r ≺i t
trans g: s ≺i t
g) a: α
a = g: s ≺i t
g (f: r ≺i s
f a: α
a) :=
  lt_le_apply: ∀ {α : Type ?u.44265} {β : Type ?u.44266} {γ : Type ?u.44267} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  (f : r ≺i s) (g : s ≼i t) (a : α), ↑(ltLe f g).toRelEmbedding a = ↑g (↑f.toRelEmbedding a)
lt_le_apply _: ?m.44271 ≺i ?m.44272
_ _: ?m.44272 ≼i ?m.44273
_ _: ?m.44268
_
#align principal_seg.trans_apply PrincipalSeg.trans_apply: ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_1} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [inst : IsTrans γ t] (f : r ≺i s) (g : s ≺i t) (a : α),
  ↑(PrincipalSeg.trans f g).toRelEmbedding a = ↑g.toRelEmbedding (↑f.toRelEmbedding a)
PrincipalSeg.trans_apply

@[simp]
theorem trans_top: ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_1} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [inst : IsTrans γ t] (f : r ≺i s) (g : s ≺i t), (PrincipalSeg.trans f g).top = ↑g.toRelEmbedding f.top
trans_top [IsTrans: (α : Type ?u.44453) → (α → α → Prop) → Prop
IsTrans γ: Type ?u.44432
γ t: γ → γ → Prop
t] (f: r ≺i s
f : r: α → α → Prop
r ≺i s: β → β → Prop
s) (g: s ≺i t
g : s: β → β → Prop
s ≺i t: γ → γ → Prop
t) : (f: r ≺i s
f.trans: {α : Type ?u.44497} →
  {β : Type ?u.44496} →
    {γ : Type ?u.44495} →
      {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → [inst : IsTrans γ t] → r ≺i s → s ≺i t → r ≺i t
trans g: s ≺i t
g).top: {α : Type ?u.44560} → {β : Type ?u.44559} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top = g: s ≺i t
g f: r ≺i s
f.top: {α : Type ?u.44623} → {β : Type ?u.44622} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top :=
  rfl: ∀ {α : Sort ?u.44637} {a : α}, a = a
rfl
#align principal_seg.trans_top PrincipalSeg.trans_top: ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_1} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [inst : IsTrans γ t] (f : r ≺i s) (g : s ≺i t), (PrincipalSeg.trans f g).top = ↑g.toRelEmbedding f.top
PrincipalSeg.trans_top

/-- Composition of an order isomorphism with a principal segment, as a principal segment -/
def equivLT: r ≃r s → s ≺i t → r ≺i t
equivLT (f: r ≃r s
f : r: α → α → Prop
r ≃r s: β → β → Prop
s) (g: s ≺i t
g : s: β → β → Prop
s ≺i t: γ → γ → Prop
t) : r: α → α → Prop
r ≺i t: γ → γ → Prop
t :=
  ⟨@RelEmbedding.trans: {α : Type ?u.44803} →
  {β : Type ?u.44802} →
    {γ : Type ?u.44801} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r t
RelEmbedding.trans _: Type ?u.44803
_ _: Type ?u.44802
_ _: Type ?u.44801
_ r: α → α → Prop
r s: β → β → Prop
s t: γ → γ → Prop
t f: r ≃r s
f g: s ≺i t
g, g: s ≺i t
g.top: {α : Type ?u.45587} → {β : Type ?u.45586} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top, fun c: ?m.45605
c =>
    suffices (∃ a: β
a : β: Type ?u.44697
β, g: s ≺i t
g a: β
a = c: ?m.45605
c) ↔ ∃ a: α
a : α: Type ?u.44694
α, g: s ≺i t
g (f: r ≃r s
f a: α
a) = c: ?m.45605
c by simpa [PrincipalSeg.down: ∀ {α : Type ?u.46713} {β : Type ?u.46714} {r : α → α → Prop} {s : β → β → Prop} (f : r ≺i s) {b : β},
  s b f.top ↔ ∃ a, ↑f.toRelEmbedding a = b
PrincipalSeg.down]
Goals accomplished! 🐙
    ⟨fun ⟨b: β
b, h: ↑g.toRelEmbedding b = c
h⟩ => ⟨f: r ≃r s
f.symm: {α : Type ?u.45847} → {β : Type ?u.45846} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → s ≃r r
symm b: β
b, by
Goals accomplished! 🐙 α: Type ?u.44694

β: Type ?u.44697

γ: Type ?u.44700

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≃r s

g: s ≺i t

c: γ

x✝: ∃ a, ↑g.toRelEmbedding a = c

b: β

h: ↑g.toRelEmbedding b = c

↑g.toRelEmbedding (↑f (↑(RelIso.symm f) b)) = csimp only [h: ↑g.toRelEmbedding b = c
h, RelIso.apply_symm_apply: ∀ {α : Type ?u.46351} {β : Type ?u.46352} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : β),
  ↑e (↑(RelIso.symm e) x) = x
RelIso.apply_symm_apply]
Goals accomplished! 🐙⟩,
      fun ⟨a: α
a, h: ↑g.toRelEmbedding (↑f a) = c
h⟩ => ⟨f: r ≃r s
f a: α
a, h: ↑g.toRelEmbedding (↑f a) = c
h⟩⟩⟩
#align principal_seg.equiv_lt PrincipalSeg.equivLT: {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≃r s → s ≺i t → r ≺i t
PrincipalSeg.equivLT

/-- Composition of a principal segment with an order isomorphism, as a principal segment -/
def ltEquiv: {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ≺i s → s ≃r t → r ≺i t
ltEquiv {r: α → α → Prop
r : α: Type ?u.54748
α → α: Type ?u.54748
α → Prop: Type
Prop} {s: β → β → Prop
s : β: Type ?u.54751
β → β: Type ?u.54751
β → Prop: Type
Prop} {t: γ → γ → Prop
t : γ: Type ?u.54754
γ → γ: Type ?u.54754
γ → Prop: Type
Prop} (f: r ≺i s
f : PrincipalSeg: {α : Type ?u.54794} → {β : Type ?u.54793} → (α → α → Prop) → (β → β → Prop) → Type (max?u.54794?u.54793)
PrincipalSeg r: α → α → Prop
r s: β → β → Prop
s)
    (g: s ≃r t
g : s: β → β → Prop
s ≃r t: γ → γ → Prop
t) : PrincipalSeg: {α : Type ?u.54830} → {β : Type ?u.54829} → (α → α → Prop) → (β → β → Prop) → Type (max?u.54830?u.54829)
PrincipalSeg r: α → α → Prop
r t: γ → γ → Prop
t :=
  ⟨@RelEmbedding.trans: {α : Type ?u.54878} →
  {β : Type ?u.54877} →
    {γ : Type ?u.54876} → {r : α → α → Prop} → {s : β → β → Prop} → {t : γ → γ → Prop} → r ↪r s → s ↪r t → r ↪r t
RelEmbedding.trans _: Type ?u.54878
_ _: Type ?u.54877
_ _: Type ?u.54876
_ r: α → α → Prop
r s: β → β → Prop
s t: γ → γ → Prop
t f: r ≺i s
f g: s ≃r t
g, g: s ≃r t
g f: r ≺i s
f.top: {α : Type ?u.55698} → {β : Type ?u.55697} → {r : α → α → Prop} → {s : β → β → Prop} → r ≺i s → β
top, by
Goals accomplished! 🐙
    α: Type ?u.54748

β: Type ?u.54751

γ: Type ?u.54754

r✝: α → α → Prop

s✝: β → β → Prop

t✝: γ → γ → Prop

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≺i s

g: s ≃r t

∀ (b : γ), t b (↑g f.top) ↔ ∃ a, ↑(RelEmbedding.trans f.toRelEmbedding (RelIso.toRelEmbedding g)) a = bintro x: γ
xα: Type ?u.54748

β: Type ?u.54751

γ: Type ?u.54754

r✝: α → α → Prop

s✝: β → β → Prop

t✝: γ → γ → Prop

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≺i s

g: s ≃r t

x: γ

t x (↑g f.top) ↔ ∃ a, ↑(RelEmbedding.trans f.toRelEmbedding (RelIso.toRelEmbedding g)) a = x
    α: Type ?u.54748

β: Type ?u.54751

γ: Type ?u.54754

r✝: α → α → Prop

s✝: β → β → Prop

t✝: γ → γ → Prop

r: α → α → Prop

s: β → β → Prop

t: γ → γ → Prop

f: r ≺i s

g: s ≃r t

∀ (b : γ), t b (↑g f.top) ↔ ∃ a, ↑(RelEmbedding.trans f.toRelEmbedding (