carlesonSum_𝔓pos_inter_ℭ₂_eq_add_sum

lemma carlesonSum_𝔓pos_inter_ℭ₂_eq_add_sum {f : X → ℂ} {x : X} (hkn : k ≤ n) (hj : j ≤ 2 * n + 3) :    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  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 [mem_inter_iff, mem_compl_iff,      Finset.mem_Iic, mem_iUnion, exists_and_left, exists_prop]    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩    · refine ⟨h.1.1, ?_⟩      simp only [𝔓₁, mem_iUnion, exists_prop, not_exists, not_and] at h      have := (notMem_ℭ₅_iff_mem_𝔏₃ (X := X) hkn hj h.1.1.1 h.1.2 h.2).1 (h.1.1.2 n k hkn j hj)      simp only [mem_iUnion, exists_prop] at this      exact this    · rcases h.2 with ⟨l, lZ, hl⟩      exact ⟨⟨h.1, ℭ₃_subset_ℭ₂ (maxLayer_subset hl)⟩,        disjoint_right.1 𝔏₂_disjoint_ℭ₃ (maxLayer_subset hl)⟩