case h
ι : Type ?u.346721
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b
ι : Type ?u.346721
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ lookmap f l = l
rw [← map_id (l.lookmap f), lookmap_map_eq, map_id]
no goals
case h
ι : Type ?u.346721
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b
exact h