/-
Copyright (c) 2019 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Minchao Wu

! This file was ported from Lean 3 source module data.prod.lex
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.BoundedOrder

/-!
# Lexicographic order

This file defines the lexicographic relation for pairs of orders, partial orders and linear orders.

## Main declarations

* `Prod.Lex.Order`: Instances lifting the orders on `α` and `β` to `α ×ₗ β`.

## Notation

* `α ×ₗ β`: `α × β` equipped with the lexicographic order

## See also

Related files are:
* `Data.Finset.CoLex`: Colexicographic order on finite sets.
* `Data.List.Lex`: Lexicographic order on lists.
* `Data.Pi.Lex`: Lexicographic order on `Πₗ i, α i`.
* `Data.PSigma.Order`: Lexicographic order on `Σ' i, α i`.
* `Data.Sigma.Order`: Lexicographic order on `Σ i, α i`.
-/


variable {α: Type ?u.18603
α β: Type ?u.2470
β γ: Type ?u.8
γ : Type _: Type (?u.2470+1)
Type _}

namespace Prod.Lex

-- porting note: `Prod.Lex` is not protected in core, hence the `_root_.` prefix
-- This will be fixed in nightly-2022-11-30
@[inherit_doc] notation:35 α: ?m.2608
α " ×ₗ " β: ?m.2599
β:34 => _root_.Lex: Type u_1 → Type u_1
_root_.Lex (Prod: Type u → Type v → Type (maxuv)
Prod α: ?m.3905
α β: ?m.148
β)

instance decidableEq: (α : Type ?u.14110) → (β : Type ?u.14113) → [inst : DecidableEq α] → [inst : DecidableEq β] → DecidableEq (Lex (α × β))
decidableEq (α: Type ?u.14110
α β: Type ?u.14113
β : Type _: Type (?u.14110+1)
Type _) [DecidableEq: Sort ?u.14116 → Sort (max1?u.14116)
DecidableEq α: Type ?u.14110
α] [DecidableEq: Sort ?u.14125 → Sort (max1?u.14125)
DecidableEq β: Type ?u.14113
β] : DecidableEq: Sort ?u.14134 → Sort (max1?u.14134)
DecidableEq (α: Type ?u.14110
α ×ₗ β: Type ?u.14113
β) :=
  instDecidableEqProd: {α : Type ?u.14158} → {β : Type ?u.14157} → [inst : DecidableEq α] → [inst : DecidableEq β] → DecidableEq (α × β)
instDecidableEqProd
#align prod.lex.decidable_eq Prod.Lex.decidableEq: (α : Type u_1) → (β : Type u_2) → [inst : DecidableEq α] → [inst : DecidableEq β] → DecidableEq (Lex (α × β))
Prod.Lex.decidableEq

instance inhabited: (α : Type ?u.14483) → (β : Type ?u.14486) → [inst : Inhabited α] → [inst : Inhabited β] → Inhabited (Lex (α × β))
inhabited (α: Type ?u.14483
α β: Type ?u.14486
β : Type _: Type (?u.14486+1)
Type _) [Inhabited: Sort ?u.14489 → Sort (max1?u.14489)
Inhabited α: Type ?u.14483
α] [Inhabited: Sort ?u.14492 → Sort (max1?u.14492)
Inhabited β: Type ?u.14486
β] : Inhabited: Sort ?u.14495 → Sort (max1?u.14495)
Inhabited (α: Type ?u.14483
α ×ₗ β: Type ?u.14486
β) :=
  instInhabitedProd: {α : Type ?u.14505} → {β : Type ?u.14504} → [inst : Inhabited α] → [inst : Inhabited β] → Inhabited (α × β)
instInhabitedProd
#align prod.lex.inhabited Prod.Lex.inhabited: (α : Type u_1) → (β : Type u_2) → [inst : Inhabited α] → [inst : Inhabited β] → Inhabited (Lex (α × β))
Prod.Lex.inhabited

/-- Dictionary / lexicographic ordering on pairs.  -/
instance instLE: (α : Type u_1) → (β : Type u_2) → [inst : LT α] → [inst : LE β] → LE (Lex (α × β))
instLE (α: Type ?u.14794
α β: Type ?u.14797
β : Type _: Type (?u.14797+1)
Type _) [LT: Type ?u.14800 → Type ?u.14800
LT α: Type ?u.14794
α] [LE: Type ?u.14803 → Type ?u.14803
LE β: Type ?u.14797
β] : LE: Type ?u.14806 → Type ?u.14806
LE (α: Type ?u.14794
α ×ₗ β: Type ?u.14797
β) where le := Prod.Lex: {α : Type ?u.14819} → {β : Type ?u.14818} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
Prod.Lex (· < ·): α → α → Prop
(· < ·) (· ≤ ·): β → β → Prop
(· ≤ ·)
#align prod.lex.has_le Prod.Lex.instLE: (α : Type u_1) → (β : Type u_2) → [inst : LT α] → [inst : LE β] → LE (Lex (α × β))
Prod.Lex.instLE

instance instLT: (α : Type ?u.14948) → (β : Type ?u.14951) → [inst : LT α] → [inst : LT β] → LT (Lex (α × β))
instLT (α: Type ?u.14948
α β: Type ?u.14951
β : Type _: Type (?u.14948+1)
Type _) [LT: Type ?u.14954 → Type ?u.14954
LT α: Type ?u.14948
α] [LT: Type ?u.14957 → Type ?u.14957
LT β: Type ?u.14951
β] : LT: Type ?u.14960 → Type ?u.14960
LT (α: Type ?u.14948
α ×ₗ β: Type ?u.14951
β) where lt := Prod.Lex: {α : Type ?u.14973} → {β : Type ?u.14972} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
Prod.Lex (· < ·): α → α → Prop
(· < ·) (· < ·): β → β → Prop
(· < ·)
#align prod.lex.has_lt Prod.Lex.instLT: (α : Type u_1) → (β : Type u_2) → [inst : LT α] → [inst : LT β] → LT (Lex (α × β))
Prod.Lex.instLT

theorem le_iff: ∀ [inst : LT α] [inst_1 : LE β] (a b : α × β), ↑toLex a ≤ ↑toLex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd ≤ b.snd
le_iff [LT: Type ?u.15103 → Type ?u.15103
LT α: Type ?u.15094
α] [LE: Type ?u.15106 → Type ?u.15106
LE β: Type ?u.15097
β] (a: α × β
a b: α × β
b : α: Type ?u.15094
α × β: Type ?u.15097
β) :
    toLex: {α : Type ?u.15118} → α ≃ Lex α
toLex a: α × β
a ≤ toLex: {α : Type ?u.15183} → α ≃ Lex α
toLex b: α × β
b ↔ a: α × β
a.1: {α : Type ?u.15273} → {β : Type ?u.15272} → α × β → α
1 < b: α × β
b.1: {α : Type ?u.15277} → {β : Type ?u.15276} → α × β → α
1 ∨ a: α × β
a.1: {α : Type ?u.15286} → {β : Type ?u.15285} → α × β → α
1 = b: α × β
b.1: {α : Type ?u.15290} → {β : Type ?u.15289} → α × β → α
1 ∧ a: α × β
a.2: {α : Type ?u.15296} → {β : Type ?u.15295} → α × β → β
2 ≤ b: α × β
b.2: {α : Type ?u.15300} → {β : Type ?u.15299} → α × β → β
2 :=
  Prod.lex_def: ∀ {α : Type ?u.15312} {β : Type ?u.15313} (r : α → α → Prop) (s : β → β → Prop) {p q : α × β},
  Prod.Lex r s p q ↔ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
Prod.lex_def (· < ·): α → α → Prop
(· < ·) (· ≤ ·): β → β → Prop
(· ≤ ·)
#align prod.lex.le_iff Prod.Lex.le_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LE β] (a b : α × β),
  ↑toLex a ≤ ↑toLex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd ≤ b.snd
Prod.Lex.le_iff

theorem lt_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] (a b : α × β),
  ↑toLex a < ↑toLex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd < b.snd
lt_iff [LT: Type ?u.15499 → Type ?u.15499
LT α: Type ?u.15490
α] [LT: Type ?u.15502 → Type ?u.15502
LT β: Type ?u.15493
β] (a: α × β
a b: α × β
b : α: Type ?u.15490
α × β: Type ?u.15493
β) :
    toLex: {α : Type ?u.15514} → α ≃ Lex α
toLex a: α × β
a < toLex: {α : Type ?u.15579} → α ≃ Lex α
toLex b: α × β
b ↔ a: α × β
a.1: {α : Type ?u.15669} → {β : Type ?u.15668} → α × β → α
1 < b: α × β
b.1: {α : Type ?u.15673} → {β : Type ?u.15672} → α × β → α
1 ∨ a: α × β
a.1: {α : Type ?u.15682} → {β : Type ?u.15681} → α × β → α
1 = b: α × β
b.1: {α : Type ?u.15686} → {β : Type ?u.15685} → α × β → α
1 ∧ a: α × β
a.2: {α : Type ?u.15692} → {β : Type ?u.15691} → α × β → β
2 < b: α × β
b.2: {α : Type ?u.15696} → {β : Type ?u.15695} → α × β → β
2 :=
  Prod.lex_def: ∀ {α : Type ?u.15708} {β : Type ?u.15709} (r : α → α → Prop) (s : β → β → Prop) {p q : α × β},
  Prod.Lex r s p q ↔ r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd
Prod.lex_def (· < ·): α → α → Prop
(· < ·) (· < ·): β → β → Prop
(· < ·)
#align prod.lex.lt_iff Prod.Lex.lt_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] (a b : α × β),
  ↑toLex a < ↑toLex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd < b.snd
Prod.Lex.lt_iff

example: ∀ {α : Type u_1} {β : Type u_2} (x : α) (y : β), ↑toLex (x, y) = ↑toLex (x, y)
example (x: α
x : α: Type ?u.15877
α) (y: β
y : β: Type ?u.15880
β) : toLex: {α : Type ?u.15891} → α ≃ Lex α
toLex (x: α
x, y: β
y) = toLex: {α : Type ?u.15960} → α ≃ Lex α
toLex (x: α
x, y: β
y) := rfl: ∀ {α : Sort ?u.16033} {a : α}, a = a
rfl

/-- Dictionary / lexicographic preorder for pairs. -/
instance preorder: (α : Type ?u.16056) → (β : Type ?u.16059) → [inst : Preorder α] → [inst : Preorder β] → Preorder (Lex (α × β))
preorder (α: Type ?u.16056
α β: Type ?u.16059
β : Type _: Type (?u.16056+1)
Type _) [Preorder: Type ?u.16062 → Type ?u.16062
Preorder α: Type ?u.16056
α] [Preorder: Type ?u.16065 → Type ?u.16065
Preorder β: Type ?u.16059
β] : Preorder: Type ?u.16068 → Type ?u.16068
Preorder (α: Type ?u.16056
α ×ₗ β: Type ?u.16059
β) :=
  { Prod.Lex.instLE: (α : Type ?u.16080) → (β : Type ?u.16079) → [inst : LT α] → [inst : LE β] → LE (Lex (α × β))
Prod.Lex.instLE α: Type ?u.16056
α β: Type ?u.16059
β, Prod.Lex.instLT: (α : Type ?u.16106) → (β : Type ?u.16105) → [inst : LT α] → [inst : LT β] → LT (Lex (α × β))
Prod.Lex.instLT α: Type ?u.16056
α β: Type ?u.16059
β with
    le_refl := refl_of: ∀ {α : Type ?u.16148} (r : α → α → Prop) [inst : IsRefl α r] (a : α), r a a
refl_of <| Prod.Lex: {α : Type ?u.16151} → {β : Type ?u.16150} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
Prod.Lex _: ?m.16152 → ?m.16152 → Prop
_ _: ?m.16153 → ?m.16153 → Prop
_,
    le_trans := fun _: ?m.16304
_ _: ?m.16307
_ _: ?m.16310
_ => trans_of: ∀ {α : Type ?u.16312} (r : α → α → Prop) [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
trans_of <| Prod.Lex: {α : Type ?u.16315} → {β : Type ?u.16314} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
Prod.Lex _: ?m.16316 → ?m.16316 → Prop
_ _: ?m.16317 → ?m.16317 → Prop
_,
    lt_iff_le_not_le := fun x₁: ?m.16492
x₁ x₂: ?m.16495
x₂ =>
      match x₁: ?m.16492
x₁, x₂: ?m.16495
x₂ with
      | (a₁: α
a₁, b₁: β
b₁), (a₂: α
a₂, b₂: β
b₂) => by
Goals accomplished! 🐙
        α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

(a₁, b₁) < (a₂, b₂) ↔ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)constructorα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mp(a₁, b₁) < (a₂, b₂) → (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mpr(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) → (a₁, b₁) < (a₂, b₂)
        α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

(a₁, b₁) < (a₂, b₂) ↔ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mp(a₁, b₁) < (a₂, b₂) → (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mp(a₁, b₁) < (a₂, b₂) → (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mpr(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) → (a₁, b₁) < (a₂, b₂)rintro (⟨_, _, hlt⟩ | ⟨_, hlt⟩): ?a
(⟨_, _, hlt⟩ | ⟨_, hlt⟩: ?a
⟨_: β
_⟨_, _, hlt⟩ | ⟨_, hlt⟩: ?a
, _: β
_⟨_, _, hlt⟩ | ⟨_, hlt⟩: ?a
, hlt: a₁ < a₂
hlt⟨_, _, hlt⟩ | ⟨_, hlt⟩: ?a
⟩ | ⟨_: α
_⟨_, _, hlt⟩ | ⟨_, hlt⟩: ?a
, hlt: b₁ < b₂
hlt⟨_, _, hlt⟩ | ⟨_, hlt⟩: ?a
⟩(⟨_, _, hlt⟩ | ⟨_, hlt⟩): ?a
)α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right(a₁, b₁) ≤ (a₁, b₂) ∧ ¬(a₁, b₂) ≤ (a₁, b₁)
          α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mp(a₁, b₁) < (a₂, b₂) → (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right(a₁, b₁) ≤ (a₁, b₂) ∧ ¬(a₁, b₂) ≤ (a₁, b₁)constructorα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.left(a₁, b₁) ≤ (a₂, b₂)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.right¬(a₂, b₂) ≤ (a₁, b₁)
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.left(a₁, b₁) ≤ (a₂, b₂) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.left(a₁, b₁) ≤ (a₂, b₂)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.right¬(a₂, b₂) ≤ (a₁, b₁)exact left: ∀ {α : Type ?u.17006} {β : Type ?u.17005} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β),
  ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
left _: ?m.17008
_ _: ?m.17008
_ hlt: a₁ < a₂
hlt
Goals accomplished! 🐙
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.right¬(a₂, b₂) ≤ (a₁, b₁) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.right¬(a₂, b₂) ≤ (a₁, b₁)rintro ⟨⟩: (a₂, b₂) ≤ (a₁, b₁)
⟨⟩α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

h✝: a₂ < a₁

mp.left.right.leftFalse
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: a₁ < a₁

h✝: b₂ ≤ b₁

mp.left.right.rightFalse
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.right¬(a₂, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

h✝: a₂ < a₁

mp.left.right.leftFalse α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

h✝: a₂ < a₁

mp.left.right.leftFalse
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: a₁ < a₁

h✝: b₂ ≤ b₁

mp.left.right.rightFalseapply lt_asymm: ∀ {α : Type ?u.17304} [inst : Preorder α] {a b : α}, a < b → ¬b < a
lt_asymm hlt: a₁ < a₂
hltα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

h✝: a₂ < a₁

mp.left.right.lefta₂ < a₁;α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

h✝: a₂ < a₁

mp.left.right.lefta₂ < a₁ α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

h✝: a₂ < a₁

mp.left.right.leftFalseassumption
Goals accomplished! 🐙
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

hlt: a₁ < a₂

mp.left.right¬(a₂, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: a₁ < a₁

h✝: b₂ ≤ b₁

mp.left.right.rightFalse α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: a₁ < a₁

h✝: b₂ ≤ b₁

mp.left.right.rightFalseexact lt_irrefl: ∀ {α : Type ?u.17319} [inst : Preorder α] (a : α), ¬a < a
lt_irrefl _: ?m.17320
_ hlt: a₁ < a₁
hlt
Goals accomplished! 🐙
          α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mp(a₁, b₁) < (a₂, b₂) → (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right(a₁, b₁) ≤ (a₁, b₂) ∧ ¬(a₁, b₂) ≤ (a₁, b₁) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right(a₁, b₁) ≤ (a₁, b₂) ∧ ¬(a₁, b₂) ≤ (a₁, b₁)constructorα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.left(a₁, b₁) ≤ (a₁, b₂)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.right¬(a₁, b₂) ≤ (a₁, b₁)
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right(a₁, b₁) ≤ (a₁, b₂) ∧ ¬(a₁, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.left(a₁, b₁) ≤ (a₁, b₂) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.left(a₁, b₁) ≤ (a₁, b₂)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.right¬(a₁, b₂) ≤ (a₁, b₁)rightα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.left.hb₁ ≤ b₂
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.left(a₁, b₁) ≤ (a₁, b₂)rw [α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.left.hb₁ ≤ b₂lt_iff_le_not_le: ∀ {α : Type ?u.17368} [inst : Preorder α] {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a
lt_iff_le_not_leα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁

mp.right.left.hb₁ ≤ b₂]α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁

mp.right.left.hb₁ ≤ b₂ at hlt: b₁ < b₂
hltα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁

mp.right.left.hb₁ ≤ b₂
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.left(a₁, b₁) ≤ (a₁, b₂)exact hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
hlt.1: ∀ {a b : Prop}, a ∧ b → a
1
Goals accomplished! 🐙
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right(a₁, b₁) ≤ (a₁, b₂) ∧ ¬(a₁, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.right¬(a₁, b₂) ≤ (a₁, b₁) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.right¬(a₁, b₂) ≤ (a₁, b₁)rintro ⟨⟩: (a₁, b₂) ≤ (a₁, b₁)
⟨⟩α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: a₁ < a₁

mp.right.right.leftFalse
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: b₂ ≤ b₁

mp.right.right.rightFalse
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.right¬(a₁, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: a₁ < a₁

mp.right.right.leftFalse α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: a₁ < a₁

mp.right.right.leftFalse
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: b₂ ≤ b₁

mp.right.right.rightFalseapply lt_irrefl: ∀ {α : Type ?u.17711} [inst : Preorder α] (a : α), ¬a < a
lt_irrefl a₁: α
a₁α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: a₁ < a₁

mp.right.right.lefta₁ < a₁
                α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: a₁ < a₁

mp.right.right.leftFalseassumption
Goals accomplished! 🐙
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

mp.right.right¬(a₁, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: b₂ ≤ b₁

mp.right.right.rightFalse α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: b₂ ≤ b₁

mp.right.right.rightFalserw [α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: b₂ ≤ b₁

mp.right.right.rightFalselt_iff_le_not_le: ∀ {α : Type ?u.17718} [inst : Preorder α] {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a
lt_iff_le_not_leα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁

h✝: b₂ ≤ b₁

mp.right.right.rightFalse]α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁

h✝: b₂ ≤ b₁

mp.right.right.rightFalse at hlt: b₁ < b₂
hltα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁

h✝: b₂ ≤ b₁

mp.right.right.rightFalse
                α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: b₂ ≤ b₁

mp.right.right.rightFalseapply hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
hlt.2: ∀ {a b : Prop}, a ∧ b → b
2α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁

h✝: b₂ ≤ b₁

mp.right.right.rightb₂ ≤ b₁
                α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

hlt: b₁ < b₂

h✝: b₂ ≤ b₁

mp.right.right.rightFalseassumption
Goals accomplished! 🐙
        α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

(a₁, b₁) < (a₂, b₂) ↔ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mpr(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) → (a₁, b₁) < (a₂, b₂) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mpr(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) → (a₁, b₁) < (a₂, b₂)rintro ⟨⟨⟩, h₂r⟩: ?b
⟨⟨⟩: (a₁, b₁) ≤ (a₂, b₂)
⟨⟩⟨⟨⟩, h₂r⟩: ?b
, h₂r: unknown free variable '_uniq.17788'
h₂r⟨⟨⟩, h₂r⟩: ?b
⟩α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

h₂r: ¬(a₂, b₂) ≤ (a₁, b₁)

h✝: a₁ < a₂

mpr.intro.left(a₁, b₁) < (a₂, b₂)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right(a₁, b₁) < (a₁, b₂)
          α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mpr(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) → (a₁, b₁) < (a₂, b₂)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

h₂r: ¬(a₂, b₂) ≤ (a₁, b₁)

h✝: a₁ < a₂

mpr.intro.left(a₁, b₁) < (a₂, b₂) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

h₂r: ¬(a₂, b₂) ≤ (a₁, b₁)

h✝: a₁ < a₂

mpr.intro.left(a₁, b₁) < (a₂, b₂)
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right(a₁, b₁) < (a₁, b₂)leftα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

h₂r: ¬(a₂, b₂) ≤ (a₁, b₁)

h✝: a₁ < a₂

mpr.intro.left.ha₁ < a₂
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

h₂r: ¬(a₂, b₂) ≤ (a₁, b₁)

h✝: a₁ < a₂

mpr.intro.left(a₁, b₁) < (a₂, b₂)assumption
Goals accomplished! 🐙
          α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁: β

a₂: α

b₂: β

mpr(a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) → (a₁, b₁) < (a₂, b₂)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right(a₁, b₁) < (a₁, b₂) α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right(a₁, b₁) < (a₁, b₂)rightα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.hb₁ < b₂
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right(a₁, b₁) < (a₁, b₂)rw [α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.hb₁ < b₂lt_iff_le_not_le: ∀ {α : Type ?u.18119} [inst : Preorder α] {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a
lt_iff_le_not_leα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.hb₁ ≤ b₂ ∧ ¬b₂ ≤ b₁]α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.hb₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right(a₁, b₁) < (a₁, b₂)constructorα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.leftb₁ ≤ b₂
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.right¬b₂ ≤ b₁
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right(a₁, b₁) < (a₁, b₂)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.leftb₁ ≤ b₂ α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.leftb₁ ≤ b₂
α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.right¬b₂ ≤ b₁assumption
Goals accomplished! 🐙
            α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right(a₁, b₁) < (a₁, b₂)·α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.right¬b₂ ≤ b₁ α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.right¬b₂ ≤ b₁intro h: b₂ ≤ b₁
hα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

h: b₂ ≤ b₁

mpr.intro.right.h.rightFalse
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.right¬b₂ ≤ b₁apply h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)
h₂rα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

h: b₂ ≤ b₁

mpr.intro.right.h.right(a₁, b₂) ≤ (a₁, b₁)
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.right¬b₂ ≤ b₁rightα✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

h: b₂ ≤ b₁

mpr.intro.right.h.right.hb₂ ≤ b₁
              α✝: Type ?u.16047

β✝: Type ?u.16050

γ: Type ?u.16053

α: Type ?u.16056

β: Type ?u.16059

inst✝¹: Preorder α

inst✝: Preorder β

src✝¹:= instLE α β: LE (Lex (α × β))

src✝:= instLT α β: LT (Lex (α × β))

x₁, x₂: Lex (α × β)

a₁: α

b₁, b₂: β

h₂r: ¬(a₁, b₂) ≤ (a₁, b₁)

h✝: b₁ ≤ b₂

mpr.intro.right.h.right¬b₂ ≤ b₁exact h: b₂ ≤ b₁
h
Goals accomplished! 🐙 }
#align prod.lex.preorder Prod.Lex.preorder: (α : Type u_1) → (β : Type u_2) → [inst : Preorder α] → [inst : Preorder β] → Preorder (Lex (α × β))
Prod.Lex.preorder

section Preorder

variable [PartialOrder: Type ?u.18627 → Type ?u.18627
PartialOrder α: Type ?u.18618
α] [Preorder: Type ?u.18630 → Type ?u.18630
Preorder β: Type ?u.18606
β]

-- porting note: type class search sees right through the type synonrm for `α ×ₗ β` and uses the
-- `Preorder` structure for `α × β` instead
-- This is hopefully the same problems as in https://github.com/leanprover/lean4/issues/1891
-- and will be fixed in nightly-2022-11-30
theorem toLex_mono: Monotone ↑toLex
toLex_mono : @Monotone: {α : Type ?u.18634} → {β : Type ?u.18633} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone _: Type ?u.18634
_ _: Type ?u.18633
_ _ (Prod.Lex.preorder: (α : Type ?u.18650) → (β : Type ?u.18649) → [inst : Preorder α] → [inst : Preorder β] → Preorder (Lex (α × β))
Prod.Lex.preorder α: Type ?u.18618
α β: Type ?u.18621
β) (toLex: {α : Type ?u.18679} → α ≃ Lex α
toLex : α: Type ?u.18618
α × β: Type ?u.18621
β → α: Type ?u.18618
α ×ₗ β: Type ?u.18621
β) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

Monotone ↑toLexrintro ⟨a₁, b₁⟩: α × β
⟨a₁: α
a₁⟨a₁, b₁⟩: α × β
, b₁: β
b₁⟨a₁, b₁⟩: α × β
⟩ ⟨a₂, b₂⟩: α × β
⟨a₂: α
a₂⟨a₂, b₂⟩: α × β
, b₂: β
b₂⟨a₂, b₂⟩: α × β
⟩ ⟨ha, hb⟩: (a₁, b₁) ≤ (a₂, b₂)
⟨ha: (a₁, b₁).fst ≤ (a₂, b₂).fst
ha⟨ha, hb⟩: (a₁, b₁) ≤ (a₂, b₂)
, hb: (a₁, b₁).snd ≤ (a₂, b₂).snd
hb⟨ha, hb⟩: (a₁, b₁) ≤ (a₂, b₂)
⟩α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

ha: (a₁, b₁).fst ≤ (a₂, b₂).fst

hb: (a₁, b₁).snd ≤ (a₂, b₂).snd

mk.mk.intro↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
  α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

Monotone ↑toLexobtain: (a₁, b₁).fst = (a₂, b₂).fst ∨ (a₁, b₁).fst < (a₂, b₂).fst
obtain rfl: a₁ = a₂
rflrfl | ha: ?m✝
 | ha: (a₁, b₁).fst < (a₂, b₂).fst
ha : a₁: α
a₁ = a₂: α
a₂ ∨ _: Prop
_ := ha: (a₁, b₁).fst ≤ (a₂, b₂).fst
ha.eq_or_lt: ∀ {α : Type ?u.18847} [inst : PartialOrder α] {a b : α}, a ≤ b → a = b ∨ a < b
eq_or_ltα: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁, b₂: β

ha: (a₁, b₁).fst ≤ (a₁, b₂).fst

hb: (a₁, b₁).snd ≤ (a₁, b₂).snd

mk.mk.intro.inl↑toLex (a₁, b₁) ≤ ↑toLex (a₁, b₂)
α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

ha✝: (a₁, b₁).fst ≤ (a₂, b₂).fst

hb: (a₁, b₁).snd ≤ (a₂, b₂).snd

ha: (a₁, b₁).fst < (a₂, b₂).fst

mk.mk.intro.inr↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
  α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

Monotone ↑toLex·α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁, b₂: β

ha: (a₁, b₁).fst ≤ (a₁, b₂).fst

hb: (a₁, b₁).snd ≤ (a₁, b₂).snd

mk.mk.intro.inl↑toLex (a₁, b₁) ≤ ↑toLex (a₁, b₂) α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁, b₂: β

ha: (a₁, b₁).fst ≤ (a₁, b₂).fst

hb: (a₁, b₁).snd ≤ (a₁, b₂).snd

mk.mk.intro.inl↑toLex (a₁, b₁) ≤ ↑toLex (a₁, b₂)
α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

ha✝: (a₁, b₁).fst ≤ (a₂, b₂).fst

hb: (a₁, b₁).snd ≤ (a₂, b₂).snd

ha: (a₁, b₁).fst < (a₂, b₂).fst

mk.mk.intro.inr↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)exact right: ∀ {α : Type ?u.18934} {β : Type ?u.18933} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β},
  rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
right _: ?m.18935
_ hb: (a₁, b₁).snd ≤ (a₁, b₂).snd
hb
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

Monotone ↑toLex·α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

ha✝: (a₁, b₁).fst ≤ (a₂, b₂).fst

hb: (a₁, b₁).snd ≤ (a₂, b₂).snd

ha: (a₁, b₁).fst < (a₂, b₂).fst

mk.mk.intro.inr↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂) α: Type u_1

β: Type u_2

γ: Type ?u.18624

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

ha✝: (a₁, b₁).fst ≤ (a₂, b₂).fst

hb: (a₁, b₁).snd ≤ (a₂, b₂).snd

ha: (a₁, b₁).fst < (a₂, b₂).fst

mk.mk.intro.inr↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)exact left: ∀ {α : Type ?u.18967} {β : Type ?u.18966} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β),
  ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
left _: ?m.18969
_ _: ?m.18969
_ ha: (a₁, b₁).fst < (a₂, b₂).fst
ha
Goals accomplished! 🐙
#align prod.lex.to_lex_mono Prod.Lex.toLex_mono: ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β], Monotone ↑toLex
Prod.Lex.toLex_mono

-- porting note: type class search sees right through the type synonrm for `α ×ₗ β` and uses the
-- `Preorder` structure for `α × β` instead
-- This is hopefully the same problems as in https://github.com/leanprover/lean4/issues/1891
-- and will be fixed in nightly-2022-11-30
theorem toLex_strictMono: StrictMono ↑toLex
toLex_strictMono : @StrictMono: {α : Type ?u.19032} → {β : Type ?u.19031} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
StrictMono _: Type ?u.19032
_ _: Type ?u.19031
_ _ (Prod.Lex.preorder: (α : Type ?u.19048) → (β : Type ?u.19047) → [inst : Preorder α] → [inst : Preorder β] → Preorder (Lex (α × β))
Prod.Lex.preorder α: Type ?u.19016
α β: Type ?u.19019
β) (toLex: {α : Type ?u.19077} → α ≃ Lex α
toLex : α: Type ?u.19016
α × β: Type ?u.19019
β → α: Type ?u.19016
α ×ₗ β: Type ?u.19019
β) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

StrictMono ↑toLexrintro ⟨a₁, b₁⟩: α × β
⟨a₁: α
a₁⟨a₁, b₁⟩: α × β
, b₁: β
b₁⟨a₁, b₁⟩: α × β
⟩ ⟨a₂, b₂⟩: α × β
⟨a₂: α
a₂⟨a₂, b₂⟩: α × β
, b₂: β
b₂⟨a₂, b₂⟩: α × β
⟩ h: (a₁, b₁) < (a₂, b₂)
hα: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

h: (a₁, b₁) < (a₂, b₂)

mk.mk↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)
  α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

StrictMono ↑toLexobtain: (a₁, b₁).fst = (a₂, b₂).fst ∨ (a₁, b₁).fst < (a₂, b₂).fst
obtain rfl: a₁ = a₂
rflrfl | ha: ?m✝
 | ha: (a₁, b₁).fst < (a₂, b₂).fst
ha : a₁: α
a₁ = a₂: α
a₂ ∨ _: Prop
_ := h: (a₁, b₁) < (a₂, b₂)
h.le: ∀ {α : Type ?u.19223} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le.1: ∀ {a b : Prop}, a ∧ b → a
1.eq_or_lt: ∀ {α : Type ?u.19261} [inst : PartialOrder α] {a b : α}, a ≤ b → a = b ∨ a < b
eq_or_ltα: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁, b₂: β

h: (a₁, b₁) < (a₁, b₂)

mk.mk.inl↑toLex (a₁, b₁) < ↑toLex (a₁, b₂)
α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

h: (a₁, b₁) < (a₂, b₂)

ha: (a₁, b₁).fst < (a₂, b₂).fst

mk.mk.inr↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)
  α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

StrictMono ↑toLex·α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁, b₂: β

h: (a₁, b₁) < (a₁, b₂)

mk.mk.inl↑toLex (a₁, b₁) < ↑toLex (a₁, b₂) α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁, b₂: β

h: (a₁, b₁) < (a₁, b₂)

mk.mk.inl↑toLex (a₁, b₁) < ↑toLex (a₁, b₂)
α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

h: (a₁, b₁) < (a₂, b₂)

ha: (a₁, b₁).fst < (a₂, b₂).fst

mk.mk.inr↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)exact right: ∀ {α : Type ?u.19346} {β : Type ?u.19345} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β},
  rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
right _: ?m.19347
_ (Prod.mk_lt_mk_iff_right: ∀ {α : Type ?u.19377} {β : Type ?u.19376} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b₁ b₂ : β},
  (a, b₁) < (a, b₂) ↔ b₁ < b₂
Prod.mk_lt_mk_iff_right.1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 h: (a₁, b₁) < (a₁, b₂)
h)
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

StrictMono ↑toLex·α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

h: (a₁, b₁) < (a₂, b₂)

ha: (a₁, b₁).fst < (a₂, b₂).fst

mk.mk.inr↑toLex (a₁, b₁) < ↑toLex (a₂, b₂) α: Type u_1

β: Type u_2

γ: Type ?u.19022

inst✝¹: PartialOrder α

inst✝: Preorder β

a₁: α

b₁: β

a₂: α

b₂: β

h: (a₁, b₁) < (a₂, b₂)

ha: (a₁, b₁).fst < (a₂, b₂).fst

mk.mk.inr↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)exact left: ∀ {α : Type ?u.19443} {β : Type ?u.19442} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β),
  ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
left _: ?m.19445
_ _: ?m.19445
_ ha: (a₁, b₁).fst < (a₂, b₂).fst
ha
Goals accomplished! 🐙
#align prod.lex.to_lex_strict_mono Prod.Lex.toLex_strictMono: ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β], StrictMono ↑toLex
Prod.Lex.toLex_strictMono

end Preorder

/-- Dictionary / lexicographic partial order for pairs. -/
instance partialOrder: (α : Type ?u.19496) →
  (β : Type ?u.19499) → [inst : PartialOrder α] → [inst : PartialOrder β] → PartialOrder (Lex (α × β))
partialOrder (α: Type ?u.19496
α β: Type ?u.19499
β : Type _: Type (?u.19499+1)
Type _) [PartialOrder: Type ?u.19502 → Type ?u.19502
PartialOrder α: Type ?u.19496
α] [PartialOrder: Type ?u.19505 → Type ?u.19505
PartialOrder β: Type ?u.19499
β] : PartialOrder: Type ?u.19508 → Type ?u.19508
PartialOrder (α: Type ?u.19496
α ×ₗ β: Type ?u.19499
β) :=
  { Prod.Lex.preorder: (α : Type ?u.19520) → (β : Type ?u.19519) → [inst : Preorder α] → [inst : Preorder β] → Preorder (Lex (α × β))
Prod.Lex.preorder α: Type ?u.19496
α β: Type ?u.19499
β with
    le_antisymm := by
Goals accomplished! 🐙
      α✝: Type ?u.19487

β✝: Type ?u.19490

γ: Type ?u.19493

α: Type ?u.19496

β: Type ?u.19499

inst✝¹: PartialOrder α

inst✝: PartialOrder β

src✝:= preorder α β: Preorder (Lex (α × β))

∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = bhaveI : IsStrictOrder: (α : Type ?u.19597) → (α → α → Prop) → Prop
IsStrictOrder α: Type ?u.19496
α (· < ·): α → α → Prop
(· < ·) := { irrefl := lt_irrefl: ∀ {α : Type ?u.19643} [inst : Preorder α] (a : α), ¬a < a
lt_irrefl, trans := fun _: ?m.19685
_ _: ?m.19688
_ _: ?m.19691
_ => lt_trans: ∀ {α : Type ?u.19693} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c
lt_trans }α✝: Type ?u.19487

β✝: Type ?u.19490

γ: Type ?u.19493

α: Type ?u.19496

β: Type ?u.19499

inst✝¹: PartialOrder α

inst✝: PartialOrder β

src✝:= preorder α β: Preorder (Lex (α × β))

this: IsStrictOrder α fun x x_1 => x < x_1

∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = b
      α✝: Type ?u.19487

β✝: Type ?u.19490

γ: Type ?u.19493

α: Type ?u.19496

β: Type ?u.19499

inst✝¹: PartialOrder α

inst✝: PartialOrder β

src✝:= preorder α β: Preorder (Lex (α × β))

∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = bhaveI : IsAntisymm: (α : Type ?u.19728) → (α → α → Prop) → Prop
IsAntisymm β: Type ?u.19499
β (· ≤ ·): β → β → Prop
(· ≤ ·) := ⟨fun _: ?m.19767
_ _: ?m.19770
_ => le_antisymm: ∀ {α : Type ?u.19772} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm⟩α✝: Type ?u.19487

β✝: Type ?u.19490

γ: Type ?u.19493

α: Type ?u.19496

β: Type ?u.19499

inst✝¹: PartialOrder α

inst✝: PartialOrder β

src✝:= preorder α β: Preorder (Lex (α × β))

this✝: IsStrictOrder α fun x x_1 => x < x_1

this: IsAntisymm β fun x x_1 => x ≤ x_1

∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = b
      α✝: Type ?u.19487

β✝: Type ?u.19490

γ: Type ?u.19493

α: Type ?u.19496

β: Type ?u.19499

inst✝¹: PartialOrder α

inst✝: PartialOrder β

src✝:= preorder α β: Preorder (Lex (α × β))

∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = bexact @antisymm: ∀ {α : Type ?u.19814} {r : α → α → Prop} [inst : IsAntisymm α r] {a b : α}, r a b → r b a → a = b
antisymm _: Type ?u.19814
_ (Prod.Lex: {α : Type ?u.19817} → {β : Type ?u.19816} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
Prod.Lex _: ?m.19818 → ?m.19818 → Prop
_ _: ?m.19819 → ?m.19819 → Prop
_) _
Goals accomplished! 🐙 }
#align prod.lex.partial_order Prod.Lex.partialOrder: (α : Type u_1) → (β : Type u_2) → [inst : PartialOrder α] → [inst : PartialOrder β] → PartialOrder (Lex (α × β))
Prod.Lex.partialOrder

/-- Dictionary / lexicographic linear order for pairs. -/
instance linearOrder: (α : Type u_1) → (β : Type u_2) → [inst : LinearOrder α] → [inst : LinearOrder β] → LinearOrder (Lex (α × β))
linearOrder (α: Type ?u.20072
α β: Type ?u.20075
β : Type _: Type (?u.20075+1)
Type _) [LinearOrder: Type ?u.20078 → Type ?u.20078
LinearOrder α: Type ?u.20072
α] [LinearOrder: Type ?u.20081 → Type ?u.20081
LinearOrder β: Type ?u.20075
β] : LinearOrder: Type ?u.20084 → Type ?u.20084
LinearOrder (α: Type ?u.20072
α ×ₗ β: Type ?u.20075
β) :=
  { Prod.Lex.partialOrder: (α : Type ?u.20096) →
  (β : Type ?u.20095) → [inst : PartialOrder α] → [inst : PartialOrder β] → PartialOrder (Lex (α × β))
Prod.Lex.partialOrder α: Type ?u.20072
α β: Type ?u.20075
β with
    le_total := total_of: ∀ {α : Type ?u.20207} (r : α → α → Prop) [inst : IsTotal α r] (a b : α), r a b ∨ r b a
total_of (Prod.Lex: {α : Type ?u.20210} → {β : Type ?u.20209} → (α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop
Prod.Lex _: ?m.20211 → ?m.20211 → Prop
_ _: ?m.20212 → ?m.20212 → Prop
_),
    decidableLE := Prod.Lex.decidable: {α : Type ?u.20417} →
  {β : Type ?u.20416} →
    [inst : DecidableEq α] →
      (r : α → α → Prop) →
        (s : β → β → Prop) → [inst : DecidableRel r] → [inst : DecidableRel s] → DecidableRel (Prod.Lex r s)
Prod.Lex.decidable _: ?m.20418 → ?m.20418 → Prop
_ _: ?m.20419 → ?m.20419 → Prop
_,
    decidableLT := Prod.Lex.decidable: {α : Type ?u.20978} →
  {β : Type ?u.20977} →
    [inst : DecidableEq α] →
      (r : α → α → Prop) →
        (s : β → β → Prop) → [inst : DecidableRel r] → [inst : DecidableRel s] → DecidableRel (Prod.Lex r s)
Prod.Lex.decidable _: ?m.20979 → ?m.20979 → Prop
_ _: ?m.20980 → ?m.20980 → Prop
_,
    decidableEq := Lex.decidableEq: (α : Type ?u.20830) → (β : Type ?u.20829) → [inst : DecidableEq α] → [inst : DecidableEq β] → DecidableEq (Lex (α × β))
Lex.decidableEq _: Type ?u.20830
_ _: Type ?u.20829
_, }
#align prod.lex.linear_order Prod.Lex.linearOrder: (α : Type u_1) → (β : Type u_2) → [inst : LinearOrder α] → [inst : LinearOrder β] → LinearOrder (Lex (α × β))
Prod.Lex.linearOrder

instance orderBot: [inst : PartialOrder α] → [inst_1 : Preorder β] → [inst_2 : OrderBot α] → [inst_3 : OrderBot β] → OrderBot (Lex (α × β))
orderBot [PartialOrder: Type ?u.22069 → Type ?u.22069
PartialOrder α: Type ?u.22060
α] [Preorder: Type ?u.22072 → Type ?u.22072
Preorder β: Type ?u.22063
β] [OrderBot: (α : Type ?u.22075) → [inst : LE α] → Type ?u.22075
OrderBot α: Type ?u.22060
α] [OrderBot: (α : Type ?u.22096) → [inst : LE α] → Type ?u.22096
OrderBot β: Type ?u.22063
β] : OrderBot: (α : Type ?u.22110) → [inst : LE α] → Type ?u.22110
OrderBot (α: Type ?u.22060
α ×ₗ β: Type ?u.22063
β) where
  bot := toLex: {α : Type ?u.22179} → α ≃ Lex α
toLex ⊥: ?m.22243
⊥
  bot_le _: ?m.22271
_ := toLex_mono: ∀ {α : Type ?u.22273} {β : Type ?u.22274} [inst : PartialOrder α] [inst_1 : Preorder β], Monotone ↑toLex
toLex_mono bot_le: ∀ {α : Type ?u.22357} [inst : LE α] [inst_1 : OrderBot α] {a : α}, ⊥ ≤ a
bot_le
#align prod.lex.order_bot Prod.Lex.orderBot: {α : Type u_1} →
  {β : Type u_2} →
    [inst : PartialOrder α] →
      [inst_1 : Preorder β] → [inst_2 : OrderBot α] → [inst_3 : OrderBot β] → OrderBot (Lex (α × β))
Prod.Lex.orderBot

instance orderTop: [inst : PartialOrder α] → [inst_1 : Preorder β] → [inst_2 : OrderTop α] → [inst_3 : OrderTop β] → OrderTop (Lex (α × β))
orderTop [PartialOrder: Type ?u.22687 → Type ?u.22687
PartialOrder α: Type ?u.22678
α] [Preorder: Type ?u.22690 → Type ?u.22690
Preorder β: Type ?u.22681
β] [OrderTop: (α : Type ?u.22693) → [inst : LE α] → Type ?u.22693
OrderTop α: Type ?u.22678
α] [OrderTop: (α : Type ?u.22714) → [inst : LE α] → Type ?u.22714
OrderTop β: Type ?u.22681
β] : OrderTop: (α : Type ?u.22728) → [inst : LE α] → Type ?u.22728
OrderTop (α: Type ?u.22678
α ×ₗ β: Type ?u.22681
β) where
  top := toLex: {α : Type ?u.22797} → α ≃ Lex α
toLex ⊤: ?m.22861
⊤
  le_top _: ?m.22889
_ := toLex_mono: ∀ {α : Type ?u.22891} {β : Type ?u.22892} [inst : PartialOrder α] [inst_1 : Preorder β], Monotone ↑toLex
toLex_mono le_top: ∀ {α : Type ?u.22971} [inst : LE α] [inst_1 : OrderTop α] {a : α}, a ≤ ⊤
le_top
#align prod.lex.order_top Prod.Lex.orderTop: {α : Type u_1} →
  {β : Type u_2} →
    [inst : PartialOrder α] →
      [inst_1 : Preorder β] → [inst_2 : OrderTop α] → [inst_3 : OrderTop β] → OrderTop (Lex (α × β))
Prod.Lex.orderTop

instance boundedOrder: {α : Type u_1} →
  {β : Type u_2} →
    [inst : PartialOrder α] →
      [inst_1 : Preorder β] → [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedOrder (Lex (α × β))
boundedOrder [PartialOrder: Type ?u.23266 → Type ?u.23266
PartialOrder α: Type ?u.23257
α] [Preorder: Type ?u.23269 → Type ?u.23269
Preorder β: Type ?u.23260
β] [BoundedOrder: (α : Type ?u.23272) → [inst : LE α] → Type ?u.23272
BoundedOrder α: Type ?u.23257
α] [BoundedOrder: (α : Type ?u.23293) → [inst : LE α] → Type ?u.23293
BoundedOrder β: Type ?u.23260
β] :
    BoundedOrder: (α : Type ?u.23307) → [inst : LE α] → Type ?u.23307
BoundedOrder (α: Type ?u.23257
α ×ₗ β: Type ?u.23260
β) :=
  { Lex.orderBot, Lex.orderTop with }: BoundedOrder ?m.23588
{ Lex.orderBot: {α : Type ?u.23348} →
  {β : Type ?u.23347} →
    [inst : PartialOrder α] →
      [inst_1 : Preorder β] → [inst_2 : OrderBot α] → [inst_3 : OrderBot β] → OrderBot (Lex (α × β))
Lex.orderBot{ Lex.orderBot, Lex.orderTop with }: BoundedOrder ?m.23588
, Lex.orderTop: {α : Type ?u.23469} →
  {β : Type ?u.23468} →
    [inst : PartialOrder α] →
      [inst_1 : Preorder β] → [inst_2 : OrderTop α] → [inst_3 : OrderTop β] → OrderTop (Lex (α × β))
Lex.orderTop{ Lex.orderBot, Lex.orderTop with }: BoundedOrder ?m.23588
 { Lex.orderBot, Lex.orderTop with }: BoundedOrder ?m.23588
with{ Lex.orderBot, Lex.orderTop with }: BoundedOrder ?m.23588
 }
#align prod.lex.bounded_order Prod.Lex.boundedOrder: {α : Type u_1} →
  {β : Type u_2} →
    [inst : PartialOrder α] →
      [inst_1 : Preorder β] → [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedOrder (Lex (α × β))
Prod.Lex.boundedOrder

instance: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : DenselyOrdered α]
  [inst_3 : DenselyOrdered β], DenselyOrdered (Lex (α × β))
instance [Preorder: Type ?u.23973 → Type ?u.23973
Preorder α: Type ?u.23964
α] [Preorder: Type ?u.23976 → Type ?u.23976
Preorder β: Type ?u.23967
β] [DenselyOrdered: (α : Type ?u.23979) → [inst : LT α] → Prop
DenselyOrdered α: Type ?u.23964
α] [DenselyOrdered: (α : Type ?u.23993) → [inst : LT α] → Prop
DenselyOrdered β: Type ?u.23967
β] :
    DenselyOrdered: (α : Type ?u.24007) → [inst : LT α] → Prop
DenselyOrdered (α: Type ?u.23964
α ×ₗ β: Type ?u.23967
β) where
  dense := by
Goals accomplished! 🐙
    α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

∀ (a₁ a₂ : Lex (α × β)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂rintro _: Lex (α × β)
_ _: Lex (α × β)
_ (@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩): a₁✝ < a₂✝
(@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
@⟨a₁: α
a₁@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
, b₁: β
b₁@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
, a₂: α
a₂@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
, b₂: β
b₂@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
, h: a₁ < a₂
h@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
⟩ | @⟨a: α
a@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
, b₁: β
b₁@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
, b₂: β
b₂@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
, h: b₁ < b₂
h@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩: a₁✝ < a₂✝
⟩(@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩): a₁✝ < a₂✝
)α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a₁: α

b₁: β

a₂: α

b₂: β

h: a₁ < a₂

left∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)
α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a: α

b₁, b₂: β

h: b₁ < b₂

right∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)
    α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

∀ (a₁ a₂ : Lex (α × β)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂·α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a₁: α

b₁: β

a₂: α

b₂: β

h: a₁ < a₂

left∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂) α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a₁: α

b₁: β

a₂: α

b₂: β

h: a₁ < a₂

left∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)
α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a: α

b₁, b₂: β

h: b₁ < b₂

right∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)obtain ⟨c, h₁, h₂⟩: ∃ a, a₁ < a ∧ a < a₂
⟨c: α
c⟨c, h₁, h₂⟩: ∃ a, a₁ < a ∧ a < a₂
, h₁: a₁ < c
h₁⟨c, h₁, h₂⟩: ∃ a, a₁ < a ∧ a < a₂
, h₂: c < a₂
h₂⟨c, h₁, h₂⟩: ∃ a, a₁ < a ∧ a < a₂
⟩ := exists_between: ∀ {α : Type ?u.24281} [inst : LT α] [inst_1 : DenselyOrdered α] {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
exists_between h: a₁ < a₂
hα: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a₁: α

b₁: β

a₂: α

b₂: β

h: a₁ < a₂

c: α

h₁: a₁ < c

h₂: c < a₂

left.intro.intro∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)
      α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a₁: α

b₁: β

a₂: α

b₂: β

h: a₁ < a₂

left∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)exact ⟨(c: α
c, b₁: β
b₁), left: ∀ {α : Type ?u.24383} {β : Type ?u.24382} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β),
  ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
left _: ?m.24385
_ _: ?m.24385
_ h₁: a₁ < c
h₁, left: ∀ {α : Type ?u.24405} {β : Type ?u.24404} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β),
  ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
left _: ?m.24407
_ _: ?m.24407
_ h₂: c < a₂
h₂⟩
Goals accomplished! 🐙
    α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

∀ (a₁ a₂ : Lex (α × β)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂·α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a: α

b₁, b₂: β

h: b₁ < b₂

right∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂) α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a: α

b₁, b₂: β

h: b₁ < b₂

right∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)obtain ⟨c, h₁, h₂⟩: ∃ a, b₁ < a ∧ a < b₂
⟨c: β
c⟨c, h₁, h₂⟩: ∃ a, b₁ < a ∧ a < b₂
, h₁: b₁ < c
h₁⟨c, h₁, h₂⟩: ∃ a, b₁ < a ∧ a < b₂
, h₂: c < b₂
h₂⟨c, h₁, h₂⟩: ∃ a, b₁ < a ∧ a < b₂
⟩ := exists_between: ∀ {α : Type ?u.24425} [inst : LT α] [inst_1 : DenselyOrdered α] {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
exists_between h: b₁ < b₂
hα: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a: α

b₁, b₂: β

h: b₁ < b₂

c: β

h₁: b₁ < c

h₂: c < b₂

right.intro.intro∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)
      α: Type ?u.23964

β: Type ?u.23967

γ: Type ?u.23970

inst✝³: Preorder α

inst✝²: Preorder β

inst✝¹: DenselyOrdered α

inst✝: DenselyOrdered β

a: α

b₁, b₂: β

h: b₁ < b₂

right∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)exact ⟨(a: α
a, c: β
c), right: ∀ {α : Type ?u.24508} {β : Type ?u.24507} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β},
  rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
right _: ?m.24509
_ h₁: b₁ < c
h₁, right: ∀ {α : Type ?u.24525} {β : Type ?u.24524} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β},
  rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
right _: ?m.24526
_ h₂: c < b₂
h₂⟩
Goals accomplished! 🐙

instance noMaxOrder_of_left: ∀ [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder α], NoMaxOrder (Lex (α × β))
noMaxOrder_of_left [Preorder: Type ?u.24663 → Type ?u.24663
Preorder α: Type ?u.24654
α] [Preorder: Type ?u.24666 → Type ?u.24666
Preorder β: Type ?u.24657
β] [NoMaxOrder: (α : Type ?u.24669) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.24654
α] : NoMaxOrder: (α : Type ?u.24683) → [inst : LT α] → Prop
NoMaxOrder (α: Type ?u.24654
α ×ₗ β: Type ?u.24657
β) where
  exists_gt := by
Goals accomplished! 🐙
    α: Type ?u.24654

β: Type ?u.24657

γ: Type ?u.24660

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder α

∀ (a : Lex (α × β)), ∃ b, a < brintro ⟨a, b⟩: Lex (α × β)
⟨a: α
a⟨a, b⟩: Lex (α × β)
, b: β
b⟨a, b⟩: Lex (α × β)
⟩α: Type ?u.24654

β: Type ?u.24657

γ: Type ?u.24660

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder α

a: α

b: β

mk∃ b_1, (a, b) < b_1
    α: Type ?u.24654

β: Type ?u.24657

γ: Type ?u.24660

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder α

∀ (a : Lex (α × β)), ∃ b, a < bobtain ⟨c, h⟩: ∃ b, a < b
⟨c: α
c⟨c, h⟩: ∃ b, a < b
, h: a < c
h⟨c, h⟩: ∃ b, a < b
⟩ := exists_gt: ∀ {α : Type ?u.24770} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt a: α
aα: Type ?u.24654

β: Type ?u.24657

γ: Type ?u.24660

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder α

a: α

b: β

c: α

h: a < c

mk.intro∃ b_1, (a, b) < b_1
    α: Type ?u.24654

β: Type ?u.24657

γ: Type ?u.24660

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder α

∀ (a : Lex (α × β)), ∃ b, a < bexact ⟨⟨c: α
c, b: β
b⟩, left: ∀ {α : Type ?u.24838} {β : Type ?u.24837} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β),
  ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
left _: ?m.24840
_ _: ?m.24840
_ h: a < c
h⟩
Goals accomplished! 🐙
#align prod.lex.no_max_order_of_left Prod.Lex.noMaxOrder_of_left: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder α],
  NoMaxOrder (Lex (α × β))
Prod.Lex.noMaxOrder_of_left

instance noMinOrder_of_left: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMinOrder α],
  NoMinOrder (Lex (α × β))
noMinOrder_of_left [Preorder: Type ?u.24932 → Type ?u.24932
Preorder α: Type ?u.24923
α] [Preorder: Type ?u.24935 → Type ?u.24935
Preorder β: Type ?u.24926
β] [NoMinOrder: (α : Type ?u.24938) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.24923
α] : NoMinOrder: (α : Type ?u.24952) → [inst : LT α] → Prop
NoMinOrder (α: Type ?u.24923
α ×ₗ β: Type ?u.24926
β) where
  exists_lt := by
Goals accomplished! 🐙
    α: Type ?u.24923

β: Type ?u.24926

γ: Type ?u.24929

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder α

∀ (a : Lex (α × β)), ∃ b, b < arintro ⟨a, b⟩: Lex (α × β)
⟨a: α
a⟨a, b⟩: Lex (α × β)
, b: β
b⟨a, b⟩: Lex (α × β)
⟩α: Type ?u.24923

β: Type ?u.24926

γ: Type ?u.24929

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder α

a: α

b: β

mk∃ b_1, b_1 < (a, b)
    α: Type ?u.24923

β: Type ?u.24926

γ: Type ?u.24929

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder α

∀ (a : Lex (α × β)), ∃ b, b < aobtain ⟨c, h⟩: ∃ b, b < a
⟨c: α
c⟨c, h⟩: ∃ b, b < a
, h: c < a
h⟨c, h⟩: ∃ b, b < a
⟩ := exists_lt: ∀ {α : Type ?u.25039} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt a: α
aα: Type ?u.24923

β: Type ?u.24926

γ: Type ?u.24929

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder α

a: α

b: β

c: α

h: c < a

mk.intro∃ b_1, b_1 < (a, b)
    α: Type ?u.24923

β: Type ?u.24926

γ: Type ?u.24929

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder α

∀ (a : Lex (α × β)), ∃ b, b < aexact ⟨⟨c: α
c, b: β
b⟩, left: ∀ {α : Type ?u.25107} {β : Type ?u.25106} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β),
  ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
left _: ?m.25109
_ _: ?m.25109
_ h: c < a
h⟩
Goals accomplished! 🐙
#align prod.lex.no_min_order_of_left Prod.Lex.noMinOrder_of_left: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMinOrder α],
  NoMinOrder (Lex (α × β))
Prod.Lex.noMinOrder_of_left

instance noMaxOrder_of_right: ∀ [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder β], NoMaxOrder (Lex (α × β))
noMaxOrder_of_right [Preorder: Type ?u.25201 → Type ?u.25201
Preorder α: Type ?u.25192
α] [Preorder: Type ?u.25204 → Type ?u.25204
Preorder β: Type ?u.25195
β] [NoMaxOrder: (α : Type ?u.25207) → [inst : LT α] → Prop
NoMaxOrder β: Type ?u.25195
β] : NoMaxOrder: (α : Type ?u.25221) → [inst : LT α] → Prop
NoMaxOrder (α: Type ?u.25192
α ×ₗ β: Type ?u.25195
β) where
  exists_gt := by
Goals accomplished! 🐙
    α: Type ?u.25192

β: Type ?u.25195

γ: Type ?u.25198

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder β

∀ (a : Lex (α × β)), ∃ b, a < brintro ⟨a, b⟩: Lex (α × β)
⟨a: α
a⟨a, b⟩: Lex (α × β)
, b: β
b⟨a, b⟩: Lex (α × β)
⟩α: Type ?u.25192

β: Type ?u.25195

γ: Type ?u.25198

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder β

a: α

b: β

mk∃ b_1, (a, b) < b_1
    α: Type ?u.25192

β: Type ?u.25195

γ: Type ?u.25198

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder β

∀ (a : Lex (α × β)), ∃ b, a < bobtain ⟨c, h⟩: ∃ b_1, b < b_1
⟨c: β
c⟨c, h⟩: ∃ b_1, b < b_1
, h: b < c
h⟨c, h⟩: ∃ b_1, b < b_1
⟩ := exists_gt: ∀ {α : Type ?u.25308} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt b: β
bα: Type ?u.25192

β: Type ?u.25195

γ: Type ?u.25198

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder β

a: α

b, c: β

h: b < c

mk.intro∃ b_1, (a, b) < b_1
    α: Type ?u.25192

β: Type ?u.25195

γ: Type ?u.25198

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder β

∀ (a : Lex (α × β)), ∃ b, a < bexact ⟨⟨a: α
a, c: β
c⟩, right: ∀ {α : Type ?u.25376} {β : Type ?u.25375} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β},
  rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
right _: ?m.25377
_ h: b < c
h⟩
Goals accomplished! 🐙
#align prod.lex.no_max_order_of_right Prod.Lex.noMaxOrder_of_right: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder β],
  NoMaxOrder (Lex (α × β))
Prod.Lex.noMaxOrder_of_right

instance noMinOrder_of_right: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMinOrder β],
  NoMinOrder (Lex (α × β))
noMinOrder_of_right [Preorder: Type ?u.25469 → Type ?u.25469
Preorder α: Type ?u.25460
α] [Preorder: Type ?u.25472 → Type ?u.25472
Preorder β: Type ?u.25463
β] [NoMinOrder: (α : Type ?u.25475) → [inst : LT α] → Prop
NoMinOrder β: Type ?u.25463
β] : NoMinOrder: (α : Type ?u.25489) → [inst : LT α] → Prop
NoMinOrder (α: Type ?u.25460
α ×ₗ β: Type ?u.25463
β) where
  exists_lt := by
Goals accomplished! 🐙
    α: Type ?u.25460

β: Type ?u.25463

γ: Type ?u.25466

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder β

∀ (a : Lex (α × β)), ∃ b, b < arintro ⟨a, b⟩: Lex (α × β)
⟨a: α
a⟨a, b⟩: Lex (α × β)
, b: β
b⟨a, b⟩: Lex (α × β)
⟩α: Type ?u.25460

β: Type ?u.25463

γ: Type ?u.25466

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder β

a: α

b: β

mk∃ b_1, b_1 < (a, b)
    α: Type ?u.25460

β: Type ?u.25463

γ: Type ?u.25466

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder β

∀ (a : Lex (α × β)), ∃ b, b < aobtain ⟨c, h⟩: ∃ b_1, b_1 < b
⟨c: β
c⟨c, h⟩: ∃ b_1, b_1 < b
, h: c < b
h⟨c, h⟩: ∃ b_1, b_1 < b
⟩ := exists_lt: ∀ {α : Type ?u.25576} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt b: β
bα: Type ?u.25460

β: Type ?u.25463

γ: Type ?u.25466

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder β

a: α

b, c: β

h: c < b

mk.intro∃ b_1, b_1 < (a, b)
    α: Type ?u.25460

β: Type ?u.25463

γ: Type ?u.25466

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder β

∀ (a : Lex (α × β)), ∃ b, b < aexact ⟨⟨a: α
a, c: β
c⟩, right: ∀ {α : Type ?u.25644} {β : Type ?u.25643} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β},
  rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
right _: ?m.25645
_ h: c < b
h⟩
Goals accomplished! 🐙
#align prod.lex.no_min_order_of_right Prod.Lex.noMinOrder_of_right: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMinOrder β],
  NoMinOrder (Lex (α × β))
Prod.Lex.noMinOrder_of_right

end Prod.Lex