Theorem: IsTotal.directed' (Sion/Semicontinuous.lean)

State before:
α : Type u_1
ι : Sort u_2
r : α → α → Prop
inst✝ : IsTotal α r
f : ι → α
i j : ι
⊢ ∃ z, r (f i) (f z) ∧ r (f j) (f z)
Tactic:
cases (total_of r (f i) (f j)) with
| inl h => exact ⟨j, h, refl _⟩
| inr h => exact ⟨i, refl _, h⟩
State after:
no goals

State before:
case inl
α : Type u_1
ι : Sort u_2
r : α → α → Prop
inst✝ : IsTotal α r
f : ι → α
i j : ι
h : r (f i) (f j)
⊢ ∃ z, r (f i) (f z) ∧ r (f j) (f z)
Tactic:
exact ⟨j, h, refl _⟩
State after:
no goals

State before:
case inr
α : Type u_1
ι : Sort u_2
r : α → α → Prop
inst✝ : IsTotal α r
f : ι → α
i j : ι
h : r (f j) (f i)
⊢ ∃ z, r (f i) (f z) ∧ r (f j) (f z)
Tactic:
exact ⟨i, refl _, h⟩
State after:
no goals