biSup_Θ'_eq_biSup_enumΘ'

lemma biSup_Θ'_eq_biSup_enumΘ' {x : X} :    ⨆ θ ∈ Θ' X, g θ x = ⨆ n, ⨆ i ∈ Finset.range (n + 1), g (enumΘ' nΘ' i) x := by  apply le_antisymm  · refine iSup₂_le fun θ mθ ↦ ?_    obtain ⟨n, hn⟩ := surjective_enumΘ' nΘ' ⟨θ, mθ⟩    have eg : g θ x = g (enumΘ' nΘ' n).1 x := by simp [hn]    rw [eg]    calc      _ ≤ ⨆ i ∈ Finset.range (n + 1), g (enumΘ' nΘ' i) x := by        have : n ∈ Finset.range (n + 1) := by rw [Finset.mem_range]; lia        convert! le_iSup₂ _ this; rfl      _ ≤ _ := le_iSup_iff.mpr fun _ a ↦ a n  · refine iSup_le fun n ↦ iSup₂_le fun i mi ↦ ?_    obtain ⟨θ, mθ⟩ := enumΘ' nΘ' i; apply le_iSup₂ _ mθ