stackSize_le_one_of_pairwiseDisjoint

lemma stackSize_le_one_of_pairwiseDisjoint {C : Set (𝔓 X)} {x : X}    (h : C.PairwiseDisjoint (fun p ↦ (𝓘 p : Set X))) : stackSize C x ≤ 1 := by  by_cases hx : ∃ p ∈ C, x ∈ (𝓘 p : Set X)  · rcases hx with ⟨p, pC, hp⟩    rw [stackSize, Finset.sum_eq_single_of_mem p]; rotate_left    · simp [pC]    · intro b hb hbp      simp only [indicator_apply_eq_zero, Pi.one_apply, one_ne_zero, imp_false]      simp only [Finset.mem_filter_univ] at hb      exact disjoint_left.1 (h pC hb hbp.symm) hp    simp [hp]  · have : stackSize C x = 0 := by      apply Finset.sum_eq_zero (fun p hp ↦ ?_)      simp only [Finset.mem_filter_univ, not_exists, not_and,        indicator_apply_eq_zero, Pi.one_apply, one_ne_zero, imp_false] at hp hx ⊢      exact hx _ hp    linarith