α : Type u_1
β : Type u_2
γ : Type ?u.478256
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun a b => f a = f b) s t ↔ Rel (fun x x_1 => x = x_1) s t
α : Type u_1
β : Type u_2
γ : Type ?u.478256
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s = map f t ↔ s = t
rw [← rel_eq, ← rel_eq, rel_map]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.478256
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun a b => f a = f b) s t ↔ Rel (fun x x_1 => x = x_1) s t
simp only [hf.eq_iff]