have : ∃ s, ↑u ⊆ T s := ih (subset_trans (Set.subset_insert _ _) hu)
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
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
this : ∃ s, ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s