[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : LE α
x : α
z : β
⊢ z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s y
[PROOFSTEP]
simp_rw [accumulate_def, mem_iUnion₂, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ ⋃ (y : α) (_ : y ≤ x), Accumulate s y = ⋃ (y : α) (_ : y ≤ x), s y
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ ⋃ (y : α) (_ : y ≤ x), Accumulate s y ⊆ ⋃ (y : α) (_ : y ≤ x), s y
[PROOFSTEP]
exact iUnion₂_subset fun y hy => monotone_accumulate hy
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ ⋃ (y : α) (_ : y ≤ x), s y ⊆ ⋃ (y : α) (_ : y ≤ x), Accumulate s y
[PROOFSTEP]
exact iUnion₂_mono fun y _ => subset_accumulate
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ⋃ (x : α), Accumulate s x = ⋃ (x : α), s x
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ⋃ (x : α), Accumulate s x ⊆ ⋃ (x : α), s x
[PROOFSTEP]
simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i
[PROOFSTEP]
intro z x x' ⟨_, hz⟩
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i
[PROOFSTEP]
exact ⟨x', hz⟩
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ⋃ (x : α), s x ⊆ ⋃ (x : α), Accumulate s x
[PROOFSTEP]
exact iUnion_mono fun i => subset_accumulate
