-- Mathlib/Data/Part.lean
theorem le_total_of_le_of_le {x y : Part α} (z : Part α) (hx : x ≤ z) (hy : y ≤ z) :
    x ≤ y ∨ y ≤ x

Proof state:
case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x

Tactic:
rw [h]

Result:
case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none

Proof state:
case inr.intro
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x

Tactic:
right

Result:
case inr.intro.h
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x

Proof state:
case inr.intro.h
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x

Tactic:
rw [Part.eq_some_iff] at h₀

Result:
case inr.intro.h
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x

Proof state:
case inr.intro.h
α : Type u_1
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

Tactic:
exact h₀

Result:
no goals

Proof state:
case inr.intro.h
α : Type u_1
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

Tactic:
have hx := Part.mem_unique hx hy

Result:
case inr.intro.h
α : Type u_1
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

Proof state:
case inr.intro.h
α : Type u_1
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

Tactic:
subst hx

Result:
case inr.intro.h
α : Type u_1
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

Proof state:
case inr.intro.h
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x

Tactic:
intro b' h₁

Result:
case inr.intro.h
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x

Proof state:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
⊢ x ≤ y ∨ y ≤ x

Tactic:
rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)

Result:
case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x

case inr.intro
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x

Proof state:
case inr.intro.h
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x

Tactic:
have hx := hx _ h₀

Result:
case inr.intro.h
α : Type u_1
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x

Proof state:
case inl.h
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y

Tactic:
apply OrderBot.bot_le _

Result:
no goals

Proof state:
case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none

Tactic:
left

Result:
case inl.h
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y

Proof state:
case inr.intro.h
α : Type u_1
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x

Tactic:
have hy := hy _ h₁

Result:
case inr.intro.h
α : Type u_1
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