Theorem: List.bind_toList_some (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
⊢ (bs.bind fun i => (f i).toList) = map g bs
Tactic:
have : bs.bind (fun i => (f i).toList) = bs.bind (pure ∘ g) :=
  List.bind_congr (by simp; intro m hm; simp[h _ hm])
State after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
this : (bs.bind fun i => (f i).toList) = bs.bind (pure ∘ g)
⊢ (bs.bind fun i => (f i).toList) = map g bs

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
this : (bs.bind fun i => (f i).toList) = bs.bind (pure ∘ g)
⊢ (bs.bind fun i => (f i).toList) = map g bs
Tactic:
rw[this, List.bind_pure_eq_map]
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
⊢ ∀ x ∈ bs, (f x).toList = (pure ∘ g) x
Tactic:
simp
State after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
⊢ ∀ x ∈ bs, f x = some (g x)

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
⊢ ∀ x ∈ bs, f x = some (g x)
Tactic:
intro m hm
State after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
m : β
hm : m ∈ bs
⊢ f m = some (g m)

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
m : β
hm : m ∈ bs
⊢ f m = some (g m)
Tactic:
simp[h _ hm]
State after:
no goals