α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ 𝒜 ∧ ¬a ∈ s → t ∈ 𝒜 ∧ ¬a ∈ t
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ ↑(Finset.nonMemberSubfamily a 𝒜) → t ∈ ↑(Finset.nonMemberSubfamily a 𝒜)
simp_rw [mem_coe, mem_nonMemberSubfamily]
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ 𝒜 ∧ ¬a ∈ s → t ∈ 𝒜 ∧ ¬a ∈ t
exact And.imp (h hts) (mt <| @hts _)