no goals
α : Type ?u.136300
β : Type ?u.136303
γ : Type ?u.136306
n : ℕ
s : Finset ℕ
a : ℕ
ha : a < n
⊢ { val := a, isLt := ha } ∈ Finset.fin n s ↔ ↑{ val := a, isLt := ha } ∈ s
simp [Finset.fin, ha, and_comm]