α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b : α
⊢ 𝓝 b = update pure a₀ l b
refine' nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => _
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
⊢ ∃ t, t ∈ update pure a l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a l a'

case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
rcases eq_or_ne a a₀ with (rfl | ha)
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb : b ∈ s
⊢ s ∈ update pure a l b
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
⊢ ∃ t, t ∈ update pure a l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a l a'
refine' ⟨s, hs, Subset.rfl, fun b hb => _⟩
case inl.inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ : α
s : Set α
b : α
hb : b ∈ s
h : pure b ≤ l
hs : s ∈ update pure b l b
⊢ s ∈ update pure b l b

case inl.inr
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb✝ : b ∈ s
hb : b ≠ a
⊢ s ∈ update pure a l b
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb : b ∈ s
⊢ s ∈ update pure a l b
rcases eq_or_ne b a with (rfl | hb)
no goals
case inl.inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ : α
s : Set α
b : α
hb : b ∈ s
h : pure b ≤ l
hs : s ∈ update pure b l b
⊢ s ∈ update pure b l b
exact hs
no goals
case inl.inr
α : Type u
inst✝ : DecidableEq α
l : Filter α
b✝ a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
b : α
hb✝ : b ∈ s
hb : b ≠ a
⊢ s ∈ update pure a l b
rwa [update_noteq hb]
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
hs' : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
have hs' := hs
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ pure a
ha : a ≠ a₀
hs' : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ pure a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
hs' : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ update pure a₀ l a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
rw [update_noteq ha] at hs⊢
no goals
case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ pure a
ha : a ≠ a₀
hs' : s ∈ update pure a₀ l a
⊢ ∃ t, t ∈ pure a ∧ t ⊆ s ∧ ∀ (a' : α), a' ∈ t → s ∈ update pure a₀ l a'
exact ⟨{a}, rfl, singleton_subset_iff.mpr hs, forall_eq.2 hs'⟩