case some.some v v' =>
  have obvs : ∀ a, Option.map f (some a) = some (f a) := by intros a; rfl
  rw [obvs v, obvs v'] at p
  rw [Option.some_inj] at p
  apply congrArg; apply inj; assumption
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
⊢ some v = some v'
no goals