[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_gt a
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
x✝ : α × β
a : α
b : β
c : α
h : a < c
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_gt b
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
x✝ : α × β
a : α
b c : β
h : b < c
⊢ ∃ b_1, (a, b) < b_1
[PROOFSTEP]
exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_lt a
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
c : α
h : c < a
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
obtain ⟨c, h⟩ := exists_lt b
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
x✝ : α × β
a : α
b c : β
h : c < b
⊢ ∃ b_1, b_1 < (a, b)
[PROOFSTEP]
exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMaxOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, a < b
[PROOFSTEP]
classical
obtain ⟨b, hb⟩ := exists_gt (a <| Classical.arbitrary _)
exact ⟨_, lt_update_self_iff.2 hb⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMaxOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, a < b
[PROOFSTEP]
obtain ⟨b, hb⟩ := exists_gt (a <| Classical.arbitrary _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMaxOrder (π i)
a : (i : ι) → π i
b : π (Classical.arbitrary ι)
hb : a (Classical.arbitrary ι) < b
⊢ ∃ b, a < b
[PROOFSTEP]
exact ⟨_, lt_update_self_iff.2 hb⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, b < a
[PROOFSTEP]
classical
obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
exact ⟨_, update_lt_self_iff.2 hb⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, b < a
[PROOFSTEP]
obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
b : π (Classical.arbitrary ι)
hb : b < a (Classical.arbitrary ι)
⊢ ∃ b, b < a
[PROOFSTEP]
exact ⟨_, update_lt_self_iff.2 hb⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoBotOrder α
a : α
⊢ ∃ b, b < a
[PROOFSTEP]
simpa [not_le] using exists_not_ge a
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoTopOrder α
a : α
⊢ ∃ b, a < b
[PROOFSTEP]
simpa [not_le] using exists_not_le a
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬IsMin a ↔ ∃ b, b < a
[PROOFSTEP]
simp [lt_iff_le_not_le, IsMin, not_forall, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Preorder α
a b : α
⊢ ¬IsMax a ↔ ∃ b, a < b
[PROOFSTEP]
simp [lt_iff_le_not_le, IsMax, not_forall, exists_prop]
