[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ (fun s => ↑up (↑f '' ↑down s)) 1 = 1
[PROOFSTEP]
dsimp only
  -- porting note: structures do not do this automatically any more
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ ↑up (↑f '' ↑down 1) = 1
[PROOFSTEP]
rw [down_one, image_one, map_one, singleton_one, up_one]
