[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
⊢ ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t
[PROOFSTEP]
rintro ⟨l₁⟩ ⟨l₂⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk Setoid.r l₁ = a ::ₘ Quot.mk Setoid.r l₂ ↔ Quot.mk Setoid.r l₁ = Quot.mk Setoid.r l₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Prop
empty : p 0
cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)
⊢ ∀ (s : Multiset α), p s
[PROOFSTEP]
rintro ⟨l⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Prop
empty : p 0
cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk Setoid.r l)
[PROOFSTEP]
induction' l with _ _ ih <;> [exact empty; exact cons ih]
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Prop
empty : p 0
cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk Setoid.r l)
[PROOFSTEP]
induction' l with _ _ ih
[GOAL]
case mk.nil
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Prop
empty : p 0
cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)
s✝ : Multiset α
⊢ p (Quot.mk Setoid.r [])
[PROOFSTEP]
exact empty
[GOAL]
case mk.cons
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Prop
empty : p 0
cons : ∀ ⦃a : α⦄ {s : Multiset α}, p s → p (a ::ₘ s)
s✝ : Multiset α
head✝ : α
tail✝ : List α
ih : p (Quot.mk Setoid.r tail✝)
⊢ p (Quot.mk Setoid.r (head✝ :: tail✝))
[PROOFSTEP]
exact cons ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
C : Multiset α → Sort u_4
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m),
    HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))
m : Multiset α
l l' : List α
h : l ≈ l'
a✝ : α
l✝ l'✝ : List α
b✝ : C (Quotient.mk (isSetoid α) l✝)
b'✝ : C (Quotient.mk (isSetoid α) l'✝)
hl : l✝ ~ l'✝
x✝ : HEq b✝ b'✝
⊢ HEq (C_cons a✝ (Quotient.mk (isSetoid α) l✝) b✝) (C_cons a✝ (Quotient.mk (isSetoid α) l'✝) b'✝)
[PROOFSTEP]
congr 1
[GOAL]
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
C : Multiset α → Sort u_4
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m),
    HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))
m : Multiset α
l l' : List α
h : l ≈ l'
a✝ : α
l✝ l'✝ : List α
b✝ : C (Quotient.mk (isSetoid α) l✝)
b'✝ : C (Quotient.mk (isSetoid α) l'✝)
hl : l✝ ~ l'✝
x✝ : HEq b✝ b'✝
⊢ Quotient.mk (isSetoid α) l✝ = Quotient.mk (isSetoid α) l'✝
[PROOFSTEP]
exact Quot.sound hl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk Setoid.r l
⊢ Quot.mk Setoid.r l = 0
[PROOFSTEP]
rw [eq_nil_iff_forall_not_mem.mpr H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk Setoid.r l
⊢ Quot.mk Setoid.r [] = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
l✝ : List α
hl : Quot.mk Setoid.r l✝ ≠ 0
a : α
l : List α
x✝ : Quot.mk Setoid.r (a :: l) ≠ 0
⊢ a ∈ Quot.mk Setoid.r (a :: l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
haveI : DecidableEq α := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ a ::ₘ as = b ::ₘ bs → a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
intro eq
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
by_cases h : a = b
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = a ::ₘ bs
⊢ a = a ∧ as = bs ∨ a ≠ a ∧ ∃ cs, as = a ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
simp_all
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
have : a ∈ b ::ₘ bs := eq ▸ mem_cons_self _ _
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
have : a ∈ bs := by simpa [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a ∈ bs
[PROOFSTEP]
simpa [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
rcases exists_cons_of_mem this with ⟨cs, hcs⟩
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
[PROOFSTEP]
simp [h, hcs]
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ as = b ::ₘ cs
[PROOFSTEP]
have : a ::ₘ as = b ::ₘ a ::ₘ cs := by simp [eq, hcs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs
[PROOFSTEP]
simp [eq, hcs]
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ as = b ::ₘ cs
[PROOFSTEP]
have : a ::ₘ as = a ::ₘ b ::ₘ cs := by rwa [cons_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = a ::ₘ b ::ₘ cs
[PROOFSTEP]
rwa [cons_swap]
[GOAL]
case neg.intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this✝³ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝² : a ∈ b ::ₘ bs
this✝¹ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this✝ : a ::ₘ as = b ::ₘ a ::ₘ cs
this : a ::ₘ as = a ::ₘ b ::ₘ cs
⊢ as = b ::ₘ cs
[PROOFSTEP]
simpa using this
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
[PROOFSTEP]
rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
[GOAL]
case mpr.inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
eq₁ : a = b
eq₂ : as = bs
⊢ a ::ₘ as = b ::ₘ bs
[PROOFSTEP]
simp [*]
[GOAL]
case mpr.inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
as bs : Multiset α
this : DecidableEq α
left✝ : a ≠ b
cs : Multiset α
eq₁ : as = b ::ₘ cs
eq₂ : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
[PROOFSTEP]
simp [*, cons_swap a b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ b ∈ {a} ↔ b = a
[PROOFSTEP]
simp only [← cons_zero, mem_cons, iff_self_iff, or_false_iff, not_mem_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
⊢ a ∈ {a}
[PROOFSTEP]
rw [← cons_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
⊢ a ∈ a ::ₘ 0
[PROOFSTEP]
exact mem_cons_self _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ {a} = {b} ↔ a = b
[PROOFSTEP]
simp_rw [← cons_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b
[PROOFSTEP]
exact cons_inj_left _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
a : α
⊢ ↑l = {a} ↔ l = [a]
[PROOFSTEP]
rw [← coe_singleton, coe_eq_coe, List.perm_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
m : Multiset α
⊢ {a} = b ::ₘ m ↔ a = b ∧ m = 0
[PROOFSTEP]
rw [← cons_zero, cons_eq_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s t : Multiset α
⊢ a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t
[PROOFSTEP]
simp [subset_iff, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
⊢ toList s = [] ↔ s = 0
[PROOFSTEP]
rw [← coe_eq_zero, coe_toList]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
⊢ a ∈ toList s ↔ a ∈ s
[PROOFSTEP]
rw [← mem_coe, coe_toList]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
m : Multiset α
⊢ toList m = [a] ↔ m = {a}
[PROOFSTEP]
rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Multiset α), a ≤ a
[PROOFSTEP]
rintro ⟨l⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Multiset α
l : List α
⊢ Quot.mk Setoid.r l ≤ Quot.mk Setoid.r l
[PROOFSTEP]
exact Subperm.refl _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a b c : Multiset α), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
rintro ⟨l₁⟩ ⟨l₂⟩ ⟨l₃⟩
[GOAL]
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Multiset α
l₁ : List α
b✝ : Multiset α
l₂ : List α
c✝ : Multiset α
l₃ : List α
⊢ Quot.mk Setoid.r l₁ ≤ Quot.mk Setoid.r l₂ →
    Quot.mk Setoid.r l₂ ≤ Quot.mk Setoid.r l₃ → Quot.mk Setoid.r l₁ ≤ Quot.mk Setoid.r l₃
[PROOFSTEP]
exact @Subperm.trans _ _ _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a b : Multiset α), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
rintro ⟨l₁⟩ ⟨l₂⟩ h₁ h₂
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Multiset α
l₁ : List α
b✝ : Multiset α
l₂ : List α
h₁ : Quot.mk Setoid.r l₁ ≤ Quot.mk Setoid.r l₂
h₂ : Quot.mk Setoid.r l₂ ≤ Quot.mk Setoid.r l₁
⊢ Quot.mk Setoid.r l₁ = Quot.mk Setoid.r l₂
[PROOFSTEP]
exact Quot.sound (Subperm.antisymm h₁ h₂)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Multiset α
a✝ : α
s : Multiset α
a : α
l : List α
this : l <+~ a :: l ∧ ¬l ~ a :: l
⊢ Quot.mk Setoid.r l < a ::ₘ Quot.mk Setoid.r l
[PROOFSTEP]
simpa [lt_iff_le_and_ne]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t ↔ s ≤ t
[PROOFSTEP]
refine' ⟨_, fun h => le_trans h <| le_cons_self _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t → s ≤ t
[PROOFSTEP]
suffices ∀ {t'} (_ : s ≤ t') (_ : a ∈ t'), a ::ₘ s ≤ t' by
  exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
a : α
m : ¬a ∈ s
this : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
⊢ s ≤ a ::ₘ t → s ≤ t
[PROOFSTEP]
exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
[PROOFSTEP]
introv h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
a : α
m : ¬a ∈ s
t' : Multiset α
h : s ≤ t'
⊢ a ∈ t' → a ::ₘ s ≤ t'
[PROOFSTEP]
revert m
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ¬a ∈ s → a ∈ t' → a ::ₘ s ≤ t'
[PROOFSTEP]
refine' leInductionOn h _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ¬a ∈ ↑l₁ → a ∈ ↑l₂ → a ::ₘ ↑l₁ ≤ ↑l₂
[PROOFSTEP]
introv s m₁ m₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ l₂ : List α
s : l₁ <+ l₂
m₁ : ¬a ∈ ↑l₁
m₂ : a ∈ ↑l₂
⊢ a ::ₘ ↑l₁ ≤ ↑l₂
[PROOFSTEP]
rcases mem_split m₂ with ⟨r₁, r₂, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ : List α
m₁ : ¬a ∈ ↑l₁
r₁ r₂ : List α
s : l₁ <+ r₁ ++ a :: r₂
m₂ : a ∈ ↑(r₁ ++ a :: r₂)
⊢ a ::ₘ ↑l₁ ≤ ↑(r₁ ++ a :: r₂)
[PROOFSTEP]
exact perm_middle.subperm_left.2 ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
⊢ s ≤ s + t
[PROOFSTEP]
simpa using add_le_add_left (zero_le t) s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
⊢ s ≤ t + s
[PROOFSTEP]
simpa using add_le_add_right (zero_le t) s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s t : Multiset α
⊢ a ::ₘ s + t = a ::ₘ (s + t)
[PROOFSTEP]
rw [← singleton_add, ← singleton_add, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s t : Multiset α
⊢ s + a ::ₘ t = a ::ₘ (s + t)
[PROOFSTEP]
rw [add_comm, cons_add, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
n : ℕ
h : a ∈ n • s
⊢ a ∈ s
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
n : ℕ
h✝ : a ∈ n • s
h : a ∈ zero • s
⊢ a ∈ s
[PROOFSTEP]
rw [zero_nsmul] at h 
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
n : ℕ
h✝ : a ∈ n • s
h : a ∈ 0
⊢ a ∈ s
[PROOFSTEP]
exact absurd h (not_mem_zero _)
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
n✝ : ℕ
h✝ : a ∈ n✝ • s
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ succ n • s
⊢ a ∈ s
[PROOFSTEP]
rw [succ_nsmul, mem_add] at h 
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
n✝ : ℕ
h✝ : a ∈ n✝ • s
n : ℕ
ih : a ∈ n • s → a ∈ s
h : a ∈ s ∨ a ∈ n • s
⊢ a ∈ s
[PROOFSTEP]
exact h.elim id ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ a ∈ n • s ↔ a ∈ s
[PROOFSTEP]
refine' ⟨mem_of_mem_nsmul, fun h => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
h : a ∈ s
⊢ a ∈ n • s
[PROOFSTEP]
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h0
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
h : a ∈ s
n : ℕ
h0 : succ n ≠ 0
⊢ a ∈ succ n • s
[PROOFSTEP]
rw [succ_nsmul, mem_add]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Multiset α
h : a ∈ s
n : ℕ
h0 : succ n ≠ 0
⊢ a ∈ s ∨ a ∈ n • s
[PROOFSTEP]
exact Or.inl h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
n : ℕ
a : α
⊢ n • (a ::ₘ s) = n • {a} + n • s
[PROOFSTEP]
rw [← singleton_add, nsmul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
⊢ length (toList s) = ↑card s
[PROOFSTEP]
rw [← coe_card, coe_toList]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
n : ℕ
⊢ ↑card (n • s) = n * ↑card s
[PROOFSTEP]
rw [card.map_nsmul s n, Nat.nsmul_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
⊢ ↑card {a} = 1
[PROOFSTEP]
simp only [← cons_zero, card_zero, eq_self_iff_true, zero_add, card_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a b : α
⊢ ↑card {a, b} = 2
[PROOFSTEP]
rw [insert_eq_cons, card_cons, card_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
e : s = 0
⊢ ↑card s = 0
[PROOFSTEP]
simp [e]
[GOAL]
α : Type u_1
p : Multiset α → Sort u_4
s : Multiset α
ih : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
t : Multiset α
_h : t < s
⊢ (invImage (fun a => PSigma.casesOn a fun s snd => ↑card s) instWellFoundedRelation).1 { fst := t, snd := ih }
    { fst := s, snd := ih }
[PROOFSTEP]
exact card_lt_of_lt _h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Sort u_4
s : Multiset α
H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
⊢ strongInductionOn s H = H s fun t _h => strongInductionOn t H
[PROOFSTEP]
rw [strongInductionOn]
[GOAL]
α : Type u_1
n : ℕ
s t : Multiset α
ht : ↑card t ≤ n
_h : s < t
⊢ (invImage (fun a => n - ↑card a) instWellFoundedRelation).1 t s
[PROOFSTEP]
exact
  (tsub_lt_tsub_iff_left_of_le ht).2
    (card_lt_of_lt _h)
      -- Porting note: reorderd universes
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Sort u_4
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → ↑card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑card t₁ ≤ n → p t₁
s : Multiset α
⊢ strongDownwardInduction H s = H s fun {t₂} ht _hst => strongDownwardInduction H t₂ ht
[PROOFSTEP]
rw [strongDownwardInduction]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Sort u_4
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → ↑card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInductionOn s H a) = H s fun {t} ht _h => strongDownwardInductionOn t H ht
[PROOFSTEP]
dsimp only [strongDownwardInductionOn]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Multiset α → Sort u_4
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → ↑card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht _h => strongDownwardInduction H t ht
[PROOFSTEP]
rw [strongDownwardInduction]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
n : ℕ
⊢ n • {a} = replicate n a
[PROOFSTEP]
rw [← replicate_one, nsmul_replicate, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ List.replicate k a <+ List.replicate n a
[PROOFSTEP]
rw [← replicate_le_coe, coe_replicate]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
x : α
n : ℕ
⊢ m < replicate (n + 1) x ↔ m ≤ replicate n x
[PROOFSTEP]
rw [lt_iff_cons_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x
[PROOFSTEP]
rintro ⟨x', hx'⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
⊢ m ≤ replicate n x
[PROOFSTEP]
have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x
[PROOFSTEP]
rwa [this, replicate_succ, cons_le_cons_iff] at hx' 
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ replicate (n + 1) x
[PROOFSTEP]
rw [replicate_succ]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x
[PROOFSTEP]
exact ⟨x, cons_le_cons _ h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b : α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ erase s a
[PROOFSTEP]
rw [erase_of_not_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b : α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s
[PROOFSTEP]
apply le_cons_self
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b : α
s t : Multiset α
a : α
⊢ s + {a} = t ↔ a ∈ t ∧ s = erase t a
[PROOFSTEP]
rw [add_comm, singleton_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b : α
s t : Multiset α
a : α
⊢ a ::ₘ s = t ↔ a ∈ t ∧ s = erase t a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b : α
s t : Multiset α
a : α
⊢ a ::ₘ s = t → a ∈ t ∧ s = erase t a
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b : α
s : Multiset α
a : α
⊢ a ∈ a ::ₘ s ∧ s = erase (a ::ₘ s) a
[PROOFSTEP]
exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b : α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = erase t a → a ::ₘ s = t
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ : Multiset α
a✝ b : α
t : Multiset α
a : α
h : a ∈ t
⊢ a ::ₘ erase t a = t
[PROOFSTEP]
exact cons_erase h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b a : α
s t : Multiset α
h : a ∈ t
⊢ erase (s + t) a = s + erase t a
[PROOFSTEP]
rw [add_comm, erase_add_left_pos s h, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b a : α
s t : Multiset α
h : ¬a ∈ t
⊢ erase (s + t) a = erase s a + t
[PROOFSTEP]
rw [add_comm, erase_add_right_neg s h, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
h : a ∈ s
⊢ erase s a < s
[PROOFSTEP]
simpa [h] using lt_cons_self (s.erase a) a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b : α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
⊢ erase s a ≤ t
[PROOFSTEP]
rw [← cons_erase m] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b : α
s t : Multiset α
a : α
h : a ::ₘ erase s a ≤ a ::ₘ t
m : a ∈ s
⊢ erase s a ≤ t
[PROOFSTEP]
exact (cons_le_cons_iff _).1 h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
⊢ ↑card (erase s a) = if a ∈ s then pred (↑card s) else ↑card s
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
h : a ∈ s
⊢ ↑card (erase s a) = if a ∈ s then pred (↑card s) else ↑card s
[PROOFSTEP]
rwa [card_erase_of_mem h, if_pos]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
h : ¬a ∈ s
⊢ ↑card (erase s a) = if a ∈ s then pred (↑card s) else ↑card s
[PROOFSTEP]
rwa [erase_of_not_mem h, if_neg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s t : Multiset α
⊢ s = t → (∀ (x : α), x ∈ t → f x = g x) → map f s = map g t
[PROOFSTEP]
rintro rfl h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
s : Multiset α
h : ∀ (x : α), x ∈ s → f x = g x
⊢ map f s = map g s
[PROOFSTEP]
induction s using Quot.inductionOn
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
a✝ : List α
h : ∀ (x : α), x ∈ Quot.mk Setoid.r a✝ → f x = g x
⊢ map f (Quot.mk Setoid.r a✝) = map g (Quot.mk Setoid.r a✝)
[PROOFSTEP]
exact congr_arg _ (List.map_congr h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
β' : Type u_2
m : Multiset α
f : α → β
f' : α → β'
h : β = β'
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (map f m) (map f' m)
[PROOFSTEP]
subst h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → HEq (f a) (f' a)
⊢ HEq (map f m) (map f' m)
[PROOFSTEP]
simp at hf 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ HEq (map f m) (map f' m)
[PROOFSTEP]
simp [map_congr rfl hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
t : α
⊢ map f ∘ cons t = cons (f t) ∘ map f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
t : α
x✝ : Multiset α
⊢ (map f ∘ cons t) x✝ = (cons (f t) ∘ map f) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
k : ℕ
a : α
⊢ map f (replicate k a) = replicate k (f a)
[PROOFSTEP]
simp only [← coe_replicate, coe_map, List.map_replicate]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
⊢ ∀ (x : Multiset α), (∀ (x_1 : α), x_1 ∈ x → p x_1) → ∃ y, map c y = x
[PROOFSTEP]
rintro ⟨l⟩ hl
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
x✝ : Multiset α
l : List α
hl : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x
⊢ ∃ y, map c y = Quot.mk Setoid.r l
[PROOFSTEP]
lift l to List β using hl
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
x✝ : Multiset α
l : List β
⊢ ∃ y, map c y = Quot.mk Setoid.r (List.map c l)
[PROOFSTEP]
exact ⟨l, coe_map _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
f : α → β
⊢ map f s = 0 ↔ s = 0
[PROOFSTEP]
rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} ↔ ∃ a, s = {a} ∧ f a = b
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} → ∃ a, s = {a} ∧ f a = b
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a} ∧ f a = b
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a, s = { a } := by rw [← card_eq_one, ← card_map, h, card_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a}
[PROOFSTEP]
rw [← card_eq_one, ← card_map, h, card_singleton]
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ ∃ a, s = {a} ∧ f a = b
[PROOFSTEP]
refine' ⟨a, ha, _⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a = b
[PROOFSTEP]
rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}
[PROOFSTEP]
rintro ⟨a, rfl, rfl⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a : α
⊢ map f {a} = {f a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t) ↔ map f s = b ::ₘ t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t) → map f s = b ::ₘ t
[PROOFSTEP]
rintro ⟨a, ha, rfl, rfl⟩
[GOAL]
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = f a ::ₘ map f (erase s a)
[PROOFSTEP]
rw [← map_cons, Multiset.cons_erase ha]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
[PROOFSTEP]
have : b ∈ s.map f := by
  rw [h]
  exact mem_cons_self _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ map f s
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t
[PROOFSTEP]
exact mem_cons_self _ _
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
this : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
[PROOFSTEP]
obtain ⟨a, h1, rfl⟩ := mem_map.mp this
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
a : α
h1 : a ∈ s
h : map f s = f a ::ₘ t
this : f a ∈ map f s
⊢ ∃ a_1, a_1 ∈ s ∧ f a_1 = f a ∧ map f (erase s a_1) = t
[PROOFSTEP]
obtain ⟨u, rfl⟩ := exists_cons_of_mem h1
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f (a ::ₘ u) = f a ::ₘ t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1, a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f (erase (a ::ₘ u) a_1) = t
[PROOFSTEP]
rw [map_cons, cons_inj_right] at h 
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1, a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f (erase (a ::ₘ u) a_1) = t
[PROOFSTEP]
refine' ⟨a, mem_cons_self _ _, rfl, _⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ map f (erase (a ::ₘ u) a) = t
[PROOFSTEP]
rw [Multiset.erase_cons_head, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) ↑l
⊢ b₁ ∈ replicate (?m.122527 h) b₂
[PROOFSTEP]
rwa [map_const] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t : Multiset α
h : s < t
⊢ map f s < map f t
[PROOFSTEP]
refine' (map_le_map h.le).lt_of_not_le fun H => h.ne <| eq_of_le_of_card_le h.le _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ ↑card t ≤ ↑card s
[PROOFSTEP]
rw [← s.card_map f, ← t.card_map f]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ ↑card (map f t) ≤ ↑card (map f s)
[PROOFSTEP]
exact card_le_of_le H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
⊢ map f (erase s x) = erase (map f s) (f x)
[PROOFSTEP]
induction' s using Multiset.induction_on with y s ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
⊢ map f (erase 0 x) = erase (map f 0) (f x)
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)
[PROOFSTEP]
by_cases hxy : y = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
hxy : y = x
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)
[PROOFSTEP]
cases hxy
[GOAL]
case pos.refl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
⊢ map f (erase (x ::ₘ s) x) = erase (map f (x ::ₘ s)) (f x)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
hxy : ¬y = x
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)
[PROOFSTEP]
rw [s.erase_cons_tail hxy, map_cons, map_cons, (s.map f).erase_cons_tail (hf.ne hxy), ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Surjective f
⊢ Surjective (map f)
[PROOFSTEP]
intro s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Surjective f
s : Multiset β
⊢ ∃ a, map f a = s
[PROOFSTEP]
induction' s using Multiset.induction_on with x s ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Surjective f
⊢ ∃ a, map f a = 0
[PROOFSTEP]
exact ⟨0, map_zero _⟩
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ a, map f a = s
⊢ ∃ a, map f a = x ::ₘ s
[PROOFSTEP]
obtain ⟨y, rfl⟩ := hf x
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Surjective f
s : Multiset β
ih : ∃ a, map f a = s
y : α
⊢ ∃ a, map f a = f y ::ₘ s
[PROOFSTEP]
obtain ⟨t, rfl⟩ := ih
[GOAL]
case cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ a, map f a = f y ::ₘ map f t
[PROOFSTEP]
exact ⟨y ::ₘ t, map_cons _ _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr f H x s)
[PROOFSTEP]
revert s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
⊢ ∀ (s : Multiset α), (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
[PROOFSTEP]
refine' Multiset.induction (by simp [px]) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
⊢ (∀ (a : α), a ∈ 0 → q a) → p (foldr f H x 0)
[PROOFSTEP]
simp [px]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (a : α), a ∈ s → q a) → p (foldr f H x s)) → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → q a_2) → p (foldr f H x (a ::ₘ s))
[PROOFSTEP]
intro a s hs hsa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
⊢ p (foldr f H x (a ::ₘ s))
[PROOFSTEP]
rw [foldr_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
⊢ p (f a (foldr f H x s))
[PROOFSTEP]
have hps : ∀ x : α, x ∈ s → q x := fun x hxs => hsa x (mem_cons_of_mem hxs)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
hps : ∀ (x : α), x ∈ s → q x
⊢ p (f a (foldr f H x s))
[PROOFSTEP]
exact hpqf a (foldr f H x s) (hsa a (mem_cons_self a s)) (hs hps)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → β
H : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldl f H x s)
[PROOFSTEP]
rw [foldl_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → β
H : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr (fun x y => f y x) (_ : ∀ (_x _y : α) (_z : β), f (f _z _y) _x = f (f _z _x) _y) x s)
[PROOFSTEP]
exact foldr_induction' (fun x y => f y x) (fun x y z => (H _ _ _).symm) x q p s hpqf px q_s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
⊢ ∀ {s₂ : Multiset α} {e : ↑l₁ = s₂} {H : ∀ (a : α), a ∈ s₂ → p a},
    Eq.ndrec (motive := fun s => (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x => ↑(List.pmap f l₁ H₁)) e H =
      ↑(List.pmap f l₁ H₁)
[PROOFSTEP]
intro s₂ e _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : ↑l₁ = s₂
H✝ : ∀ (a : α), a ∈ s₂ → p a
⊢ Eq.ndrec (motive := fun s => (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x => ↑(List.pmap f l₁ H₁)) e H✝ =
    ↑(List.pmap f l₁ H₁)
[PROOFSTEP]
subst e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
H✝ : ∀ (a : α), a ∈ ↑l₁ → p a
⊢ Eq.ndrec (motive := fun s => (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x => ↑(List.pmap f l₁ H₁)) (_ : ↑l₁ = ↑l₁)
      H✝ =
    ↑(List.pmap f l₁ H₁)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SizeOf α
x : α
s : Multiset α
hx : x ∈ s
⊢ sizeOf x < sizeOf s
[PROOFSTEP]
induction' s using Quot.inductionOn with l a b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SizeOf α
x : α
s : Multiset α
hx✝ : x ∈ s
l : List α
hx : x ∈ Quot.mk Setoid.r l
⊢ sizeOf x < sizeOf (Quot.mk Setoid.r l)
[PROOFSTEP]
exact List.sizeOf_lt_sizeOf_of_mem hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l (_ : ∀ (x : α), x ∈ l → (fun a_2 => a_2 ∈ a ::ₘ Quotient.mk (isSetoid α) l) x) =
    List.map (fun p => { val := ↑p, property := (_ : ↑p ∈ a ::ₘ Quotient.mk (isSetoid α) l) })
      (List.pmap mk l (_ : ∀ (_a : α), _a ∈ Quotient.mk (isSetoid α) l → _a ∈ Quotient.mk (isSetoid α) l))
[PROOFSTEP]
rw [List.map_pmap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l (_ : ∀ (x : α), x ∈ l → (fun a_2 => a_2 ∈ a ::ₘ Quotient.mk (isSetoid α) l) x) =
    List.pmap
      (fun a_1 h =>
        { val := ↑{ val := a_1, property := h },
          property := (_ : ↑{ val := a_1, property := h } ∈ a ::ₘ Quotient.mk (isSetoid α) l) })
      l (_ : ∀ (_a : α), _a ∈ Quotient.mk (isSetoid α) l → _a ∈ Quotient.mk (isSetoid α) l)
[PROOFSTEP]
exact List.pmap_congr _ fun _ _ _ _ => Subtype.eq rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
p : α → Prop
hp : (a : α) → Decidable (p a)
l : List α
⊢ (∀ (a : α), a ∈ l → p a) ↔ ∀ (a : α), a ∈ Quotient.mk (isSetoid α) l → p a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
m : Multiset α
β : α → Type u_4
h : (a : α) → DecidableEq (β a)
f g : (a : α) → a ∈ m → β a
⊢ (∀ (a : α) (h : a ∈ m), f a h = g a h) ↔ f = g
[PROOFSTEP]
simp [Function.funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Multiset α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ (∃ a, a ∈ l ∧ p a) ↔ ∃ x, x ∈ Quotient.mk (isSetoid α) l ∧ p x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
⊢ s - t ≤ u ↔ s ≤ u + t
[PROOFSTEP]
revert s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t u : Multiset α
a b : α
⊢ ∀ {s : Multiset α}, s - t ≤ u ↔ s ≤ u + t
[PROOFSTEP]
exact @(Multiset.induction_on t (by simp [Multiset.sub_zero]) fun a t IH s => by simp [IH, erase_le_iff_le_cons])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t u : Multiset α
a b : α
⊢ ∀ {s : Multiset α}, s - 0 ≤ u ↔ s ≤ u + 0
[PROOFSTEP]
simp [Multiset.sub_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t✝ u : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s : Multiset α}, s - t ≤ u ↔ s ≤ u + t
s : Multiset α
⊢ s - a ::ₘ t ≤ u ↔ s ≤ u + a ::ₘ t
[PROOFSTEP]
simp [IH, erase_le_iff_le_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a✝ b a : α
s t : Multiset α
h : t ≤ s
⊢ a ::ₘ s - t = a ::ₘ (s - t)
[PROOFSTEP]
rw [← singleton_add, ← singleton_add, add_tsub_assoc_of_le h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
l₁ l₂ : List α
⊢ Quotient.mk (isSetoid α) l₁ - Quotient.mk (isSetoid α) l₂ =
    foldl erase (_ : ∀ (s : Multiset α) (a b : α), erase (erase s a) b = erase (erase s b) a)
      (Quotient.mk (isSetoid α) l₁) (Quotient.mk (isSetoid α) l₂)
[PROOFSTEP]
show ofList (l₁.diff l₂) = foldl erase erase_comm l₁ l₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(List.diff l₁ l₂) = foldl erase (_ : ∀ (s : Multiset α) (a b : α), erase (erase s a) b = erase (erase s b) a) ↑l₁ ↑l₂
[PROOFSTEP]
rw [diff_eq_foldl l₁ l₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(List.foldl List.erase l₁ l₂) =
    foldl erase (_ : ∀ (s : Multiset α) (a b : α), erase (erase s a) b = erase (erase s b) a) ↑l₁ ↑l₂
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
l₁ l₂ : List α
⊢ foldl erase (_ : ∀ (s : Multiset α) (a b : α), erase (erase s a) b = erase (erase s b) a) ↑l₁ ↑l₂ =
    ↑(List.foldl List.erase l₁ l₂)
[PROOFSTEP]
exact foldl_hom _ _ _ _ _ fun x y => rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
h : t ≤ s
⊢ ↑card s = ↑card t + ↑card (s - t)
[PROOFSTEP]
rw [add_comm, ← card_add, tsub_add_cancel_of_le h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u
[PROOFSTEP]
rw [← eq_union_left h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t
[PROOFSTEP]
exact union_le_union_right h₁ t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ List.map f (List.diff l₁ l₂ ++ l₂) = List.diff (List.map f l₁) (List.map f l₂) ++ List.map f l₂
[PROOFSTEP]
rw [List.map_append f, List.map_diff finj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
⊢ 0 ∪ s = s
[PROOFSTEP]
simp [union_def]
  --Porting note: new theorem
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
⊢ s ∪ 0 = s
[PROOFSTEP]
simp [union_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝¹ t✝ u : Multiset α
a✝ b : α
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t : Multiset α), s ∩ t ≤ t
t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t
[PROOFSTEP]
simpa [h] using cons_le_cons a (IH (t.erase a))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝¹ t✝ u : Multiset α
a✝ b : α
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t : Multiset α), s ∩ t ≤ t
t : Multiset α
h : ¬a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t
[PROOFSTEP]
simp [h, IH]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
h₁ : s ≤ t
h₂ : s ≤ u
⊢ s ≤ t ∩ u
[PROOFSTEP]
revert s u
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t : Multiset α
a b : α
⊢ ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
[PROOFSTEP]
refine @(Multiset.induction_on t ?_ fun a t IH => ?_)
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t : Multiset α
a b : α
⊢ ∀ {s u : Multiset α}, s ≤ 0 → s ≤ u → s ≤ 0 ∩ u
[PROOFSTEP]
intros s u h₁ h₂
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
⊢ ∀ {s u : Multiset α}, s ≤ a ::ₘ t → s ≤ u → s ≤ (a ::ₘ t) ∩ u
[PROOFSTEP]
intros s u h₁ h₂
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t : Multiset α
a b : α
s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0 ∩ u
[PROOFSTEP]
simpa only [zero_inter, nonpos_iff_eq_zero] using h₁
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
⊢ s ≤ (a ::ₘ t) ∩ u
[PROOFSTEP]
by_cases h : a ∈ u
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u
[PROOFSTEP]
rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ erase s a ≤ t ∩ erase u a
[PROOFSTEP]
exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u
[PROOFSTEP]
rw [cons_inter_of_neg _ h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
t✝ : Multiset α
a✝ b a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ t ∩ u
[PROOFSTEP]
exact IH ((le_cons_of_not_mem <| mt (mem_of_le h₂) h).1 h₁) h₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ s ∩ t
[PROOFSTEP]
rw [← cons_erase h₁, cons_inter_of_pos _ h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ erase s a ∩ erase t a
[PROOFSTEP]
apply mem_cons_self
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a b : α
h : s ≤ t
⊢ s ∪ t = t
[PROOFSTEP]
rw [union_comm, eq_union_left h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
⊢ s ∪ t + u = s + u ∪ (t + u)
[PROOFSTEP]
simpa [(· ∪ ·), union, eq_comm, add_assoc] using
  show s + u - (t + u) = s - t by rw [add_comm t, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
⊢ s + u - (t + u) = s - t
[PROOFSTEP]
rw [add_comm t, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
⊢ s + (t ∪ u) = s + t ∪ (s + u)
[PROOFSTEP]
rw [add_comm, union_add_distrib, add_comm s, add_comm s]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a✝ b a : α
s t : Multiset α
⊢ a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t
[PROOFSTEP]
simpa using add_union_distrib (a ::ₘ 0) s t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
⊢ s ∩ t + u = (s + u) ∩ (t + u)
[PROOFSTEP]
by_contra h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
h : ¬s ∩ t + u = (s + u) ∩ (t + u)
⊢ False
[PROOFSTEP]
cases'
  lt_iff_cons_le.1
    (lt_of_le_of_ne (le_inter (add_le_add_right (inter_le_left s t) u) (add_le_add_right (inter_le_right s t) u))
      h) with
  a hl
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a✝ b : α
s t u : Multiset α
h : ¬s ∩ t + u = (s + u) ∩ (t + u)
a : α
hl : a ::ₘ (s ∩ t + u) ≤ (s + u) ∩ (t + u)
⊢ False
[PROOFSTEP]
rw [← cons_add] at hl 
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a✝ b : α
s t u : Multiset α
h : ¬s ∩ t + u = (s + u) ∩ (t + u)
a : α
hl : a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)
⊢ False
[PROOFSTEP]
exact
  not_le_of_lt (lt_cons_self (s ∩ t) a)
    (le_inter (le_of_add_le_add_right (le_trans hl (inter_le_left _ _)))
      (le_of_add_le_add_right (le_trans hl (inter_le_right _ _))))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
⊢ s + t ∩ u = (s + t) ∩ (s + u)
[PROOFSTEP]
rw [add_comm, inter_add_distrib, add_comm s, add_comm s]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a✝ b a : α
s t : Multiset α
⊢ a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s ∪ t + s ∩ t = s + t
[PROOFSTEP]
apply _root_.le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s ∪ t + s ∩ t ≤ s + t
[PROOFSTEP]
rw [union_add_distrib]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + s ∩ t ∪ (t + s ∩ t) ≤ s + t
[PROOFSTEP]
refine' union_le (add_le_add_left (inter_le_right _ _) _) _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ∩ t ≤ s + t
[PROOFSTEP]
rw [add_comm]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s ∩ t + t ≤ s + t
[PROOFSTEP]
exact add_le_add_right (inter_le_left _ _) _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t
[PROOFSTEP]
rw [add_comm, add_inter_distrib]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)
[PROOFSTEP]
refine' le_inter (add_le_add_right (le_union_right _ _) _) _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ t + s ≤ s ∪ t + t
[PROOFSTEP]
rw [add_comm]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t
[PROOFSTEP]
exact add_le_add_right (le_union_left _ _) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s - t + s ∩ t = s
[PROOFSTEP]
rw [inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s - t + t ∩ s = s
[PROOFSTEP]
revert s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u : Multiset α
a b : α
t : Multiset α
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s
[PROOFSTEP]
refine' Multiset.induction_on t (by simp) fun a t IH s => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u : Multiset α
a b : α
t : Multiset α
⊢ ∀ (s : Multiset α), s - 0 + 0 ∩ s = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
[PROOFSTEP]
rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝¹ u : Multiset α
a✝ b : α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
[PROOFSTEP]
rw [cons_inter_of_neg _ h, sub_cons, erase_of_not_mem h, IH]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
⊢ s - s ∩ t + ?m.192556 s t = s - t + ?m.192556 s t
[PROOFSTEP]
rw [sub_add_inter s t, tsub_add_cancel_of_le (inter_le_left s t)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Multiset α
_l : List α
h : ∀ (x : α), x ∈ Quot.mk Setoid.r _l → (p x ↔ q x)
⊢ ∀ (x : α), x ∈ _l → (decide (p x) = true ↔ decide (q x) = true)
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (b : α), p b → q b
l : List α
⊢ ∀ (a : α), decide (p a) = true → decide (q a) = true
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
l : List α
h : p a
⊢ decide (p a) = true
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
l : List α
h : ¬p a
⊢ ¬decide (p a) = true
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
_l : List α
⊢ a ∈ filter p (Quot.mk Setoid.r _l) ↔ a ∈ Quot.mk Setoid.r _l ∧ p a
[PROOFSTEP]
simpa using List.mem_filter (p := (p ·))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b => decide (p b)) _l = _l ↔ ∀ (a : α), a ∈ Quot.mk Setoid.r _l → p a
[PROOFSTEP]
simpa using List.filter_eq_self (p := (p ·))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b => decide (p b)) _l = [] ↔ ∀ (a : α), a ∈ Quot.mk Setoid.r _l → ¬p a
[PROOFSTEP]
simpa using List.filter_eq_nil (p := (p ·))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ filter p (a ::ₘ s) = {a} + filter p s
[PROOFSTEP]
rw [filter_cons_of_pos _ h, singleton_add]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ filter p (a ::ₘ s) = 0 + filter p s
[PROOFSTEP]
rw [filter_cons_of_neg _ h, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
a : α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p {a} = if p a then {a} else ∅
[PROOFSTEP]
simp only [singleton, filter_cons, filter_zero, add_zero, empty_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • s) = n • filter p s
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • 0) = n • filter p 0
[PROOFSTEP]
simp only [filter_zero, nsmul_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ ⦃a : α⦄ {s : Multiset α}, filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
[PROOFSTEP]
intro a ha ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • (a ::ₘ ha)) = n • filter p (a ::ₘ ha)
[PROOFSTEP]
rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) + n • filter p ha = (n • if p a then {a} else 0) + n • filter p ha
[PROOFSTEP]
congr
[GOAL]
case refine'_2.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) = n • if p a then {a} else 0
[PROOFSTEP]
split_ifs with hp
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ filter p (n • {a}) = n • {a}
[PROOFSTEP]
simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ ∀ (a_1 : α), a_1 ∈ n • {a} → p a_1
[PROOFSTEP]
intro b hb
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
b : α
hb : b ∈ n • {a}
⊢ p b
[PROOFSTEP]
rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (n • {a}) = n • 0
[PROOFSTEP]
simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ ∀ (a_1 : α), a_1 ∈ n • {a} → ¬p a_1
[PROOFSTEP]
intro b hb
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
b : α
hb : b ∈ n • {a}
⊢ ¬p b
[PROOFSTEP]
rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Multiset α
⊢ filter p (s - t) = filter p s - filter p t
[PROOFSTEP]
revert s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
[PROOFSTEP]
refine' Multiset.induction_on t (by simp) fun a t IH s => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - 0) = filter p s - filter p 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)
[PROOFSTEP]
rw [sub_cons, IH]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)
[PROOFSTEP]
by_cases h : p a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)
[PROOFSTEP]
rw [filter_cons_of_pos _ h, sub_cons]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) - filter p t = erase (filter p s) a - filter p t
[PROOFSTEP]
congr
[GOAL]
case pos.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (erase s a) = erase (filter p s) a
[PROOFSTEP]
by_cases m : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : a ∈ s
⊢ filter p (erase s a) = erase (filter p s) a
[PROOFSTEP]
rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h), cons_erase m]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : ¬a ∈ s
⊢ filter p (erase s a) = erase (filter p s) a
[PROOFSTEP]
rw [erase_of_not_mem m, erase_of_not_mem (mt mem_of_mem_filter m)]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p (a ::ₘ t)
[PROOFSTEP]
rw [filter_cons_of_neg _ h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
⊢ filter p (erase s a) - filter p t = filter p s - filter p t
[PROOFSTEP]
by_cases m : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (erase s a) - filter p t = filter p s - filter p t
[PROOFSTEP]
rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)), cons_erase m]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (erase s a) = filter p (a ::ₘ erase s a)
[PROOFSTEP]
rw [filter_cons_of_neg _ h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (erase s a) - filter p t = filter p s - filter p t
[PROOFSTEP]
rw [erase_of_not_mem m]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Multiset α
⊢ filter p (s ∪ t) = filter p s ∪ filter p t
[PROOFSTEP]
simp [(· ∪ ·), union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
l : List α
⊢ filter p (filter q (Quot.mk Setoid.r l)) = filter (fun a => p a ∧ q a) (Quot.mk Setoid.r l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
by_cases p a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
by_cases p a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
h : p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
by_cases q a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
h : p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
by_cases q a
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
h : ¬p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
by_cases q a
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
h : ¬p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
by_cases q a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
h✝ : p a
h : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
h✝ : p a
h : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
h✝ : ¬p a
h : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
h✝ : ¬p a
h : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ filter p s + filter (fun a => ¬p a) s = s
[PROOFSTEP]
rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + 0 = s
[PROOFSTEP]
simp only [add_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)
[PROOFSTEP]
simp [Decidable.em, -Bool.not_eq_true, -not_and, not_and_or, or_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a
[PROOFSTEP]
simp only [Bool.not_eq_true, decide_eq_true_eq, Bool.eq_false_or_eq_true, decide_True, implies_true, Decidable.em]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ filter p (map f (Quot.mk Setoid.r l)) = map f (filter (p ∘ f) (Quot.mk Setoid.r l))
[PROOFSTEP]
simp [List.map_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ List.map f (List.filter ((fun b => decide (p b)) ∘ f) l) ~ List.map f (List.filter (fun b => decide (p (f b))) l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard p) l = List.filter (fun b => decide (p b)) l
[PROOFSTEP]
rw [← List.filterMap_eq_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard p) l = List.filterMap (Option.guard fun x => decide (p x) = true) l
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ Option.guard p = Option.guard fun x => decide (p x) = true
[PROOFSTEP]
funext a
[GOAL]
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
a : α
⊢ Option.guard p a = Option.guard (fun x => decide (p x) = true) a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
f : α → Option β
s : Multiset α
l : List α
⊢ List.filterMap f (List.filter (fun b => decide (p b)) l) = List.filterMap (fun x => if p x then f x else none) l
[PROOFSTEP]
simpa using List.filterMap_filter p f l
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), p a → countp p (a ::ₘ Quot.mk Setoid.r a_1) = countp p (Quot.mk Setoid.r a_1) + 1
[PROOFSTEP]
simpa using List.countp_cons_of_pos (p ·)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), ¬p a → countp p (a ::ₘ Quot.mk Setoid.r a_1) = countp p (Quot.mk Setoid.r a_1)
[PROOFSTEP]
simpa using List.countp_cons_of_neg (p ·)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
b : α
s : Multiset α
⊢ ∀ (a : List α), countp p (b ::ₘ Quot.mk Setoid.r a) = countp p (Quot.mk Setoid.r a) + if p b then 1 else 0
[PROOFSTEP]
simp [List.countp_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
⊢ countp p (s + t) = countp p s + countp p t
[PROOFSTEP]
simp [countp_eq_card_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ countp p (n • s) = n * countp p s
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ countp p (zero • s) = zero * countp p s
[PROOFSTEP]
simp [*, succ_nsmul', succ_mul, zero_nsmul]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n✝ : ℕ
n_ih✝ : countp p (n✝ • s) = n✝ * countp p s
⊢ countp p (succ n✝ • s) = succ n✝ * countp p s
[PROOFSTEP]
simp [*, succ_nsmul', succ_mul, zero_nsmul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ ↑card (Quot.mk Setoid.r l) = countp p (Quot.mk Setoid.r l) + countp (fun x => ¬p x) (Quot.mk Setoid.r l)
[PROOFSTEP]
simp [l.length_eq_countp_add_countp p]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ countp p (s - t) = countp p s - countp p t
[PROOFSTEP]
simp [countp_eq_card_filter, h, filter_le_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
h : s ≤ t
⊢ countp p s ≤ countp p t
[PROOFSTEP]
simpa [countp_eq_card_filter] using card_le_of_le (filter_le_filter p h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ countp p (filter q s) = countp (fun a => p a ∧ q a) s
[PROOFSTEP]
simp [countp_eq_card_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
l : List α
⊢ countp p (Quot.mk Setoid.r l) =
    countp p (filter q (Quot.mk Setoid.r l)) + countp p (filter (fun a => ¬q a) (Quot.mk Setoid.r l))
[PROOFSTEP]
convert l.countp_eq_countp_filter_add (p ·) (q ·)
[GOAL]
case h.e'_3.h.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
l : List α
⊢ countp p (filter (fun a => ¬q a) (Quot.mk Setoid.r l)) =
    List.countp (fun x => decide (p x)) (List.filter (fun a => decide ¬decide (q a) = true) l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countp p (map f s) = ↑card (filter (fun a => p (f a)) s)
[PROOFSTEP]
refine' Multiset.induction_on s _ fun a t IH => _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countp p (map f 0) = ↑card (filter (fun a => p (f a)) 0)
[PROOFSTEP]
rw [map_zero, countp_zero, filter_zero, card_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countp p (map f t) = ↑card (filter (fun a => p (f a)) t)
⊢ countp p (map f (a ::ₘ t)) = ↑card (filter (fun a => p (f a)) (a ::ₘ t))
[PROOFSTEP]
rw [map_cons, countp_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ 0 < countp p (Quot.mk Setoid.r _l) ↔ ∃ a, a ∈ Quot.mk Setoid.r _l ∧ p a
[PROOFSTEP]
simpa using List.countp_pos (p ·)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countp p (Quot.mk Setoid.r _l) = 0 ↔ ∀ (a : α), a ∈ Quot.mk Setoid.r _l → ¬p a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countp p (Quot.mk Setoid.r _l) = ↑card (Quot.mk Setoid.r _l) ↔ ∀ (a : α), a ∈ Quot.mk Setoid.r _l → p a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
hs : s = s'
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
hp : ∀ (x : α), x ∈ s → p x = p' x
⊢ countp p s = countp p' s'
[PROOFSTEP]
revert hs hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
⊢ s = s' → (∀ (x : α), x ∈ s → p x = p' x) → countp p s = countp p' s'
[PROOFSTEP]
exact
  Quot.induction_on₂ s s'
    (fun l l' hs hp => by
      simp only [quot_mk_to_coe'', coe_eq_coe] at hs 
      apply hs.countp_congr
      simpa using hp)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hs : Quot.mk Setoid.r l = Quot.mk Setoid.r l'
hp : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x = p' x
⊢ countp p (Quot.mk Setoid.r l) = countp p' (Quot.mk Setoid.r l')
[PROOFSTEP]
simp only [quot_mk_to_coe'', coe_eq_coe] at hs 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x = p' x
hs : l ~ l'
⊢ countp p (Quot.mk Setoid.r l) = countp p' (Quot.mk Setoid.r l')
[PROOFSTEP]
apply hs.countp_congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : α → Prop
inst✝² : DecidablePred p✝
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk Setoid.r l → p x = p' x
hs : l ~ l'
⊢ ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)
[PROOFSTEP]
simpa using hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a ↑l = List.count a l
[PROOFSTEP]
simp_rw [count, List.count, coe_countp (a = ·) l, @eq_comm _ a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
l : List α
⊢ List.countp (fun b => decide (b = a)) l = List.countp (fun x => x == a) l
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : α
⊢ count a {b} = if a = b then 1 else 0
[PROOFSTEP]
simp only [count_cons, ← cons_zero, count_zero, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
n : ℕ
s : Multiset α
⊢ count a (n • s) = n * count a s
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a (zero • s) = zero * count a s
[PROOFSTEP]
simp [*, succ_nsmul', succ_mul, zero_nsmul]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
n✝ : ℕ
n_ih✝ : count a (n✝ • s) = n✝ * count a s
⊢ count a (succ n✝ • s) = succ n✝ * count a s
[PROOFSTEP]
simp [*, succ_nsmul', succ_mul, zero_nsmul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ 0 < count a s ↔ a ∈ s
[PROOFSTEP]
simp [count, countp_pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ 1 ≤ count a s ↔ a ∈ s
[PROOFSTEP]
rw [succ_le_iff, count_pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a s ≠ 0 ↔ a ∈ s
[PROOFSTEP]
simp [Ne.def, count_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a s = ↑card s ↔ ∀ (x : α), x ∈ s → a = x
[PROOFSTEP]
simp [countp_eq_card, count, @eq_comm _ a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = n
[PROOFSTEP]
convert List.count_replicate_self a n
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = List.count a (List.replicate n a)
[PROOFSTEP]
rw [← coe_count, coe_replicate]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if a = b then n else 0
[PROOFSTEP]
convert List.count_replicate a b n
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n b)
[PROOFSTEP]
rw [← coe_count, coe_replicate]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase (Quotient.mk (isSetoid α) l) a) = count a (Quotient.mk (isSetoid α) l) - 1
[PROOFSTEP]
convert List.count_erase_self a l
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase (Quotient.mk (isSetoid α) l) a) = List.count a (List.erase l a)
[PROOFSTEP]
rw [← coe_count]
[GOAL]
case h.e'_3.h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (Quotient.mk (isSetoid α) l) = List.count a l
[PROOFSTEP]
rw [← coe_count]
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase (Quotient.mk (isSetoid α) l) a) = count a ↑(List.erase l a)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (Quotient.mk (isSetoid α) l) = count a ↑l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase (Quotient.mk (isSetoid α) l) b) = count a (Quotient.mk (isSetoid α) l)
[PROOFSTEP]
convert List.count_erase_of_ne ab l
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase (Quotient.mk (isSetoid α) l) b) = List.count a (List.erase l b)
[PROOFSTEP]
rw [← coe_count]
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (Quotient.mk (isSetoid α) l) = List.count a l
[PROOFSTEP]
rw [← coe_count]
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase (Quotient.mk (isSetoid α) l) b) = count a ↑(List.erase l b)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (Quotient.mk (isSetoid α) l) = count a ↑l
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) = count a s - count a t
[PROOFSTEP]
revert s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
t : Multiset α
⊢ ∀ (s : Multiset α), count a (s - t) = count a s - count a t
[PROOFSTEP]
refine' Multiset.induction_on t (by simp) fun b t IH s => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
t : Multiset α
⊢ ∀ (s : Multiset α), count a (s - 0) = count a s - count a 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (s - b ::ₘ t) = count a s - count a (b ::ₘ t)
[PROOFSTEP]
rw [sub_cons, IH]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (erase s b) - count a t = count a s - count a (b ::ₘ t)
[PROOFSTEP]
rcases Decidable.eq_or_ne a b with rfl | ab
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
t✝ t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
⊢ count a (erase s a) - count a t = count a s - count a (a ::ₘ t)
[PROOFSTEP]
rw [count_erase_self, count_cons_self, Nat.sub_sub, add_comm]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
t✝ : Multiset α
b : α
t : Multiset α
IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t
s : Multiset α
ab : a ≠ b
⊢ count a (erase s b) - count a t = count a s - count a (b ::ₘ t)
[PROOFSTEP]
rw [count_erase_of_ne ab, count_cons_of_ne ab]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∪ t) = max (count a s) (count a t)
[PROOFSTEP]
simp [(· ∪ ·), union, tsub_add_eq_max]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∩ t) = min (count a s) (count a t)
[PROOFSTEP]
apply @Nat.add_left_cancel (count a (s - t))
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
[PROOFSTEP]
rw [← count_add, sub_add_inter, count_sub, tsub_add_min]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ count a (Quot.mk Setoid.r _l) ↔ replicate n a ≤ Quot.mk Setoid.r _l
[PROOFSTEP]
simp only [quot_mk_to_coe'', mem_coe, coe_count]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ ↑_l
[PROOFSTEP]
exact le_count_iff_replicate_sublist.trans replicate_le_coe.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ count a (filter p (Quot.mk Setoid.r _l)) = count a (Quot.mk Setoid.r _l)
[PROOFSTEP]
simp only [quot_mk_to_coe'', coe_filter, mem_coe, coe_count, decide_eq_true_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ List.count a (List.filter (fun b => decide (p b)) _l) = List.count a _l
[PROOFSTEP]
apply count_filter
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ decide (p a) = true
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ count a (filter p s) = if p a then count a s else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s
[PROOFSTEP]
exact count_filter_of_pos h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0
[PROOFSTEP]
exact count_filter_of_neg h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ _l₁ ≈ _l₂ ↔ ∀ (a : α), count a (Quotient.mk (isSetoid α) _l₁) = count a (Quotient.mk (isSetoid α) _l₂)
[PROOFSTEP]
simp only [quot_mk_to_coe, coe_filter, mem_coe, coe_count, decide_eq_true_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ _l₁ ≈ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂
[PROOFSTEP]
apply perm_iff_count
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : List α
⊢ ↑s ∩ ↑t = ↑(List.bagInter s t)
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(List.bagInter s t)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
al : ∀ (a : α), count a s ≤ count a t
⊢ s ≤ t
[PROOFSTEP]
rw [← (ext.2 fun a => by simp [max_eq_right (al a)] : s ∪ t = t)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
al : ∀ (a : α), count a s ≤ count a t
a : α
⊢ count a (s ∪ t) = count a t
[PROOFSTEP]
simp [max_eq_right (al a)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
al : ∀ (a : α), count a s ≤ count a t
⊢ s ≤ s ∪ t
[PROOFSTEP]
apply le_union_left
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
a : α
⊢ count a (s ⊔ t ⊓ u) = count a ((s ⊔ t) ⊓ (s ⊔ u))
[PROOFSTEP]
simp only [max_min_distrib_left, Multiset.count_inter, Multiset.sup_eq_union, Multiset.count_union,
  Multiset.inf_eq_inter]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α✝
α : Type u_4
β : Type u_5
f : α → β
s : Multiset α
inst✝ : DecidableEq β
b : β
⊢ count b (map f s) = ↑card (filter (fun a => b = f a) s)
[PROOFSTEP]
simp [Bool.beq_eq_decide_eq, eq_comm, count, countp_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s
[PROOFSTEP]
suffices (filter (fun a : α => f x = f a) s).count x = card (filter (fun a : α => f x = f a) s)
  by
  rw [count, countp_map, ← this]
  exact count_filter_of_pos $ rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a => f x = f a) s) = ↑card (filter (fun a => f x = f a) s)
⊢ count (f x) (map f s) = count x s
[PROOFSTEP]
rw [count, countp_map, ← this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a => f x = f a) s) = ↑card (filter (fun a => f x = f a) s)
⊢ count x (filter (fun a => f x = f a) s) = count x s
[PROOFSTEP]
exact count_filter_of_pos $ rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (filter (fun a => f x = f a) s) = ↑card (filter (fun a => f x = f a) s)
[PROOFSTEP]
rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (replicate (↑card (filter (fun a => f x = f a) s)) x) =
    ↑card (replicate (↑card (filter (fun a => f x = f a) s)) x)
[PROOFSTEP]
simp only [count_replicate, eq_self_iff_true, if_true, card_replicate]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ ∀ (b : α), b ∈ filter (fun a => f x = f a) s → f x = f b
[PROOFSTEP]
simp only [mem_filter, beq_iff_eq, and_imp, @eq_comm _ (f x), imp_self, implies_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
⊢ count (f x) (map f s) = count x s
[PROOFSTEP]
by_cases H : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s
[PROOFSTEP]
exact count_map_eq_count f _ (Set.injOn_of_injective hf _) _ H
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = count x s
[PROOFSTEP]
rw [count_eq_zero_of_not_mem H, count_eq_zero, mem_map]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ ¬∃ a, a ∈ s ∧ f a = f x
[PROOFSTEP]
rintro ⟨k, hks, hkx⟩
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
k : α
hks : k ∈ s
hkx : f k = f x
⊢ False
[PROOFSTEP]
rw [hf hkx] at hks 
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
k : α
hks : x ∈ s
hkx : f k = f x
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ filter (fun x => x = b) (Quotient.mk (isSetoid α) l) = replicate (count b (Quotient.mk (isSetoid α) l)) b
[PROOFSTEP]
simp only [quot_mk_to_coe, coe_filter, mem_coe, coe_count]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.filter (fun b_1 => decide (b_1 = b)) l) = replicate (List.count b l) b
[PROOFSTEP]
rw [List.filter_eq' l b, coe_replicate]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
b : α
⊢ filter (Eq b) s = replicate (count b s) b
[PROOFSTEP]
simp_rw [← filter_eq', eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
⊢ replicate n x ∩ s = replicate (min n (count x s)) x
[PROOFSTEP]
ext y
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)
[PROOFSTEP]
rw [count_inter, count_replicate, count_replicate]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
[PROOFSTEP]
by_cases h : y = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : y = x
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
[PROOFSTEP]
simp only [h, if_true]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬y = x
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
[PROOFSTEP]
simp only [h, if_false, zero_min]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ s ∩ replicate n x = replicate (min (count x s) n) x
[PROOFSTEP]
rw [inter_comm, replicate_inter, min_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
⊢ f = g
[PROOFSTEP]
ext s
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
s : Multiset α
⊢ ↑f s = ↑g s
[PROOFSTEP]
induction' s using Multiset.induction_on with a s ih
[GOAL]
case h.empty
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
⊢ ↑f 0 = ↑g 0
[PROOFSTEP]
simp only [_root_.map_zero]
[GOAL]
case h.cons
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
a : α
s : Multiset α
ih : ↑f s = ↑g s
⊢ ↑f (a ::ₘ s) = ↑g (a ::ₘ s)
[PROOFSTEP]
simp only [← singleton_add, _root_.map_add, ih, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t
[PROOFSTEP]
classical
refine' ⟨fun h => le_iff_count.mpr fun a => _, map_le_map⟩
simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t
[PROOFSTEP]
refine' ⟨fun h => le_iff_count.mpr fun a => _, map_le_map⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t
[PROOFSTEP]
simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s = ↑card (filter (fun x => a = x) s)
[PROOFSTEP]
rw [count, countp_eq_card_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ count True (map p s) = ↑card (filter p s)
[PROOFSTEP]
simp only [count_eq_card_filter_eq, map_filter, card_map, Function.comp.left_id, eq_true_eq_id, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑card (filter (fun x => True = p x) s) = ↑card (filter p s)
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h.e_p
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (fun x => True = p x) = p
[PROOFSTEP]
funext _
[GOAL]
case h.e_6.h.e_p.h
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
x✝ : α
⊢ (True = p x✝) = p x✝
[PROOFSTEP]
simp only [eq_iff_iff, true_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ m → r x x) → Rel r m m
[PROOFSTEP]
refine' m.induction_on _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
a✝ : ∀ (x : α), x ∈ 0 → r x x
⊢ Rel r 0 0
[PROOFSTEP]
apply Rel.zero
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
r : α → α → Prop
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)
[PROOFSTEP]
intro a m ih h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)
[PROOFSTEP]
exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ Rel (fun x x_1 => x = x_1) s t ↔ s = t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ Rel (fun x x_1 => x = x_1) s t → s = t
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
h : Rel (fun x x_1 => x = x_1) s t
⊢ s = t
[PROOFSTEP]
induction h
[GOAL]
case mp.zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ 0 = 0
[PROOFSTEP]
simp [*]
[GOAL]
case mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
a✝² b✝ : α
as✝ bs✝ : Multiset α
a✝¹ : a✝² = b✝
a✝ : Rel (fun x x_1 => x = x_1) as✝ bs✝
a_ih✝ : as✝ = bs✝
⊢ a✝² ::ₘ as✝ = b✝ ::ₘ bs✝
[PROOFSTEP]
simp [*]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ s = t → Rel (fun x x_1 => x = x_1) s t
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
h : s = t
⊢ Rel (fun x x_1 => x = x_1) s t
[PROOFSTEP]
subst h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
⊢ Rel (fun x x_1 => x = x_1) s s
[PROOFSTEP]
exact rel_eq_refl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
hst : Rel r s t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b
⊢ Rel p s t
[PROOFSTEP]
induction hst
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), a ∈ 0 → ∀ (b : β), b ∈ 0 → r a b → p a b
⊢ Rel p 0 0
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : (∀ (a : α), a ∈ as✝ → ∀ (b : β), b ∈ bs✝ → r a b → p a b) → Rel p as✝ bs✝
h : ∀ (a : α), a ∈ a✝² ::ₘ as✝ → ∀ (b : β), b ∈ b✝ ::ₘ bs✝ → r a b → p a b
⊢ Rel p (a✝² ::ₘ as✝) (b✝ ::ₘ bs✝)
[PROOFSTEP]
case zero => exact Rel.zero
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), a ∈ 0 → ∀ (b : β), b ∈ 0 → r a b → p a b
⊢ Rel p 0 0
[PROOFSTEP]
case zero => exact Rel.zero
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), a ∈ 0 → ∀ (b : β), b ∈ 0 → r a b → p a b
⊢ Rel p 0 0
[PROOFSTEP]
exact Rel.zero
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : (∀ (a : α), a ∈ as✝ → ∀ (b : β), b ∈ bs✝ → r a b → p a b) → Rel p as✝ bs✝
h : ∀ (a : α), a ∈ a✝² ::ₘ as✝ → ∀ (b : β), b ∈ b✝ ::ₘ bs✝ → r a b → p a b
⊢ Rel p (a✝² ::ₘ as✝) (b✝ ::ₘ bs✝)
[PROOFSTEP]
case cons a b s t hab _hst
  ih =>
  apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
  exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p (a ::ₘ s) (b ::ₘ t)
[PROOFSTEP]
case cons a b s t hab _hst
  ih =>
  apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
  exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p (a ::ₘ s) (b ::ₘ t)
[PROOFSTEP]
apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p✝ : γ → δ → Prop
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t
[PROOFSTEP]
exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
⊢ Rel r (s + u) (t + v)
[PROOFSTEP]
induction hst
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝² ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)
[PROOFSTEP]
case zero => simpa using huv
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)
[PROOFSTEP]
case zero => simpa using huv
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)
[PROOFSTEP]
simpa using huv
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝² ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)
[PROOFSTEP]
case cons a b s t hab hst ih => simpa using ih.cons hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s✝ : Multiset α
t✝ : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
hst : Rel r s t
ih : Rel r (s + u) (t + v)
⊢ Rel r (a ::ₘ s + u) (b ::ₘ t + v)
[PROOFSTEP]
case cons a b s t hab hst ih => simpa using ih.cons hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s✝ : Multiset α
t✝ : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
hst : Rel r s t
ih : Rel r (s + u) (t + v)
⊢ Rel r (a ::ₘ s + u) (b ::ₘ t + v)
[PROOFSTEP]
simpa using ih.cons hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ Rel (flip fun x x_1 => x = x_1) s t ↔ s = t
[PROOFSTEP]
rw [rel_flip, rel_eq, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
b : Multiset β
⊢ Rel r 0 b ↔ b = 0
[PROOFSTEP]
rw [Rel_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨
      Exists fun {a} =>
        Exists fun {b_1} =>
          Exists fun {as} => Exists fun {bs} => r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔
    b = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : Multiset α
⊢ Rel r a 0 ↔ a = 0
[PROOFSTEP]
rw [Rel_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨
      Exists fun {a_1} =>
        Exists fun {b} => Exists fun {as} => Exists fun {bs} => r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔
    a = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
[PROOFSTEP]
generalize hm : a ::ₘ as = m
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
⊢ Rel r m bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
h : Rel r m bs
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
[PROOFSTEP]
induction h generalizing as
[GOAL]
case mp.zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'
case mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m : Multiset α
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : ∀ {as : Multiset α}, a ::ₘ as = as✝ → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs✝ = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a✝² ::ₘ as✝
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ b✝ ::ₘ bs✝ = b ::ₘ bs'
[PROOFSTEP]
case zero => simp at hm 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'
[PROOFSTEP]
case zero => simp at hm 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'
[PROOFSTEP]
simp at hm 
[GOAL]
case mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m : Multiset α
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : ∀ {as : Multiset α}, a ::ₘ as = as✝ → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs✝ = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a✝² ::ₘ as✝
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ b✝ ::ₘ bs✝ = b ::ₘ bs'
[PROOFSTEP]
case cons a' b as' bs ha'b h
  ih =>
  rcases cons_eq_cons.1 hm with (⟨eq₁, eq₂⟩ | ⟨_h, cs, eq₁, eq₂⟩)
  · subst eq₁
    subst eq₂
    exact ⟨b, bs, ha'b, h, rfl⟩
  · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
    exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
[PROOFSTEP]
case cons a' b as' bs ha'b h
  ih =>
  rcases cons_eq_cons.1 hm with (⟨eq₁, eq₂⟩ | ⟨_h, cs, eq₁, eq₂⟩)
  · subst eq₁
    subst eq₂
    exact ⟨b, bs, ha'b, h, rfl⟩
  · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
    exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
[PROOFSTEP]
rcases cons_eq_cons.1 hm with (⟨eq₁, eq₂⟩ | ⟨_h, cs, eq₁, eq₂⟩)
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
eq₁ : a = a'
eq₂ : as = as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
[PROOFSTEP]
subst eq₁
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
as' : Multiset α
bs : Multiset β
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
eq₂ : as = as'
ha'b : r a b
hm : a ::ₘ as = a ::ₘ as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
[PROOFSTEP]
subst eq₂
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
bs : Multiset β
as : Multiset α
ha'b : r a b
h : Rel r as bs
ih : ∀ {as_1 : Multiset α}, a ::ₘ as_1 = as → ∃ b bs', r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs'
hm : a ::ₘ as = a ::ₘ as
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
[PROOFSTEP]
exact ⟨b, bs, ha'b, h, rfl⟩
[GOAL]
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
[PROOFSTEP]
rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
[GOAL]
case inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
b' : β
bs' : Multiset β
h₁ : r a b'
h₂ : Rel r cs bs'
eq : bs = b' ::ₘ bs'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
[PROOFSTEP]
exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs
[PROOFSTEP]
exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
[PROOFSTEP]
rw [← rel_flip, rel_cons_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ (∃ b_1 bs', flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
[PROOFSTEP]
refine' exists₂_congr fun a as' => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as : Multiset α
b : β
bs : Multiset β
a : α
as' : Multiset α
⊢ flip r b a ∧ Rel (flip r) bs as' ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
[PROOFSTEP]
rw [rel_flip, flip]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
⊢ ∀ {bs : Multiset β}, Rel r (0 + as₁) bs ↔ ∃ bs₀ bs₁, Rel r 0 bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ Rel r (a ::ₘ s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r (a ::ₘ s) bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
[PROOFSTEP]
simp only [ih, cons_add, rel_cons_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') ↔
    ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') →
    ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
h : ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
⊢ ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
[PROOFSTEP]
rcases h with ⟨b, bs', hab, h, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
bs' : Multiset β
hab : r a b
h : ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁
⊢ ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ b ::ₘ bs' = bs₀ + bs₁
[PROOFSTEP]
rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ ∃ bs₀_1 bs₁_1,
    (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀_1 = b ::ₘ bs') ∧ Rel r as₁ bs₁_1 ∧ b ::ₘ (bs₀ + bs₁) = bs₀_1 + bs₁_1
[PROOFSTEP]
exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ b ::ₘ (bs₀ + bs₁) = b ::ₘ bs₀ + bs₁
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁) →
    ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
h : ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
⊢ ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
[PROOFSTEP]
rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₀ bs₁ : Multiset β
h : ∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs'
h₁ : Rel r as₁ bs₁
⊢ ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs₀ + bs₁ = b ::ₘ bs'
[PROOFSTEP]
rcases h with ⟨b, bs, hab, h₀, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₁ : Multiset β
h₁ : Rel r as₁ bs₁
b : β
bs : Multiset β
hab : r a b
h₀ : Rel r s bs
⊢ ∃ b_1 bs', r a b_1 ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ b ::ₘ bs + bs₁ = b_1 ::ₘ bs'
[PROOFSTEP]
exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs₁ : Multiset β
h₁ : Rel r as₁ bs₁
b : β
bs : Multiset β
hab : r a b
h₀ : Rel r s bs
⊢ b ::ₘ bs + bs₁ = b ::ₘ (bs + bs₁)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
[PROOFSTEP]
rw [← rel_flip, rel_add_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
[PROOFSTEP]
simp [rel_flip]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset γ
f : γ → α
⊢ ∀ {t : Multiset β}, Rel r (map f 0) t ↔ Rel (fun a b => r (f a) b) 0 t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset γ
f : γ → α
⊢ ∀ ⦃a : γ⦄ {s : Multiset γ},
    (∀ {t : Multiset β}, Rel r (map f s) t ↔ Rel (fun a b => r (f a) b) s t) →
      ∀ {t : Multiset β}, Rel r (map f (a ::ₘ s)) t ↔ Rel (fun a b => r (f a) b) (a ::ₘ s) t
[PROOFSTEP]
simp (config := { contextual := true }) [rel_cons_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel r s (map f t) ↔ Rel (fun a b => r a (f b)) s t
[PROOFSTEP]
rw [← rel_flip, rel_map_left, ← rel_flip]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b => flip r (f a) b) s t ↔ Rel (fun a b => r a (f b)) s t
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ↑card s = ↑card t
[PROOFSTEP]
induction h
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ ↑card 0 = ↑card 0
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : ↑card as✝ = ↑card bs✝
⊢ ↑card (a✝² ::ₘ as✝) = ↑card (b✝ ::ₘ bs✝)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
[PROOFSTEP]
induction' h with x y s t hxy _hst ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ ∀ {a : α}, a ∈ 0 → ∃ b, b ∈ 0 ∧ r a b
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
⊢ ∀ {a : α}, a ∈ x ::ₘ s → ∃ b, b ∈ y ::ₘ t ∧ r a b
[PROOFSTEP]
intro a ha
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha : a ∈ x ::ₘ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
[PROOFSTEP]
cases' mem_cons.1 ha with ha ha
[GOAL]
case cons.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
[PROOFSTEP]
exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
[GOAL]
case cons.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
[PROOFSTEP]
rcases ih ha with ⟨b, hbt, hab⟩
[GOAL]
case cons.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
b : β
hbt : b ∈ t
hab : r a b
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
[PROOFSTEP]
exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m1 m2 : Multiset α
r : α → α → Prop
h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b
hc : ↑card m1 = ↑card m2
⊢ Rel r m1 m2
[PROOFSTEP]
revert m1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) → ↑card m1 = ↑card m2 → Rel r m1 m2
[PROOFSTEP]
refine' @(m2.induction_on _ _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ 0 → r a b) → ↑card m1 = ↑card 0 → Rel r m1 0
[PROOFSTEP]
intro m _h hc
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : ↑card m = ↑card 0
⊢ Rel r m 0
[PROOFSTEP]
rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → ↑card m1 = ↑card s → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → ↑card m1 = ↑card (a ::ₘ s) → Rel r m1 (a ::ₘ s)
[PROOFSTEP]
intro a t ih m h hc
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card (a ::ₘ t)
⊢ Rel r m (a ::ₘ t)
[PROOFSTEP]
rw [card_cons] at hc 
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card t + 1
⊢ Rel r m (a ::ₘ t)
[PROOFSTEP]
obtain ⟨b, hb⟩ := card_pos_iff_exists_mem.1 (show 0 < card m from hc.symm ▸ Nat.succ_pos _)
[GOAL]
case refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card t + 1
b : α
hb : b ∈ m
⊢ Rel r m (a ::ₘ t)
[PROOFSTEP]
obtain ⟨m', rfl⟩ := exists_cons_of_mem hb
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ Rel r (b ::ₘ m') (a ::ₘ t)
[PROOFSTEP]
refine' rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih _ _, rfl⟩
[GOAL]
case refine'_2.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ ∀ (a b : α), a ∈ m' → b ∈ t → r a b
[PROOFSTEP]
exact fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)
[GOAL]
case refine'_2.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ ↑card m' = ↑card t
[PROOFSTEP]
simpa using hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
⊢ r a x
[PROOFSTEP]
obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
⊢ r a x
[PROOFSTEP]
rwa [eq_of_mem_replicate hb1] at hb2 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s t u : Multiset α
r1 : Rel r s t
r2 : Rel r t u
⊢ Rel r s u
[PROOFSTEP]
induction' t using Multiset.induction_on with x t ih generalizing s u
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s✝ t u✝ : Multiset α
r1✝ : Rel r s✝ t
r2✝ : Rel r t u✝
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r s u
[PROOFSTEP]
rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s✝ t✝ u✝ : Multiset α
r1✝ : Rel r s✝ t✝
r2✝ : Rel r t✝ u✝
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
s u : Multiset α
r1 : Rel r s (x ::ₘ t)
r2 : Rel r (x ::ₘ t) u
⊢ Rel r s u
[PROOFSTEP]
obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
[GOAL]
case cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s t✝ u✝ : Multiset α
r1✝ : Rel r s t✝
r2✝ : Rel r t✝ u✝
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
u : Multiset α
r2 : Rel r (x ::ₘ t) u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
⊢ Rel r (a ::ₘ as) u
[PROOFSTEP]
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
[GOAL]
case cons.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝ : IsTrans α r
s t✝ u : Multiset α
r1✝ : Rel r s t✝
r2✝ : Rel r t✝ u
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
b : α
bs : Multiset α
hb1 : r x b
hb2 : Rel r t bs
r2 : Rel r (x ::ₘ t) (b ::ₘ bs)
⊢ Rel r (a ::ₘ as) (b ::ₘ bs)
[PROOFSTEP]
exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h : Rel r s t
⊢ countp (r x) s = countp (r x) t
[PROOFSTEP]
induction' s using Multiset.induction_on with y s ih generalizing t
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s t✝ : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s t✝
t : Multiset α
h : Rel r 0 t
⊢ countp (r x) 0 = countp (r x) t
[PROOFSTEP]
rw [rel_zero_left.mp h]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t✝ : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t✝
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countp (r x) s = countp (r x) t
t : Multiset α
h : Rel r (y ::ₘ s) t
⊢ countp (r x) (y ::ₘ s) = countp (r x) t
[PROOFSTEP]
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
[GOAL]
case cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countp (r x) s = countp (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ countp (r x) (y ::ₘ s) = countp (r x) (b ::ₘ bs)
[PROOFSTEP]
rw [countp_cons, countp_cons, ih hb2]
[GOAL]
case cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countp (r x) s = countp (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countp (r x) bs + if r x y then 1 else 0) = countp (r x) bs + if r x b then 1 else 0
[PROOFSTEP]
simp only [decide_eq_true_eq, add_right_inj]
[GOAL]
case cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : IsSymm α r
s✝ t : Multiset α
x : α
inst✝ : DecidablePred (r x)
h✝ : Rel r s✝ t
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countp (r x) s = countp (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (if r x y then 1 else 0) = if r x b then 1 else 0
[PROOFSTEP]
refine' (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s = map f t ↔ s = t
[PROOFSTEP]
rw [← rel_eq, ← rel_eq, rel_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp only [hf.eq_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s t : Multiset α
hst : Rel r s t
a✝ b✝ : α
as✝ bs✝ : Multiset α
hab : r a✝ b✝
_hst : Rel r as✝ bs✝
ih : map (Quot.mk r) as✝ = map (Quot.mk r) bs✝
⊢ map (Quot.mk r) (a✝ ::ₘ as✝) = map (Quot.mk r) (b✝ ::ₘ bs✝)
[PROOFSTEP]
simp [ih, Quot.sound hab]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Multiset α
⊢ Disjoint s t ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
[PROOFSTEP]
simp [disjoint_left, imp_not_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : Multiset α
a : α
⊢ Disjoint {a} l ↔ ¬a ∈ l
[PROOFSTEP]
simp [Disjoint]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : Multiset α
a : α
⊢ Disjoint l {a} ↔ ¬a ∈ l
[PROOFSTEP]
rw [disjoint_comm, singleton_disjoint]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t u : Multiset α
⊢ Disjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u
[PROOFSTEP]
simp [Disjoint, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t u : Multiset α
⊢ Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u
[PROOFSTEP]
rw [disjoint_comm, disjoint_add_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t u : Multiset α
⊢ Disjoint t s ∧ Disjoint u s ↔ Disjoint s t ∧ Disjoint s u
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s t : Multiset α
⊢ Disjoint {a} t ∧ Disjoint s t ↔ ¬a ∈ t ∧ Disjoint s t
[PROOFSTEP]
rw [singleton_disjoint]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s t : Multiset α
⊢ Disjoint s (a ::ₘ t) ↔ ¬a ∈ s ∧ Disjoint s t
[PROOFSTEP]
rw [disjoint_comm, disjoint_cons_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t = 0 ↔ Disjoint s t
[PROOFSTEP]
rw [← subset_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ Disjoint s t
[PROOFSTEP]
simp [subset_iff, Disjoint]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
⊢ Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
[PROOFSTEP]
simp [Disjoint, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u : Multiset α
⊢ Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
[PROOFSTEP]
simp [Disjoint, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ Disjoint s t
[PROOFSTEP]
simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero, Nat.min_eq_zero_iff,
  Nat.add_eq_max_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
⊢ Disjoint (map f s) (map g t) ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a ≠ g b
[PROOFSTEP]
simp [Disjoint, @eq_comm _ (f _) (g _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
l : List α
⊢ ∀ (a : List α), ↑l = ↑a ∧ List.Pairwise r a ↔ l ~ a ∧ List.Pairwise r a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a | a ∈ m} fun a₁ a₂ => r (f a₁) (f a₂)
b₁ : β
h₁ : b₁ ∈ {b | b ∈ map f m}
b₂ : β
h₂ : b₂ ∈ {b | b ∈ map f m}
hn : b₁ ≠ b₂
⊢ r b₁ b₂
[PROOFSTEP]
obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
r : β → β → Prop
m : Multiset α
h : Set.Pairwise {a | a ∈ m} fun a₁ a₂ => r (f a₁) (f a₂)
a₁ : α
H₁ : a₁ ∈ m
h₁ : f a₁ ∈ {b | b ∈ map f m}
a₂ : α
H₂ : a₂ ∈ m
h₂ : f a₂ ∈ {b | b ∈ map f m}
hn : f a₁ ≠ f a₂
⊢ r (f a₁) (f a₂)
[PROOFSTEP]
exact h H₁ H₂ (mt (congr_arg f) hn)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
⊢ ∀ (a b : List α) (p_1 : a ≈ b),
    Eq.ndrec (motive := fun x => (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a })
        (fun ex_unique => List.chooseX p a (_ : ∃ x, x ∈ a ∧ p x))
        (_ : Quotient.mk (isSetoid α) a = Quotient.mk (isSetoid α) b) =
      fun ex_unique => List.chooseX p b (_ : ∃ x, x ∈ b ∧ p x)
[PROOFSTEP]
intros a b _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
⊢ Eq.ndrec (motive := fun x => (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a })
      (fun ex_unique => List.chooseX p a (_ : ∃ x, x ∈ a ∧ p x))
      (_ : Quotient.mk (isSetoid α) a = Quotient.mk (isSetoid α) b) =
    fun ex_unique => List.chooseX p b (_ : ∃ x, x ∈ b ∧ p x)
[PROOFSTEP]
funext hp
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ Quotient.mk (isSetoid α) b ∧ p a
⊢ Eq.ndrec (motive := fun x => (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a })
      (fun ex_unique => List.chooseX p a (_ : ∃ x, x ∈ a ∧ p x))
      (_ : Quotient.mk (isSetoid α) a = Quotient.mk (isSetoid α) b) hp =
    List.chooseX p b (_ : ∃ x, x ∈ b ∧ p x)
[PROOFSTEP]
suffices all_equal : ∀ x y : { t // t ∈ b ∧ p t }, x = y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ Quotient.mk (isSetoid α) b ∧ p a
all_equal : ∀ (x y : { t // t ∈ b ∧ p t }), x = y
⊢ Eq.ndrec (motive := fun x => (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a })
      (fun ex_unique => List.chooseX p a (_ : ∃ x, x ∈ a ∧ p x))
      (_ : Quotient.mk (isSetoid α) a = Quotient.mk (isSetoid α) b) hp =
    List.chooseX p b (_ : ∃ x, x ∈ b ∧ p x)
[PROOFSTEP]
apply all_equal
[GOAL]
case all_equal
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ Quotient.mk (isSetoid α) b ∧ p a
⊢ ∀ (x y : { t // t ∈ b ∧ p t }), x = y
[PROOFSTEP]
rintro ⟨x, px⟩ ⟨y, py⟩
[GOAL]
case all_equal.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ Quotient.mk (isSetoid α) b ∧ p a
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
⊢ { val := x, property := px } = { val := y, property := py }
[PROOFSTEP]
rcases hp with ⟨z, ⟨_z_mem_l, _pz⟩, z_unique⟩
[GOAL]
case all_equal.mk.mk.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun a => a ∈ Quotient.mk (isSetoid α) b ∧ p a) y → y = z
_z_mem_l : z ∈ Quotient.mk (isSetoid α) b
_pz : p z
⊢ { val := x, property := px } = { val := y, property := py }
[PROOFSTEP]
congr
[GOAL]
case all_equal.mk.mk.intro.intro.intro.e_val
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun a => a ∈ Quotient.mk (isSetoid α) b ∧ p a) y → y = z
_z_mem_l : z ∈ Quotient.mk (isSetoid α) b
_pz : p z
⊢ x = y
[PROOFSTEP]
calc
  x = z := z_unique x px
  _ = y := (z_unique y py).symm
