Set.iUnion_lt_minLayer_iff_bounded_series

lemma iUnion_lt_minLayer_iff_bounded_series :    ⋃ (k < n), A.minLayer k = A ↔ ∀ p : LTSeries A, p.length < n := by  refine ⟨fun h p ↦ ?_, fun hlength ↦ ?_⟩  · have hx : p.last.1 ∈ ⋃ (k < n), A.minLayer k := h.symm ▸ p.last.2    simp only [minLayer_eq_setOf_height] at hx    push _ ∈ _ at hx    simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const] at hx    obtain ⟨i, hix, hi⟩ := hx    have hh := length_le_height_last (p := p)    rw [hi, Nat.cast_le] at hh    exact hh.trans_lt hix  · ext x    simp only [minLayer_eq_setOf_height]; push _ ∈ _    wlog hxs : x ∈ A; · simp [hxs]    simp only [hxs, exists_true_left, iff_true]    suffices height (⟨x, hxs⟩ : A) < n by      revert this      cases height (⟨x, hxs⟩ : A) <;> simp    cases n with    | zero =>      specialize hlength (RelSeries.singleton _ ⟨x, hxs⟩)      simp at hlength    | succ n =>      simp only [Nat.lt_succ_iff] at hlength      apply lt_of_le_of_lt (b := ↑n) _ (mod_cast lt_add_one n)      exact iSup_le fun _ ↦ by simp [hlength]