-- Mathlib/Order/Filter/ListTraverse.lean
theorem mem_traverse_iff (fs : List β) (t : Set (List α)) :
    t ∈ traverse f fs ↔
      ∃ us : List (Set α), Forall₂ (fun b (s : Set α) => s ∈ f b) fs us ∧ sequence us ⊆ t

Proof state:
case mpr.intro.intro
α β : Type u
f : β → Filter α
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

Tactic:
exact mem_of_superset (mem_traverse _ _ hus) hs

Result:
no goals

Proof state:
case mp.cons
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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

Tactic:
intro ht

Result:
case mp.cons
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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

Proof state:
case mp.cons.intro.intro.intro.intro.intro.intro
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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 : u.seq 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

Tactic:
rcases ih v hv with ⟨us, hus, hu⟩

Result:
case mp.cons.intro.intro.intro.intro.intro.intro.intro.intro
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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 : u.seq 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

Proof state:
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ t ∈ traverse f fs ↔ ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t

Tactic:
constructor

Result:
case mp
α β : Type u
f : β → Filter α
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
f : β → Filter α
fs : List β
t : Set (List α)
⊢ (∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t) → t ∈ traverse f fs

Proof state:
case mpr
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ (∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t) → t ∈ traverse f fs

Tactic:
rintro ⟨us, hus, hs⟩

Result:
case mpr.intro.intro
α β : Type u
f : β → Filter α
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

Proof state:
case mp.cons
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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

Tactic:
rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩

Result:
case mp.cons.intro.intro.intro.intro
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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 : u.seq v ⊆ t
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

Proof state:
case mp.nil
α β : Type u
f : β → Filter α
t : Set (List α)
⊢ t ∈ traverse f [] → ∃ us, Forall₂ (fun b s => s ∈ f b) [] us ∧ sequence us ⊆ t

Tactic:
simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
  singleton_subset_iff, traverse_nil]

Result:
no goals

Proof state:
case mp
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
⊢ t ∈ traverse f fs → ∃ us, Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t

Tactic:
induction fs generalizing t with
| nil =>
  simp only [sequence, mem_pure, imp_self, forall₂_nil_left_iff, exists_eq_left, Set.pure_def,
    singleton_subset_iff, traverse_nil]
| 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⟩

Result:
no goals

Proof state:
case mp.cons.intro.intro.intro.intro
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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 : u.seq v ⊆ t
⊢ ∃ us, Forall₂ (fun b s => s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

Tactic:
rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hwu⟩

Result:
case mp.cons.intro.intro.intro.intro.intro.intro
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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 : u.seq 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

Proof state:
case mp.cons.intro.intro.intro.intro.intro.intro.intro.intro
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ 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 : u.seq 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

Tactic:
exact ⟨w::us, Forall₂.cons hw hus, (Set.seq_mono hwu hu).trans ht⟩

Result:
no goals