ι : Type ?u.328587
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
h : a ∈ l
this : ∃ a_1, a_1 ∈ attach l ∧ ↑a_1 = a
⊢ { val := a, property := h } ∈ attach l
ι : Type ?u.328587
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
h : a ∈ l
⊢ { val := a, property := h } ∈ attach l
have := mem_map.1 (by rw [attach_map_val] <;> exact h)
no goals
ι : Type ?u.328587
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
h : a ∈ l
⊢ ?m.328751 ∈ map ?m.328752 ?m.328753
rw [attach_map_val] <;> exact h
case intro.mk.intro
ι : Type ?u.328587
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
val✝ : α
property✝ : val✝ ∈ l
m : { val := val✝, property := property✝ } ∈ attach l
h : ↑{ val := val✝, property := property✝ } ∈ l
⊢ { val := ↑{ val := val✝, property := property✝ }, property := h } ∈ attach l
ι : Type ?u.328587
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
a : α
h : a ∈ l
this : ∃ a_1, a_1 ∈ attach l ∧ ↑a_1 = a
⊢ { val := a, property := h } ∈ attach l
rcases this with ⟨⟨_, _⟩, m, rfl⟩
no goals
case intro.mk.intro
ι : Type ?u.328587
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
val✝ : α
property✝ : val✝ ∈ l
m : { val := val✝, property := property✝ } ∈ attach l
h : ↑{ val := val✝, property := property✝ } ∈ l
⊢ { val := ↑{ val := val✝, property := property✝ }, property := h } ∈ attach l
exact m