Antichain.exists_larger_grid

lemma exists_larger_grid : ∃ (L' : Grid X), L ≤ L' ∧ s L' = s L + 1 := by  classical  obtain ⟨p, hp⟩ : ∃ (p : 𝔄' 𝔄 ϑ N), L ≤ 𝓘 (p : 𝔓 X) := exists_p'_ge_L hL  set SL : Finset (𝔓 X) := (SL 𝔄 ϑ N L).toFinset with SL_def  have hSL : SL.Nonempty := SL_nonempty hL  set q := p' hL  have hq' : q ∈ SL := ((Finset.exists_minimalFor 𝔰 SL (SL_nonempty hL)).choose_spec).1  simp only [defaultA, Antichain.SL, SL] at hq'  have hqL : ¬ 𝓘 q ≤ L := not_I_p'_le_L hL  simp only [Grid.le_def, not_and_or, not_le] at hqL  have : s L < 𝔰 q  := s_L_le_s_p' hL  have hS : s L < s topCube (X := X) := by    conv_rhs => simp only [s, s_topCube]    exact lt_of_lt_of_le this scale_mem_Icc.2  exact Grid.exists_scale_succ (X := X) hS