case intro.intro
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Disjoint atBot atTop
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
⊢ Disjoint atBot atTop
rcases exists_pair_ne α with ⟨x, y, hne⟩
case pos
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop

case neg
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop
case intro.intro
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Disjoint atBot atTop
by_cases hle : x ≤ y
case pos
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)
case pos
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop
refine' disjoint_of_disjoint_of_mem _ (Iic_mem_atBot x) (Ici_mem_atTop y)
no goals
case pos
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)
exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_le
case neg
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint (Iic y) (Ici x)
case neg
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop
refine' disjoint_of_disjoint_of_mem _ (Iic_mem_atBot y) (Ici_mem_atTop x)
no goals
case neg
ι : Type ?u.4780
ι' : Type ?u.4783
α : Type u_1
β : Type ?u.4789
γ : Type ?u.4792
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint (Iic y) (Ici x)
exact Iic_disjoint_Ici.2 hle