α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ ¬a ∈ s → s ∈ 𝒜 ∧ ¬a ∈ s
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ s ∈ Finset.memberSubfamily a 𝒜 → s ∈ Finset.nonMemberSubfamily a 𝒜
rw [mem_memberSubfamily, mem_nonMemberSubfamily]
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ ¬a ∈ s → s ∈ 𝒜 ∧ ¬a ∈ s
exact And.imp_left (h <| subset_insert _ _)