[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
⊢ s = a ::ₘ a ::ₘ t
[PROOFSTEP]
rwa [cons_add, cons_add, zero_add] at s_eq 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a : α
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ Nodup (Quot.mk Setoid.r _l) ↔ ∀ (a : α), count a (Quot.mk Setoid.r _l) ≤ 1
[PROOFSTEP]
simp only [quot_mk_to_coe'', coe_nodup, mem_coe, coe_count]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a : α
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ List.Nodup _l ↔ ∀ (a : α), List.count a _l ≤ 1
[PROOFSTEP]
apply List.nodup_iff_count_le_one
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
⊢ count a s = if a ∈ s then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
h : a ∈ s
⊢ count a s = 1
[PROOFSTEP]
exact count_eq_one_of_mem d h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
h : ¬a ∈ s
⊢ count a s = 0
[PROOFSTEP]
exact count_eq_zero_of_not_mem h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t : Multiset α
a : α
d₁ : Nodup s
d₂ : Nodup t
⊢ Nodup (s + t) ↔ Disjoint s t
[PROOFSTEP]
simp [nodup_add, d₁, d₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : Nodup l
⊢ a ∈ Multiset.erase l b ↔ a ≠ b ∧ a ∈ l
[PROOFSTEP]
rw [d.erase_eq_filter b, mem_filter, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t✝ : Multiset α
a : α
t : Multiset β
l₁ : List α
l₂ : List β
d₁ : Nodup (Quotient.mk (isSetoid α) l₁)
d₂ : Nodup (Quotient.mk (isSetoid β) l₂)
⊢ Nodup (Quotient.mk (isSetoid α) l₁ ×ˢ Quotient.mk (isSetoid β) l₂)
[PROOFSTEP]
simp [List.Nodup.product d₁ d₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t✝ : Multiset α
a : α
σ : α → Type u_4
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)
[PROOFSTEP]
choose f hf using fun a => Quotient.exists_rep (t a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t✝ : Multiset α
a : α
σ : α → Type u_4
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)
[PROOFSTEP]
simpa [← funext hf] using List.Nodup.sigma
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
s t : Multiset α
x✝ : Nodup s ∧ Nodup t
h₁ : Nodup s
h₂ : Nodup t
a : α
⊢ count a (s ∪ t) ≤ 1
[PROOFSTEP]
rw [count_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
s t : Multiset α
x✝ : Nodup s ∧ Nodup t
h₁ : Nodup s
h₂ : Nodup t
a : α
⊢ max (count a s) (count a t) ≤ 1
[PROOFSTEP]
exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
s : Multiset α
t : α → Multiset β
h₁ : ∀ (a : α), ∃ l, t a = ↑l
t' : α → List β
h' : ∀ (x : α), t x = ↑(t' x)
this : t = fun a => ↑(t' a)
hd : Symmetric fun a b => List.Disjoint (t' a) (t' b)
⊢ ∀ (a : List α),
    Nodup (bind (Quot.mk Setoid.r a) t) ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk Setoid.r a → Nodup (t a_1)) ∧
        Pairwise (fun a b => Disjoint (t a) (t b)) (Quot.mk Setoid.r a)
[PROOFSTEP]
simp [this, List.nodup_bind, pairwise_coe_iff_pairwise hd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ False
[PROOFSTEP]
refine' count_eq_zero.1 _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ count a (s - t) = 0
[PROOFSTEP]
rw [count_sub a s t, tsub_eq_zero_iff_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t
[PROOFSTEP]
exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
x : β
⊢ x ∈ t ↔ x ∈ map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
[PROOFSTEP]
simp only [mem_map, true_and_iff, Subtype.exists, eq_comm, mem_attach]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
x : β
⊢ x ∈ t ↔ ∃ a h, x = i a (_ : ↑{ val := a, property := (_ : a ∈ s) } ∈ s)
[PROOFSTEP]
exact ⟨i_surj _, fun ⟨y, hy⟩ => hy.snd.symm ▸ hi _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
this : t = map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
⊢ map f s = pmap (fun x x_1 => f x) s (_ : ∀ (x : α), x ∈ s → x ∈ s)
[PROOFSTEP]
rw [pmap_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
this : t = map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
⊢ pmap (fun x x_1 => f x) s (_ : ∀ (x : α), x ∈ s → x ∈ s) = map (fun x => f ↑x) (attach s)
[PROOFSTEP]
rw [pmap_eq_map_attach]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
this : t = map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
⊢ map (fun x => f ↑x) (attach s) = map g t
[PROOFSTEP]
rw [this, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ t✝ : Multiset α
a : α
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : Nodup s
ht : Nodup t
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, b = i a ha
this : t = map (fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
⊢ map (fun x => f ↑x) (attach s) = map (g ∘ fun x => i ↑x (_ : ↑x ∈ s)) (attach s)
[PROOFSTEP]
exact map_congr rfl fun x _ => h _ _
