no goals
α : Type u
R : α → α → Prop
n : ℕ
f : Fin n → α
⊢ Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)
simp only [pairwise_iff_get, (Fin.cast (length_ofFn f)).surjective.forall, get_ofFn,
  OrderIso.lt_iff_lt]