α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : (fun x => β) a
ha : ↑f a < c
hb : c < ↑f b
⊢ False
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
⊢ ↑f a ⩿ ↑f b
refine' ⟨f.monotone hab.le, fun c ha hb => _⟩
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : α
ha : ↑f a < ↑f c
hb : ↑f c < ↑f b
⊢ False
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : (fun x => β) a
ha : ↑f a < c
hb : c < ↑f b
⊢ False
obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : α
ha : a < c
hb : c < b
⊢ False
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : α
ha : ↑f a < ↑f c
hb : ↑f c < ↑f b
⊢ False
rw [f.lt_iff_lt] at ha hb
no goals
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : α
ha : a < c
hb : c < b
⊢ False
exact hab.2 ha hb