TileStructure.Forest.stackSize_remainder_ge_one_of_exists

lemma stackSize_remainder_ge_one_of_exists (t : Forest X n) (j : ℕ) (x : X)    (hx : ∃ 𝔲' ∈ (t.rowDecomp j).𝔘, x ∈ 𝓘 𝔲') :    1 ≤ stackSize ((t \ ⋃ i < j, t.rowDecomp i) ∩ t.rowDecomp j: Set _) x := by  classical  obtain ⟨𝔲', h𝔲'⟩ := hx  calc 1      = stackSize {𝔲'} x := by        rw [stackSize, Finset.sum_eq_single_of_mem]        · exact (Set.indicator_of_mem h𝔲'.2 (1 : X → ℕ)).symm        · rw [Finset.mem_filter_univ]          exact Set.mem_singleton_iff.mpr rfl        · intro b hb hbp          rw [Finset.mem_filter_univ, Set.mem_singleton_iff] at hb          exact absurd hb hbp    _ ≤ stackSize ((t \ ⋃ i < j, t.rowDecomp i) ∩ t.rowDecomp j : Set _) x :=        stackSize_mono (Set.singleton_subset_iff.mpr ⟨t.rowDecomp_𝔘_subset j h𝔲'.1, h𝔲'.1⟩)