case mp
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
fs : List β'
t : Set (List α')
⊢ t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t

case mpr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
fs : List β'
t : Set (List α')
⊢ (∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t) → t ∈ traverse f fs
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
fs : List β'
t : Set (List α')
⊢ t ∈ traverse f fs ↔ ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
constructor
case mp.nil
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
t : Set (List α')
⊢ t ∈ traverse f [] → ∃ us, Forall₂ (fun b s => s ∈ f b) [] us ∧ sequence us ⊆ t

case mp.cons
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
head✝ : β'
tail✝ : List β'
tail_ih✝ : ∀ (t : Set (List α')), t ∈ traverse f tail✝ → ∃ us, Forall₂ (fun b s => s ∈ f b) tail✝ us ∧ sequence us ⊆ t
t : Set (List α')
⊢ t ∈ traverse f (head✝ :: tail✝) → ∃ us, Forall₂ (fun b s => s ∈ f b) (head✝ :: tail✝) us ∧ sequence us ⊆ t
case mp
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
fs : List β'
t : Set (List α')
⊢ t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
induction fs generalizing t
case mp.cons
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
head✝ : β'
tail✝ : List β'
tail_ih✝ : ∀ (t : Set (List α')), t ∈ traverse f tail✝ → ∃ us, Forall₂ (fun b s => s ∈ f b) tail✝ us ∧ sequence us ⊆ t
t : Set (List α')
⊢ t ∈ traverse f (head✝ :: tail✝) → ∃ us, Forall₂ (fun b s => s ∈ f b) (head✝ :: tail✝) us ∧ sequence us ⊆ t
case mp.nil
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
t : Set (List α')
⊢ t ∈ traverse f [] → ∃ us, Forall₂ (fun b s => s ∈ f b) [] us ∧ sequence us ⊆ t

case mp.cons
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
head✝ : β'
tail✝ : List β'
tail_ih✝ : ∀ (t : Set (List α')), t ∈ traverse f tail✝ → ∃ us, Forall₂ (fun b s => s ∈ f b) tail✝ us ∧ sequence us ⊆ t
t : Set (List α')
⊢ t ∈ traverse f (head✝ :: tail✝) → ∃ us, Forall₂ (fun b s => s ∈ f b) (head✝ :: tail✝) us ∧ sequence us ⊆ t
case nil =>
  simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
    singleton_subset_iff, traverse_nil]
no goals
case mp.cons
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
head✝ : β'
tail✝ : List β'
tail_ih✝ : ∀ (t : Set (List α')), t ∈ traverse f tail✝ → ∃ us, Forall₂ (fun b s => s ∈ f b) tail✝ us ∧ sequence us ⊆ t
t : Set (List α')
⊢ t ∈ traverse f (head✝ :: tail✝) → ∃ us, Forall₂ (fun b s => s ∈ f b) (head✝ :: tail✝) us ∧ sequence us ⊆ t
case cons b fs ih =>
  intro ht
  rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
  rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩
  rcases ih v hv with ⟨us, hus, hu⟩
  exact ⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
t : Set (List α')
⊢ t ∈ traverse f [] → ∃ us, Forall₂ (fun b s => s ∈ f b) [] us ∧ sequence us ⊆ t
simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
  singleton_subset_iff, traverse_nil]
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
ht : t ∈ traverse f (b :: fs)
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
⊢ t ∈ traverse f (b :: fs) → ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
intro ht
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
ht✝ : t ∈ traverse f (b :: fs)
u : Set (List α' → List α')
hu : u ∈ cons <$> f b
v : Set (List α')
hv : v ∈ (fun x => List.traverse f fs) ()
ht : Set.seq u v ⊆ t
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
ht : t ∈ traverse f (b :: fs)
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
ht✝ : t ∈ traverse f (b :: fs)
u : Set (List α' → List α')
hu : u ∈ cons <$> f b
v : Set (List α')
hv : v ∈ (fun x => List.traverse f fs) ()
ht : Set.seq u v ⊆ t
w : Set α'
hw : w ∈ f b
hwu : cons '' w ⊆ u
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
ht✝ : t ∈ traverse f (b :: fs)
u : Set (List α' → List α')
hu : u ∈ cons <$> f b
v : Set (List α')
hv : v ∈ (fun x => List.traverse f fs) ()
ht : Set.seq u v ⊆ t
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
ht✝ : t ∈ traverse f (b :: fs)
u : Set (List α' → List α')
hu✝ : u ∈ cons <$> f b
v : Set (List α')
hv : v ∈ (fun x => List.traverse f fs) ()
ht : Set.seq u v ⊆ t
w : Set α'
hw : w ∈ f b
hwu : cons '' w ⊆ u
us : List (Set α')
hus : Forall₂ (fun b s => s ∈ f b) fs us
hu : sequence us ⊆ v
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
ht✝ : t ∈ traverse f (b :: fs)
u : Set (List α' → List α')
hu : u ∈ cons <$> f b
v : Set (List α')
hv : v ∈ (fun x => List.traverse f fs) ()
ht : Set.seq u v ⊆ t
w : Set α'
hw : w ∈ f b
hwu : cons '' w ⊆ u
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
rcases ih v hv with ⟨us, hus, hu⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
b : β'
fs : List β'
ih : ∀ (t : Set (List α')), t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α')
ht✝ : t ∈ traverse f (b :: fs)
u : Set (List α' → List α')
hu✝ : u ∈ cons <$> f b
v : Set (List α')
hv : v ∈ (fun x => List.traverse f fs) ()
ht : Set.seq u v ⊆ t
w : Set α'
hw : w ∈ f b
hwu : cons '' w ⊆ u
us : List (Set α')
hus : Forall₂ (fun b s => s ∈ f b) fs us
hu : sequence us ⊆ v
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
exact ⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
fs : List β'
t : Set (List α')
us : List (Set α')
hus : Forall₂ (fun b s => s ∈ f b) fs us
hs : sequence us ⊆ t
⊢ t ∈ traverse f fs
case mpr
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
fs : List β'
t : Set (List α')
⊢ (∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t) → t ∈ traverse f fs
rintro ⟨us, hus, hs⟩
no goals
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.305467
ι : Sort x
α' β' γ' : Type u
f : β' → Filter α'
s : γ' → Set α'
fs : List β'
t : Set (List α')
us : List (Set α')
hus : Forall₂ (fun b s => s ∈ f b) fs us
hs : sequence us ⊆ t
⊢ t ∈ traverse f fs
exact mem_of_superset (mem_traverse _ _ hus) hs