Set.exists_le_in_layersAbove_of_le

lemma exists_le_in_layersAbove_of_le [Finite α] (ha : a ∈ A.layersAbove n) (hm : m ≤ n) :    ∃ c ∈ A.minLayer m, c ≤ a := by  classical  have ma : a ∈ A \ ⋃ (l' < n), A.minLayer l' := by    simp only [layersAbove] at ha ⊢    push _ ∈ _ at ha ⊢; push Not at ha ⊢    exact ⟨ha.1, fun l' hl' h ↦ ha.2 l' hl'.le h⟩  have := Fintype.ofFinite α  let C : Finset α :=    (A.toFinset \ (Finset.range n).biUnion fun l ↦ (A.minLayer l).toFinset).filter (· ≤ a)  have Cn : C.Nonempty := by use a; simp_all [C]  obtain ⟨a', ma', mina'⟩ := C.exists_minimal Cn  simp_rw [C, Finset.mem_filter, Finset.mem_sdiff, Finset.mem_biUnion, Finset.mem_range, not_exists,    not_and, mem_toFinset] at ma' mina'  conv at mina' => enter [x]; rw [and_imp]  have ma'₁ : a' ∈ A.minLayer n := by    rw [minLayer, mem_setOf, minimal_iff]    push _ ∈ _; push Not    exact ⟨ma'.1, fun y hy ly ↦ le_antisymm (mina' hy (ly.trans ma'.2) ly) ly⟩  obtain ⟨c, mc, lc⟩ := exists_le_in_minLayer_of_le ma'₁ hm  use c, mc, lc.trans ma'.2