cases (total_of r (f i) (f j)) with
| inl h => exact ⟨j, h, refl _⟩
| inr h => exact ⟨i, refl _, h⟩
α : 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)
no goals