[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ (a₁, b₁) < (a₂, b₂) ↔ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ (a₁, b₁) < (a₂, b₂) → (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
rintro (⟨_, _, hlt⟩ | ⟨_, hlt⟩)
[GOAL]
case mp.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
⊢ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
constructor
[GOAL]
case mp.left.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
⊢ (a₁, b₁) ≤ (a₂, b₂)
[PROOFSTEP]
exact left _ _ hlt
[GOAL]
case mp.left.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
⊢ ¬(a₂, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mp.left.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
h✝ : a₂ < a₁
⊢ False
[PROOFSTEP]
apply lt_asymm hlt
[GOAL]
case mp.left.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hlt : a₁ < a₂
h✝ : a₂ < a₁
⊢ a₂ < a₁
[PROOFSTEP]
assumption
[GOAL]
case mp.left.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : a₁ < a₁
h✝ : b₂ ≤ b₁
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hlt
[GOAL]
case mp.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
⊢ (a₁, b₁) ≤ (a₁, b₂) ∧ ¬(a₁, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
constructor
[GOAL]
case mp.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
⊢ (a₁, b₁) ≤ (a₁, b₂)
[PROOFSTEP]
right
[GOAL]
case mp.right.left.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
⊢ b₁ ≤ b₂
[PROOFSTEP]
rw [lt_iff_le_not_le] at hlt 
[GOAL]
case mp.right.left.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
⊢ b₁ ≤ b₂
[PROOFSTEP]
exact hlt.1
[GOAL]
case mp.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
⊢ ¬(a₁, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mp.right.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
h✝ : a₁ < a₁
⊢ False
[PROOFSTEP]
apply lt_irrefl a₁
[GOAL]
case mp.right.right.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
h✝ : a₁ < a₁
⊢ a₁ < a₁
[PROOFSTEP]
assumption
[GOAL]
case mp.right.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ < b₂
h✝ : b₂ ≤ b₁
⊢ False
[PROOFSTEP]
rw [lt_iff_le_not_le] at hlt 
[GOAL]
case mp.right.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
h✝ : b₂ ≤ b₁
⊢ False
[PROOFSTEP]
apply hlt.2
[GOAL]
case mp.right.right.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
hlt : b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
h✝ : b₂ ≤ b₁
⊢ b₂ ≤ b₁
[PROOFSTEP]
assumption
[GOAL]
case mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ (a₁, b₁) ≤ (a₂, b₂) ∧ ¬(a₂, b₂) ≤ (a₁, b₁) → (a₁, b₁) < (a₂, b₂)
[PROOFSTEP]
rintro ⟨⟨⟩, h₂r⟩
[GOAL]
case mpr.intro.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h₂r : ¬(a₂, b₂) ≤ (a₁, b₁)
h✝ : a₁ < a₂
⊢ (a₁, b₁) < (a₂, b₂)
[PROOFSTEP]
left
[GOAL]
case mpr.intro.left.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h₂r : ¬(a₂, b₂) ≤ (a₁, b₁)
h✝ : a₁ < a₂
⊢ a₁ < a₂
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ (a₁, b₁) < (a₁, b₂)
[PROOFSTEP]
right
[GOAL]
case mpr.intro.right.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ b₁ < b₂
[PROOFSTEP]
rw [lt_iff_le_not_le]
[GOAL]
case mpr.intro.right.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ b₁ ≤ b₂ ∧ ¬b₂ ≤ b₁
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.right.h.left
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ b₁ ≤ b₂
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.right.h.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
⊢ ¬b₂ ≤ b₁
[PROOFSTEP]
intro h
[GOAL]
case mpr.intro.right.h.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
h : b₂ ≤ b₁
⊢ False
[PROOFSTEP]
apply h₂r
[GOAL]
case mpr.intro.right.h.right
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
h : b₂ ≤ b₁
⊢ (a₁, b₂) ≤ (a₁, b₁)
[PROOFSTEP]
right
[GOAL]
case mpr.intro.right.h.right.h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (Lex (α × β)) := instLE α β
src✝ : LT (Lex (α × β)) := instLT α β
x₁ x₂ : Lex (α × β)
a₁ : α
b₁ b₂ : β
h₂r : ¬(a₁, b₂) ≤ (a₁, b₁)
h✝ : b₁ ≤ b₂
h : b₂ ≤ b₁
⊢ b₂ ≤ b₁
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
⊢ Monotone ↑toLex
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨ha, hb⟩
[GOAL]
case mk.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha : (a₁, b₁).fst ≤ (a₂, b₂).fst
hb : (a₁, b₁).snd ≤ (a₂, b₂).snd
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
[PROOFSTEP]
obtain rfl | ha : a₁ = a₂ ∨ _ := ha.eq_or_lt
[GOAL]
case mk.mk.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
ha : (a₁, b₁).fst ≤ (a₁, b₂).fst
hb : (a₁, b₁).snd ≤ (a₁, b₂).snd
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₁, b₂)
[PROOFSTEP]
exact right _ hb
[GOAL]
case mk.mk.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
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
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
[PROOFSTEP]
exact left _ _ ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
⊢ StrictMono ↑toLex
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ ↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)
[PROOFSTEP]
obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ ↑toLex (a₁, b₁) < ↑toLex (a₁, b₂)
[PROOFSTEP]
exact right _ (Prod.mk_lt_mk_iff_right.1 h)
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).fst < (a₂, b₂).fst
⊢ ↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)
[PROOFSTEP]
exact left _ _ ha
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
src✝ : Preorder (Lex (α × β)) := preorder α β
⊢ ∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
haveI : IsStrictOrder α (· < ·) := { irrefl := lt_irrefl, trans := fun _ _ _ => lt_trans }
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
src✝ : Preorder (Lex (α × β)) := preorder α β
this : IsStrictOrder α fun x x_1 => x < x_1
⊢ ∀ (a b : Lex (α × β)), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
haveI : IsAntisymm β (· ≤ ·) := ⟨fun _ _ => le_antisymm⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
src✝ : Preorder (Lex (α × β)) := preorder α β
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
[PROOFSTEP]
exact @antisymm _ (Prod.Lex _ _) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
⊢ ∀ (a₁ a₂ : Lex (α × β)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro _ _ (@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩)
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
⊢ ∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)
[PROOFSTEP]
obtain ⟨c, h₁, h₂⟩ := exists_between h
[GOAL]
case left.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
c : α
h₁ : a₁ < c
h₂ : c < a₂
⊢ ∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)
[PROOFSTEP]
exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a : α
b₁ b₂ : β
h : b₁ < b₂
⊢ ∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)
[PROOFSTEP]
obtain ⟨c, h₁, h₂⟩ := exists_between h
[GOAL]
case right.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a : α
b₁ b₂ : β
h : b₁ < b₂
c : β
h₁ : b₁ < c
h₂ : c < b₂
⊢ ∃ a_1, (a, b₁) < a_1 ∧ a_1 < (a, b₂)
[PROOFSTEP]
exact ⟨(a, c), right _ h₁, right _ h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_gt a
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
c : α
h : a < c
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
exact ⟨⟨c, b⟩, left _ _ h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
⊢ ∀ (a : Lex (α × β)), ∃ b, b < a
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_lt a
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
a : α
b : β
c : α
h : c < a
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
exact ⟨⟨c, b⟩, left _ _ h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b : β
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_gt b
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b c : β
h : b < c
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
exact ⟨⟨a, c⟩, right _ h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
⊢ ∀ (a : Lex (α × β)), ∃ b, b < a
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_lt b
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
a : α
b c : β
h : c < b
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
exact ⟨⟨a, c⟩, right _ h⟩
