have : ∃ s', f ∈ T s' := by simpa using (Set.insert_subset_iff.mp hu).1
case intro
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 : ℕ
hs : ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
case intro
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 : ℕ
hs : ↑u ⊆ T s
this : ∃ s', f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s