case intro.inl
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : α
h : inl b < inl a
⊢ ∃ b, b < a

case intro.inr
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
b : β
h : inr b < inl a
⊢ ∃ b, b < a
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
⊢ ∃ b, b < a
obtain ⟨b | b, h⟩ := exists_lt (inl a : Sum α β)
no goals
case intro.inl
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : α
h : inl b < inl a
⊢ ∃ b, b < a
exact ⟨b, inl_lt_inl_iff.1 h⟩
no goals
case intro.inr
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
b : β
h : inr b < inl a
⊢ ∃ b, b < a
exact (not_inr_lt_inl h).elim
case intro.inl
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ b, b < a

case intro.inr
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : β
h : inr b < inr a
⊢ ∃ b, b < a
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
⊢ ∃ b, b < a
obtain ⟨b | b, h⟩ := exists_lt (inr a : Sum α β)
no goals
case intro.inl
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ b, b < a
exact (not_inl_lt_inr h).elim
no goals
case intro.inr
α : Type u_1
β : Type u_2
γ : Type ?u.14611
δ : Type ?u.14614
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a b : β
h : inr b < inr a
⊢ ∃ b, b < a
exact ⟨b, inr_lt_inr_iff.1 h⟩