no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a : (_ : Fin n) × Fin n
⊢ a ∈ finPairsLT n ↔ a.snd < a.fst
simp only [finPairsLT, Fin.lt_iff_val_lt_val, true_and_iff, mem_attachFin, mem_range, mem_univ,
  mem_sigma]