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 : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ insert f ↑u ⊆ T (max s s')
no goals