case none
ι : Type ?u.345717
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

case some
ι : Type ?u.345717
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)
ι : Type ?u.345717
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
⊢ map g (lookmap f (a :: l)) = map g (a :: l)
cases' h' : f a with b
case none
ι : Type ?u.345717
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f l) = map g l
case none
ι : Type ?u.345717
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f (a :: l)) = map g (a :: l)
simp [h']
no goals
case none
ι : Type ?u.345717
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f l) = map g l
exact lookmap_map_eq _ h l
no goals
case some
ι : Type ?u.345717
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)
simp [lookmap_cons_some _ _ h', h _ _ h']