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