Alt Set eq upcrossings Before

lemma altSet_eq_upcrossingsBefore (hab : a < b) :    altSet X F a b m = {ω | m ≤ upcrossingsBefore a b (fun k ↦ X (finIdx F t k)) #F ω} := by  refine subset_antisymm ?_ ?_  · rintro ω ⟨c, hc1, hc2, hca, hcb⟩    have hex : ∀ i, i < 2 * m → ∃ k, k < #F ∧ finIdx F t k = c i :=      fun i hi ↦ exists_finIdx_eq (hc2 i hi)    let c' : ℕ → ℕ := fun i ↦ if hi : i < 2 * m then (hex i hi).choose else 0    have hc'spec : ∀ i (hi : i < 2 * m), c' i < #F ∧ finIdx F t (c' i) = c i := by grind    refine le_upcrossingsBefore_of_alternating hab (c := c') ?_ (by grind) ?_ ?_    · intro i hi      obtain ⟨hlt1, heq1⟩ := hc'spec i (by lia)      obtain ⟨hlt2, heq2⟩ := hc'spec (i + 1) hi      rw [← finIdx_lt_finIdx_iff (t := t) hlt1 hlt2, heq1, heq2]      exact hc1 i hi    · intro i hi      obtain ⟨_, heq⟩ := hc'spec (2 * i) (by lia)      simp only [heq]      exact hca i hi    · intro i hi      obtain ⟨_, heq⟩ := hc'spec (2 * i + 1) (by lia)      simp only [heq]      exact hcb i hi  · intro ω hω    obtain ⟨c, hmono, hcN, ha, hb⟩ := exists_alternating_of_le_upcrossingsBefore hab hω    exact ⟨fun i ↦ finIdx F t (c i), fun i hi ↦ finIdx_lt_of_lt (hmono i hi) (hcN (i + 1) hi),      fun i hi ↦ finIdx_mem (hcN i hi), fun i hi ↦ ha i hi, fun i hi ↦ hb i hi⟩