case insert f u _ ih =>
  simp at hu
  have : ∃ s, ↑u ⊆ T s := ih (subset_trans (Set.subset_insert _ _) hu)
  rcases this with ⟨s, hs⟩
  have : ∃ s', f ∈ T s' := by simpa using (Set.insert_subset_iff.mp hu).1
  rcases this with ⟨s', hs'⟩
  exact ⟨max s s', by
    simp; exact Set.insert_subset
      (subset_of_le H (Nat.le_max_right s s') hs')
      (subset_trans hs (subset_of_le H $ Nat.le_max_left s s'))⟩
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : ↑(insert f u) ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
no goals