-- Mathlib/Data/Multiset/Bind.lean
@[simp] lemma nodup_bind :
    Nodup (bind s f) ↔ (∀ a ∈ s, Nodup (f a)) ∧ s.Pairwise (Disjoint on f)

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
have : f = fun a ↦ ofList (f' a) := funext h'

Result:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a => ↑(f' a)
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a => ↑(f' a)
hd : Symmetric fun a b => (f' a).Disjoint (f' b)
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a, (f a_1).Nodup) ∧
        Pairwise (fun x y => Disjoint (f x) (f y)) (Quot.mk (⇑(List.isSetoid α)) a)

Tactic:
simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise hd]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a => ↑(f' a)
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
have hd : Symmetric fun a b ↦ List.Disjoint (f' a) (f' b) := fun a b h ↦ h.symm

Result:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a => ↑(f' a)
hd : Symmetric fun a b => (f' a).Disjoint (f' b)
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
have : ∀ a, ∃ l : List β, f a = l := fun a => Quot.induction_on (f a) fun l => ⟨l, rfl⟩

Result:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
this : ∀ (a : α), ∃ l, f a = ↑l
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a => ↑(f' a)
hd : Symmetric fun a b => (f' a).Disjoint (f' b)
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a, (f a_1).Nodup) ∧
        Pairwise (Disjoint on f) (Quot.mk (⇑(List.isSetoid α)) a)

Tactic:
unfold Function.onFun

Result:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a => ↑(f' a)
hd : Symmetric fun a b => (f' a).Disjoint (f' b)
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a, (f a_1).Nodup) ∧
        Pairwise (fun x y => Disjoint (f x) (f y)) (Quot.mk (⇑(List.isSetoid α)) a)

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a => ↑(f' a)
hd : Symmetric fun a b => (f' a).Disjoint (f' b)
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
exact Quot.induction_on s <| by
  unfold Function.onFun
  simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise hd]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
this : ∀ (a : α), ∃ l, f a = ↑l
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
choose f' h' using this

Result:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
⊢ (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (Disjoint on f) s