no goals
α : Type u_1
l l₁ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₂ : List α
⊢ count a (List.bagInter [] l₂) = min (count a []) (count a l₂)
simp
no goals
α : Type u_1
l l₁✝ l₂ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ count a (List.bagInter l₁ []) = min (count a l₁) (count a [])
simp
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ count a (List.bagInter (b :: l₁) l₂) = min (count a (b :: l₁)) (count a l₂)

case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ count a (List.bagInter (b :: l₁) l₂) = min (count a (b :: l₁)) (count a l₂)
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
⊢ count a (List.bagInter (b :: l₁) l₂) = min (count a (b :: l₁)) (count a l₂)
by_cases hb : b ∈ l₂
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ count a (List.bagInter (b :: l₁) l₂) = min (count a (b :: l₁)) (count a l₂)
rw [cons_bagInter_of_pos _ hb, count_cons', count_cons', count_bagInter, count_erase, ←
  min_add_add_right]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : a = b
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)

case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : ¬a = b
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)
by_cases ab : a = b
case pos.h
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : a = b
⊢ 1 ≤ count a l₂
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : a = b
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)
rw [if_pos ab, @tsub_add_cancel_of_le]
no goals
case pos.h
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : a = b
⊢ 1 ≤ count a l₂
rwa [succ_le_iff, count_pos, ab]
no goals
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ab : ¬a = b
⊢ min (count a l₁ + if a = b then 1 else 0) ((count a l₂ - if a = b then 1 else 0) + if a = b then 1 else 0) =
    min (count a l₁ + if a = b then 1 else 0) (count a l₂)
rw [if_neg ab, tsub_zero, add_zero, add_zero]
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ count a (List.bagInter (b :: l₁) l₂) = min (count a (b :: l₁)) (count a l₂)
rw [cons_bagInter_of_neg _ hb, count_bagInter]
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)

case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : ¬a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
by_cases ab : a = b
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬a ∈ l₂
ab : a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
rw [← ab] at hb
no goals
case pos
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬a ∈ l₂
ab : a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
rw [count_eq_zero.2 hb, min_zero, min_zero]
no goals
case neg
α : Type u_1
l l₁✝ l₂✝ : List α
p : α → Prop
a✝ : α
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : ¬a = b
⊢ min (count a l₁) (count a l₂) = min (count a (b :: l₁)) (count a l₂)
rw [count_cons_of_ne ab]