case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
x : Option α
⊢ (Option.map g ∘ Option.map f) x = Option.map (g ∘ f) x
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ Option.map g ∘ Option.map f = Option.map (g ∘ f)
funext x
no goals
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
x : Option α
⊢ (Option.map g ∘ Option.map f) x = Option.map (g ∘ f) x
simp