Theorem: List.subset_bind_of_mem (Logic/Vorspiel/OmegaRec.lean)

State before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
a : α
as : List α
h : a ∈ as
f : α → List α
⊢ f a ⊆ as.bind f
Tactic:
intro a' ha'
State after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
a : α
as : List α
h : a ∈ as
f : α → List α
a' : α
ha' : a' ∈ f a
⊢ a' ∈ as.bind f

State before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
a : α
as : List α
h : a ∈ as
f : α → List α
a' : α
ha' : a' ∈ f a
⊢ a' ∈ as.bind f
Tactic:
simpa using ⟨a, h, ha'⟩
State after:
no goals