carlesonSum_𝔓pos_inter_ℭ₁_eq_add_sum

lemma carlesonSum_𝔓pos_inter_ℭ₁_eq_add_sum {f : X → ℂ} {x : X} :    carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ₁ k n j) f x =      carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ₂ k n j) f x      + ∑ l ≤ Z * (n + 1), carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₁ k n j l) f x := by  classical  conv_lhs => rw [← carlesonSum_inter_add_inter_compl _ (ℭ₂ k n j)]  rw [sum_carlesonSum_of_pairwiseDisjoint]; swap  · apply PairwiseDisjoint.subset _ (subset_univ _)    have : univ.PairwiseDisjoint fun l ↦ 𝔏₁ (X := X) k n j l := pairwiseDisjoint_minLayer    apply this.mono    intro j    exact inter_subset_right  congr 2  · ext p    simp only [mem_inter_iff, mem_compl_iff, and_congr_left_iff, and_iff_left_iff_imp, and_imp]    intro hp    exact fun _ _ ↦ mem_of_mem_inter_left hp  · ext p    simp only [ℭ₂, layersAbove, mem_inter_iff, mem_compl_iff, mem_sdiff, mem_iUnion, exists_prop,      not_exists, not_and, not_forall, Decidable.not_not, Finset.mem_Iic, 𝔏₁]    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩    · obtain ⟨i, hi, hmem⟩ := h.2 h.1.2      exact ⟨i, hi, h.1.1, hmem⟩    · rcases h with ⟨i, hi, h'i⟩      simp only [h'i.1, not_false_eq_true, and_self, minLayer_subset h'i.2, forall_const, true_and]      exact ⟨i, hi, h'i.2⟩