[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
⊢ ∀ (a : α ⊕ β), ¬LiftRel r s a a
[PROOFSTEP]
rintro _ (⟨h⟩ | ⟨h⟩)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
a✝ : α
h : r a✝ a✝
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
b✝ : β
h : s b✝ b✝
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
⊢ ∀ (a b : α ⊕ β), LiftRel r s a b → LiftRel r s b a → a = b
[PROOFSTEP]
rintro _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hba⟩ | ⟨hba⟩)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
a✝ c✝ : α
hab : r a✝ c✝
hba : r c✝ a✝
⊢ inl a✝ = inl c✝
[PROOFSTEP]
rw [antisymm hab hba]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
b✝ d✝ : β
hab : s b✝ d✝
hba : s d✝ b✝
⊢ inr b✝ = inr d✝
[PROOFSTEP]
rw [antisymm hab hba]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsRefl β s
⊢ ∀ (a : α ⊕ β), Lex r s a a
[PROOFSTEP]
rintro (a | a)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsRefl β s
a : α
⊢ Lex r s (inl a) (inl a)
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsRefl β s
a : β
⊢ Lex r s (inr a) (inr a)
[PROOFSTEP]
exacts [Lex.inl (refl _), Lex.inr (refl _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
⊢ ∀ (a : α ⊕ β), ¬Lex r s a a
[PROOFSTEP]
rintro _ (⟨h⟩ | ⟨h⟩)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
a₁✝ : α
h : r a₁✝ a₁✝
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsIrrefl α r
inst✝ : IsIrrefl β s
b₁✝ : β
h : s b₁✝ b₁✝
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
⊢ ∀ (a b c : α ⊕ β), Lex r s a b → Lex r s b c → Lex r s a c
[PROOFSTEP]
rintro _ _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hbc⟩ | ⟨hbc⟩)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a₁✝ a₂✝¹ : α
hab : r a₁✝ a₂✝¹
a₂✝ : α
hbc : r a₂✝¹ a₂✝
⊢ Lex r s (inl a₁✝) (inl a₂✝)
case inl.sep
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
b✝ : β
⊢ Lex r s (inl a₁✝) (inr b✝)
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
b₁✝ b₂✝¹ : β
hab : s b₁✝ b₂✝¹
b₂✝ : β
hbc : s b₂✝¹ b₂✝
⊢ Lex r s (inr b₁✝) (inr b₂✝)
case sep.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a✝ : α
b✝ b₂✝ : β
hbc : s b✝ b₂✝
⊢ Lex r s (inl a✝) (inr b₂✝)
[PROOFSTEP]
exacts [.inl (_root_.trans hab hbc), .sep _ _, .inr (_root_.trans hab hbc), .sep _ _]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
⊢ ∀ (a b : α ⊕ β), Lex r s a b → Lex r s b a → a = b
[PROOFSTEP]
rintro _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hba⟩ | ⟨hba⟩)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
hba : r a₂✝ a₁✝
⊢ inl a₁✝ = inl a₂✝
[PROOFSTEP]
rw [antisymm hab hba]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsAntisymm α r
inst✝ : IsAntisymm β s
b₁✝ b₂✝ : β
hab : s b₁✝ b₂✝
hba : s b₂✝ b₁✝
⊢ inr b₁✝ = inr b₂✝
[PROOFSTEP]
rw [antisymm hab hba]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a b : α ⊕ β
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
refine' ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, _⟩, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a b : α ⊕ β
hab : a < b
⊢ ¬b ≤ a
[PROOFSTEP]
rintro (⟨hba⟩ | ⟨hba⟩)
[GOAL]
case refine'_1.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a✝ c✝ : α
hba : a✝ ≤ c✝
hab : inl c✝ < inl a✝
⊢ False
[PROOFSTEP]
exact hba.not_lt (inl_lt_inl_iff.1 hab)
[GOAL]
case refine'_1.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
b✝ d✝ : β
hba : b✝ ≤ d✝
hab : inr d✝ < inr b✝
⊢ False
[PROOFSTEP]
exact hba.not_lt (inr_lt_inr_iff.1 hab)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a b : α ⊕ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b
[PROOFSTEP]
rintro ⟨⟨hab⟩ | ⟨hab⟩, hba⟩
[GOAL]
case refine'_2.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
a✝ c✝ : α
hab : a✝ ≤ c✝
hba : ¬inl c✝ ≤ inl a✝
⊢ inl a✝ < inl c✝
[PROOFSTEP]
exact LiftRel.inl (hab.lt_of_not_le fun h => hba <| LiftRel.inl h)
[GOAL]
case refine'_2.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (α ⊕ β) := instLESum
src✝ : LT (α ⊕ β) := instLTSum
b✝ d✝ : β
hab : b✝ ≤ d✝
hba : ¬inr d✝ ≤ inr b✝
⊢ inr b✝ < inr d✝
[PROOFSTEP]
exact LiftRel.inr (hab.lt_of_not_le fun h => hba <| LiftRel.inr h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
⊢ ∃ b, b < a
[PROOFSTEP]
obtain ⟨b | b, h⟩ := exists_lt (inl a : Sum α β)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : α
h : inl b < inl a
⊢ ∃ b, b < a
[PROOFSTEP]
exact ⟨b, inl_lt_inl_iff.1 h⟩
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
b : β
h : inr b < inl a
⊢ ∃ b, b < a
[PROOFSTEP]
exact (not_inr_lt_inl h).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
⊢ ∃ b, b < a
[PROOFSTEP]
obtain ⟨b | b, h⟩ := exists_lt (inr a : Sum α β)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ b, b < a
[PROOFSTEP]
exact (not_inl_lt_inr h).elim
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : β
h : inr b < inr a
⊢ ∃ b, b < a
[PROOFSTEP]
exact ⟨b, inr_lt_inr_iff.1 h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
⊢ ∃ b, a < b
[PROOFSTEP]
obtain ⟨b | b, h⟩ := exists_gt (inl a : Sum α β)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : α
h : inl a < inl b
⊢ ∃ b, a < b
[PROOFSTEP]
exact ⟨b, inl_lt_inl_iff.1 h⟩
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
b : β
h : inl a < inr b
⊢ ∃ b, a < b
[PROOFSTEP]
exact (not_inl_lt_inr h).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
⊢ ∃ b, a < b
[PROOFSTEP]
obtain ⟨b | b, h⟩ := exists_gt (inr a : Sum α β)
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : β
b : α
h : inr a < inl b
⊢ ∃ b, a < b
[PROOFSTEP]
exact (not_inr_lt_inl h).elim
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : β
h : inr a < inr b
⊢ ∃ b, a < b
[PROOFSTEP]
exact ⟨b, inr_lt_inr_iff.1 h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
obtain ⟨c | c, ha, hb⟩ := @exists_between (Sum α β) _ _ _ _ (inl_lt_inl_iff.2 h)
[GOAL]
case intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : α
ha : inl a < inl c
hb : inl c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩
[GOAL]
case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
exact (not_inl_lt_inr ha).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
obtain ⟨c | c, ha, hb⟩ := @exists_between (Sum α β) _ _ _ _ (inr_lt_inr_iff.2 h)
[GOAL]
case intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : α
ha : inr a < inl c
hb : inl c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
exact (not_inl_lt_inr hb).elim
[GOAL]
case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : β
ha : inr a < inr c
hb : inr c < inr b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
[PROOFSTEP]
exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a b : _root_.Lex (α ⊕ β)
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
[PROOFSTEP]
refine' ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, _⟩, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a b : _root_.Lex (α ⊕ β)
hab : a < b
⊢ ¬b ≤ a
[PROOFSTEP]
rintro (⟨hba⟩ | ⟨hba⟩ | ⟨b, a⟩)
[GOAL]
case refine'_1.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a₁✝ a₂✝ : α
hba : a₁✝ ≤ a₂✝
hab : inl a₂✝ < inl a₁✝
⊢ False
[PROOFSTEP]
exact hba.not_lt (inl_lt_inl_iff.1 hab)
[GOAL]
case refine'_1.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
b₁✝ b₂✝ : β
hba : b₁✝ ≤ b₂✝
hab : inr b₂✝ < inr b₁✝
⊢ False
[PROOFSTEP]
exact hba.not_lt (inr_lt_inr_iff.1 hab)
[GOAL]
case refine'_1.sep
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
b : α
a : β
hab : inr a < inl b
⊢ False
[PROOFSTEP]
exact not_inr_lt_inl hab
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a b : _root_.Lex (α ⊕ β)
⊢ a ≤ b ∧ ¬b ≤ a → a < b
[PROOFSTEP]
rintro ⟨⟨hab⟩ | ⟨hab⟩ | ⟨a, b⟩, hba⟩
[GOAL]
case refine'_2.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a₁✝ a₂✝ : α
hab : a₁✝ ≤ a₂✝
hba : ¬inl a₂✝ ≤ inl a₁✝
⊢ inl a₁✝ < inl a₂✝
[PROOFSTEP]
exact Lex.inl (hab.lt_of_not_le fun h => hba <| Lex.inl h)
[GOAL]
case refine'_2.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
b₁✝ b₂✝ : β
hab : b₁✝ ≤ b₂✝
hba : ¬inr b₂✝ ≤ inr b₁✝
⊢ inr b₁✝ < inr b₂✝
[PROOFSTEP]
exact Lex.inr (hab.lt_of_not_le fun h => hba <| Lex.inr h)
[GOAL]
case refine'_2.intro.sep
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
src✝¹ : LE (_root_.Lex (α ⊕ β)) := Lex.LE
src✝ : LT (_root_.Lex (α ⊕ β)) := Lex.LT
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b
[PROOFSTEP]
exact Lex.sep _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
⊢ ∀ (a : _root_.Lex (α ⊕ β)), ⊥ ≤ a
[PROOFSTEP]
rintro (a | b)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
a : α
⊢ ⊥ ≤ inl a
[PROOFSTEP]
exact Lex.inl bot_le
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
b : β
⊢ ⊥ ≤ inr b
[PROOFSTEP]
exact Lex.sep _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
⊢ ∀ (a : _root_.Lex (α ⊕ β)), a ≤ ⊤
[PROOFSTEP]
rintro (a | b)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
a : α
⊢ inl a ≤ ⊤
[PROOFSTEP]
exact Lex.sep _ _
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
b : β
⊢ inr b ≤ ⊤
[PROOFSTEP]
exact Lex.inr le_top
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a✝ : α✝
b✝ : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
a b : (α ⊕ β) ⊕ γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        a ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    a ≤ b
[PROOFSTEP]
rcases a with ((_ | _) | _)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b✝ : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
b : (α ⊕ β) ⊕ γ
val✝ : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inl (inl val✝) ≤ b
[PROOFSTEP]
rcases b with ((_ | _) | _)
[GOAL]
case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b✝ : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
b : (α ⊕ β) ⊕ γ
val✝ : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inl (inr val✝) ≤ b
[PROOFSTEP]
rcases b with ((_ | _) | _)
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b✝ : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
b : (α ⊕ β) ⊕ γ
val✝ : γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inr val✝ ≤ b
[PROOFSTEP]
rcases b with ((_ | _) | _)
[GOAL]
case inl.inl.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ val✝ : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝)) ↔
    inl (inl val✝¹) ≤ inl (inl val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inl.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : α
val✝ : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝)) ↔
    inl (inl val✝¹) ≤ inl (inr val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : α
val✝ : γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝) ↔
    inl (inl val✝¹) ≤ inr val✝
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inr.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : β
val✝ : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝)) ↔
    inl (inr val✝¹) ≤ inl (inl val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inr.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ val✝ : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝)) ↔
    inl (inr val✝¹) ≤ inl (inr val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inl.inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : β
val✝ : γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝¹)) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝) ↔
    inl (inr val✝¹) ≤ inr val✝
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inr.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : γ
val✝ : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝¹) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inl val✝)) ↔
    inr val✝¹ ≤ inl (inl val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inr.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ : γ
val✝ : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝¹) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl (inr val✝)) ↔
    inr val✝¹ ≤ inl (inr val✝)
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
inst✝⁵ : LE α✝
inst✝⁴ : LE β✝
inst✝³ : LE γ✝
a : α✝
b : β✝
c : γ✝
α : Type u_5
β : Type u_6
γ : Type u_7
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
src✝ : (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γ := Equiv.sumAssoc α β γ
val✝¹ val✝ : γ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝¹) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr val✝) ↔
    inr val✝¹ ≤ inr val✝
[PROOFSTEP]
simp [Equiv.sumAssoc]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a : α✝
b : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
⊢ ∀ {a b : (α ⊕ β)ᵒᵈ},
    ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          a ≤
        ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          b ↔
      a ≤ b
[PROOFSTEP]
rintro (a | a) (b | b)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inl a ≤ inl b
[PROOFSTEP]
change inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a b : α
⊢ inl (↑toDual a) ≤ inl (↑toDual b) ↔ ↑toDual (inl a) ≤ ↑toDual (inl b)
[PROOFSTEP]
simp [toDual_le_toDual, inl_le_inl_iff]
[GOAL]
case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a : α
b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inl a ≤ inr b
[PROOFSTEP]
exact iff_of_false (@not_inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _) not_inr_le_inl
[GOAL]
case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a : β
b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inr a ≤ inl b
[PROOFSTEP]
exact iff_of_false (@not_inr_le_inl (OrderDual α) (OrderDual β) _ _ _ _) not_inl_le_inr
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inr a ≤ inr b
[PROOFSTEP]
change inr (toDual a) ≤ inr (toDual b) ↔ toDual (inr a) ≤ toDual (inr b)
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : (α ⊕ β)ᵒᵈ ≃ (α ⊕ β)ᵒᵈ := Equiv.refl (α ⊕ β)ᵒᵈ
a b : β
⊢ inr (↑toDual a) ≤ inr (↑toDual b) ↔ ↑toDual (inr a) ≤ ↑toDual (inr b)
[PROOFSTEP]
simp [toDual_le_toDual, inr_le_inr_iff]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : (_root_.Lex (α ⊕ β))ᵒᵈ
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        a ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    a ≤ b
[PROOFSTEP]
rcases a with (a | a)
[GOAL]
case inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
b : (_root_.Lex (α ⊕ β))ᵒᵈ
a : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inl a ≤ b
[PROOFSTEP]
rcases b with (b | b)
[GOAL]
case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
b : (_root_.Lex (α ⊕ β))ᵒᵈ
a : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        b ↔
    inr a ≤ b
[PROOFSTEP]
rcases b with (b | b)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inl a ≤ inl b
case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a : α
b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inl a ≤ inr b
case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a : β
b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inr a ≤ inl b
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inr a ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : α
⊢ inr a ≤ inr b ↔ inl a ≤ inl b
[PROOFSTEP]
change toLex (inr <| toDual a) ≤ toLex (inr <| toDual b) ↔ toDual (toLex <| inl a) ≤ toDual (toLex <| inl b)
[GOAL]
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : α
⊢ ↑toLex (inr (↑toDual a)) ≤ ↑toLex (inr (↑toDual b)) ↔ ↑toDual (↑toLex (inl a)) ≤ ↑toDual (↑toLex (inl b))
[PROOFSTEP]
simp [toDual_le_toDual, Lex.inl_le_inl_iff, Lex.inr_le_inr_iff]
[GOAL]
case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a : α
b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inl a ≤ inr b
[PROOFSTEP]
exact iff_of_false (@Lex.not_inr_le_inl (OrderDual β) (OrderDual α) _ _ _ _) Lex.not_inr_le_inl
[GOAL]
case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a : β
b : α
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inl b) ↔
    inr a ≤ inl b
[PROOFSTEP]
exact iff_of_true (@Lex.inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _) (Lex.inl_le_inr _ _)
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : β
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr a) ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (inr b) ↔
    inr a ≤ inr b
[PROOFSTEP]
change toLex (inl <| toDual a) ≤ toLex (inl <| toDual b) ↔ toDual (toLex <| inr a) ≤ toDual (toLex <| inr b)
[GOAL]
case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : LE α✝
inst✝³ : LE β✝
inst✝² : LE γ
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
src✝ : α ⊕ β ≃ β ⊕ α := Equiv.sumComm α β
a b : β
⊢ ↑toLex (inl (↑toDual a)) ≤ ↑toLex (inl (↑toDual b)) ↔ ↑toDual (↑toLex (inr a)) ≤ ↑toDual (↑toLex (inr b))
[PROOFSTEP]
simp [toDual_le_toDual, Lex.inl_le_inl_iff, Lex.inr_le_inr_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
a b : WithBot α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) a ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) b ↔
    a ≤ b
[PROOFSTEP]
rcases a with (a | _)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
b : WithBot α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) b ↔
    none ≤ b
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
b : WithBot α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝) ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) b ↔
    Option.some val✝ ≤ b
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ↔
    none ≤ none
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝) ↔
    none ≤ Option.some val✝
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝) ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) none ↔
    Option.some val✝ ≤ none
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝¹ val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝¹) ≤
      ↑((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) (Option.some val✝) ↔
    Option.some val✝¹ ≤ Option.some val✝
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ¬Option.some val✝ ≤ none
[PROOFSTEP]
exact not_coe_le_bot _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
a b : WithTop α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) a ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) b ↔ a ≤ b
[PROOFSTEP]
rcases a with (a | _)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
b : WithTop α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) b ↔ none ≤ b
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
b : WithTop α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝) ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) b ↔
    Option.some val✝ ≤ b
[PROOFSTEP]
rcases b with (b | _)
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ↔ none ≤ none
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝) ↔
    none ≤ Option.some val✝
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝) ≤ ↑((Equiv.optionEquivSumPUnit α).trans toLex) none ↔
    Option.some val✝ ≤ none
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝¹ val✝ : α
⊢ ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝¹) ≤
      ↑((Equiv.optionEquivSumPUnit α).trans toLex) (Option.some val✝) ↔
    Option.some val✝¹ ≤ Option.some val✝
[PROOFSTEP]
simp [swap, Equiv.optionEquivSumPUnit]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : LE α
val✝ : α
⊢ ¬none ≤ Option.some val✝
[PROOFSTEP]
exact not_top_le_coe _
