no goals
α : Type u_1
β : Type u_2
γ : Type ?u.798
δ : Type ?u.801
f : α → β
Hf : Function.Injective f
a₁ a₂ : α
H : Option.map f (some a₁) = Option.map f (some a₂)
⊢ some a₁ = some a₂
rw [Hf (Option.some.inj H)]