no goals
α✝ : Type ?u.1896
β✝ : Type ?u.1899
α : Type u_1
β : Type u_2
inst✝ : Encodable α
e : β ≃ α
n : ℕ
⊢ Option.bind (decode n) (some ∘ ↑e.symm) = Option.map (↑e.symm) (decode n)
rw [Option.map_eq_bind]