α : Type ?u.56027
β : Type ?u.56030
G : Type u_1
inst✝ : Group G
a b c d : G
⊢ Injective fun a => a * b⁻¹
α : Type ?u.56027
β : Type ?u.56030
G : Type u_1
inst✝ : Group G
a b c d : G
⊢ Injective fun a => a / b
simp only [div_eq_mul_inv]
no goals
α : Type ?u.56027
β : Type ?u.56030
G : Type u_1
inst✝ : Group G
a b c d : G
⊢ Injective fun a => a * b⁻¹
exact fun a a' h ↦ mul_left_injective b⁻¹ h