Set.exists_le_in_minLayer_of_le

lemma exists_le_in_minLayer_of_le (ha : a ∈ A.minLayer n) (hm : m ≤ n) :    ∃ c ∈ A.minLayer m, c ≤ a := by  induction n, hm using Nat.le_induction generalizing a with  | base => use a  | succ n _ ih =>    have nma : a ∉ A.minLayer n :=      disjoint_right.mp (disjoint_minLayer_of_ne (by lia)) ha    rw [minLayer, mem_setOf, minimal_iff] at ha nma    have al : a ∈ A \ ⋃ (l < n), A.minLayer l := by      have : a ∈ A \ ⋃ (k < n + 1), A.minLayer k := ha.1      push (_ ∈ _) at this ⊢; push Not at this ⊢      exact ⟨this.1, fun l hl h ↦ this.2 l (Nat.lt_succ_of_lt hl) h⟩    simp_rw [al, true_and] at nma; push Not at nma; obtain ⟨a', ha', la⟩ := nma    have ma' : a' ∈ A.minLayer n := by      by_contra h      have a'l : a' ∈ A \ ⋃ (l < n + 1), A.minLayer l := by        have : ∀ l, l < n + 1 ↔ l < n ∨ l = n := by lia        simp_all [iUnion_or, iUnion_union_distrib]      exact absurd (ha.2 a'l la.1) (ne_eq _ _ ▸ la.2)    obtain ⟨c, mc, lc⟩ := ih ma'; use c, mc, lc.trans la.1