C6_forest

lemma C6_forest : ℭ₆ (X := X) k n j = ⋃ u ∈ 𝔘₃ k n j, 𝔗₂ k n j u := by  ext p; constructor <;> intro h  · have hp : p ∈ ℭ₃ k n j := (ℭ₆_subset_ℭ₅ |>.trans ℭ₅_subset_ℭ₄ |>.trans ℭ₄_subset_ℭ₃) h    rw [ℭ₃, mem_sdiff, 𝔏₂, mem_setOf] at hp    have mp := hp.1    simp_rw [hp.1, true_and, not_not] at hp    obtain ⟨u, mu, np, sl⟩ := hp    have mp' : p ∈ 𝔗₁ k n j u := by      rw [𝔗₁, mem_setOf]; exact ⟨ℭ₂_subset_ℭ₁ mp, np, sl⟩    have mu' : u ∈ 𝔘₂ k n j := by      rw [𝔘₂, mem_setOf]; exact ⟨mu, not_disjoint_iff.mpr ⟨_, mp', h⟩⟩    let rr := equivalenceOn_urel (X := X) (k := k) (n := n) (j := j)    rw [mem_iUnion₂]; use rr.out u, (rr.out_mem_reprs mu')    refine ⟨h, ?_⟩; rw [mem_iUnion₂]; use u, mu'; rw [mem_iUnion]; use rr.out_rel mu'  · rw [mem_iUnion₂] at h; obtain ⟨_, _, mp, _⟩ := h; exact mp