ordConnected_C4

lemma ordConnected_C4 : OrdConnected (ℭ₄ k n j : Set (𝔓 X)) := by  rw [ordConnected_def]; intro p mp p'' mp'' p' mp'  have mp''₁ := mem_of_mem_of_subset mp'' ℭ₄_subset_ℭ₃  have mp'₁ : p' ∈ ℭ₃ (X := X) k n j := mem_of_mem_of_subset mp'    (ordConnected_C3.out (mem_of_mem_of_subset mp ℭ₄_subset_ℭ₃) mp''₁)  by_cases e : p' = p''; · rwa [← e] at mp''  simp_rw [ℭ₄, layersBelow, mem_sdiff, mp'₁, true_and]  by_contra h; simp_rw [mem_iUnion] at h; obtain ⟨l', hl', p'm⟩ := h  rw [maxLayer_def, mem_setOf, maximal_iff] at p'm  simp_rw [mem_sdiff] at p'm  have p''nm : p'' ∉ ⋃ l'', ⋃ (_ : l'' < l'), 𝔏₃ k n j l'' := by    replace mp'' := mp''.2; contrapose! mp''    refine mem_of_mem_of_subset mp'' <| iUnion₂_mono' fun i hi ↦ ⟨i, hi.le.trans hl', subset_rfl⟩  exact absurd (p'm.2 ⟨mp''₁, p''nm⟩ mp'.2) e