no goals
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (↑(↑(Units.map f) c)) (↑f a) (↑f b)
rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]