case inl
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x

case inr.intro
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
⊢ x ≤ y ∨ y ≤ x
rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x
case inr.intro
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x
right
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x
intro b' h₁
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
rw [Part.eq_some_iff] at h₀
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
have hx := hx _ h₀
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
hy : b' ∈ z
⊢ b' ∈ x
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x
have hy := hy _ h₁
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx✝¹ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx✝ : b ∈ z
hy : b' ∈ z
hx : b = b'
⊢ b' ∈ x
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
hy : b' ∈ z
⊢ b' ∈ x
have hx := Part.mem_unique hx hy
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
hx : b ∈ z
h₁ : b ∈ y
hy : b ∈ z
⊢ b ∈ x
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx✝¹ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx✝ : b ∈ z
hy : b' ∈ z
hx : b = b'
⊢ b' ∈ x
subst hx
no goals
case inr.intro.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
hx : b ∈ z
h₁ : b ∈ y
hy : b ∈ z
⊢ b ∈ x
exact h₀
case inl
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none
case inl
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x
rw [h]
case inl.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y
case inl
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none
left
no goals
case inl.h
α : Type u_1
β : Type ?u.12580
γ : Type ?u.12583
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y
apply OrderBot.bot_le _