α : Type u
e : Encoding α
x✝¹ x✝ : α
h : encode e x✝¹ = encode e x✝
⊢ some x✝¹ = some x✝
α : Type u
e : Encoding α
⊢ Function.Injective e.encode
refine' fun _ _ h => Option.some_injective _ _
no goals
α : Type u
e : Encoding α
x✝¹ x✝ : α
h : encode e x✝¹ = encode e x✝
⊢ some x✝¹ = some x✝
rw [← e.decode_encode, ← e.decode_encode, h]