case intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
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

case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
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
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
obtain ⟨c | c, ha, hb⟩ := @exists_between (Sum α β) _ _ _ _ (inl_lt_inl_iff.2 h)
no goals
case intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
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
exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩
no goals
case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
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
exact (not_inl_lt_inr ha).elim
case intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
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

case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
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
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
obtain ⟨c | c, ha, hb⟩ := @exists_between (Sum α β) _ _ _ _ (inr_lt_inr_iff.2 h)
no goals
case intro.inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
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
exact (not_inl_lt_inr hb).elim
no goals
case intro.inr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.17805
δ : Type ?u.17808
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
exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩