rw [obvs v, obvs v'] at p
A B : Type
f : A → B
inj : Injective f
v v' : A
p : Option.map f (some v) = Option.map f (some v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'
A B : Type
f : A → B
inj : Injective f
v v' : A
p : some (f v) = some (f v')
obvs : ∀ (a : A), Option.map f (some a) = some (f a)
⊢ some v = some v'