theorem Equiv.option_eq_iff_map {α : Type u_1} {β : Type u_2} {e : α ≃ β} {x y : Option α} : x = y ↔ Option.map (⇑e) x = Option.map (⇑e) y

@[simp]

theorem Equiv.symm_one {α : Type u_1} : Equiv.symm 1 = 1