Set.minLayer_eq_setOf_height

lemma minLayer_eq_setOf_height : A.minLayer n = {x | ∃ hx : x ∈ A, height (⟨x, hx⟩ : A) = n} := by  induction n using Nat.strongRec with  | ind n ih =>    ext x    simp only [mem_setOf_eq]    wlog hxs : x ∈ A    · simp only [hxs, IsEmpty.exists_iff, iff_false]      contrapose! hxs; exact minLayer_subset hxs    simp only [hxs, exists_true_left]    rw [minLayer]    simp_rw [height_eq_coe_iff_minimal_le_height]    simp +contextual only [ih]; clear ih    have : Minimal (n ≤ height ·) (⟨x, hxs⟩ : A) ↔        Minimal (· ∈ {y | n ≤ height y}) (⟨x, hxs⟩ : A) := Eq.to_iff rfl    rw [this, subtype_mk_minimal_iff, mem_setOf]    congr! 2 with y    wlog hys : y ∈ A    · simp [hys]    simp only [mem_sdiff, hys, mem_iUnion, exists_prop, not_exists, not_and, true_and, mem_setOf_eq,      exists_true_left]    cases height (⟨y, hys⟩ : A)    · simp    · simp only [Nat.cast_inj, Nat.cast_le]      exact ⟨fun h ↦ by contrapose! h; simp [h], fun h m hm ↦ by lia⟩