α : Type u_1
β : Type ?u.72368
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b
α : Type u_1
β : Type ?u.72368
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b
refine' ⟨fun h => _, fun h => Ioi_subset_Ioi h⟩
α : Type u_1
β : Type ?u.72368
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False
α : Type u_1
β : Type ?u.72368
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b
by_contra ba
no goals
α : Type u_1
β : Type ?u.72368
inst✝ : LinearOrder α
a a₁ a₂ b b₁ b₂ c d : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False
exact lt_irrefl _ (h (not_le.mp ba))