α : Type u_2
β : Type ?u.9365
γ : Type ?u.9368
r : α → α → Prop
s t✝ : Multiset α
a : α
σ : α → Type u_1
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), Quotient.mk (isSetoid (σ a)) (f a) = t a
⊢ Nodup (Quot.mk Setoid.r l₁) → (∀ (a : α), Nodup (t a)) → Nodup (Multiset.sigma (Quot.mk Setoid.r l₁) t)
α : Type u_2
β : Type ?u.9365
γ : Type ?u.9368
r : α → α → Prop
s t✝ : Multiset α
a : α
σ : α → Type u_1
t : (a : α) → Multiset (σ a)
l₁ : List α
⊢ Nodup (Quot.mk Setoid.r l₁) → (∀ (a : α), Nodup (t a)) → Nodup (Multiset.sigma (Quot.mk Setoid.r l₁) t)
choose f hf using fun a => Quotient.exists_rep (t a)
no goals
α : Type u_2
β : Type ?u.9365
γ : Type ?u.9368
r : α → α → Prop
s t✝ : Multiset α
a : α
σ : α → Type u_1
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), Quotient.mk (isSetoid (σ a)) (f a) = t a
⊢ Nodup (Quot.mk Setoid.r l₁) → (∀ (a : α), Nodup (t a)) → Nodup (Multiset.sigma (Quot.mk Setoid.r l₁) t)
simpa [←funext hf] using List.Nodup.sigma