-- Mathlib/Data/List/Lattice.lean
theorem count_bagInter {a : α} :
    ∀ {l₁ l₂ : List α}, count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)
  | [], l₂ => by simp
  | l₁, [] => by simp
  | b :: l₁, l₂ => by
    by_cases hb : b ∈ l₂
    · rw [cons_bagInter_of_pos _ hb, count_cons, count_cons, count_bagInter, count_erase,
        ← Nat.add_min_add_right]
      by_cases ba : b = a
      · simp only [beq_iff_eq]
        rw [if_pos ba, Nat.sub_add_cancel]
        rwa [succ_le_iff, count_pos_iff, ← ba]
      · simp only [beq_iff_eq]
        rw [if_neg ba, Nat.sub_zero, Nat.add_zero, Nat.add_zero]
    · rw [cons_bagInter_of_neg _ hb, count_bagInter]
      by_cases ab : a = b
      · rw [← ab] at hb
        rw [count_eq_zero.2 hb, Nat.min_zero, Nat.min_zero]
      · rw [count_cons_of_ne ab]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ count a (l₁.bagInter []) = count a l₁ ⊓ count a []

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ count a ((b :: l₁).bagInter l₂) = count a (b :: l₁) ⊓ count a l₂

Tactic:
rw [cons_bagInter_of_pos _ hb, count_cons, count_cons, count_bagInter, count_erase,
  ← Nat.add_min_add_right]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ (count a l₁ + if (b == a) = true then 1 else 0) ⊓
      ((count a l₂ - if (b == a) = true then 1 else 0) + if (b == a) = true then 1 else 0) =
    (count a l₁ + if (b == a) = true then 1 else 0) ⊓ count a l₂

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ count a ((b :: l₁).bagInter l₂) = count a (b :: l₁) ⊓ count a l₂

Tactic:
rw [cons_bagInter_of_neg _ hb, count_bagInter]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ count a l₁ ⊓ count a l₂ = count a (b :: l₁) ⊓ count a l₂

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : b = a
⊢ (count a l₁ + if b = a then 1 else 0) ⊓ ((count a l₂ - if b = a then 1 else 0) + if b = a then 1 else 0) =
    (count a l₁ + if b = a then 1 else 0) ⊓ count a l₂

Tactic:
rw [if_pos ba, Nat.sub_add_cancel]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : b = a
⊢ 1 ≤ count a l₂

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬a ∈ l₂
ab : a = b
⊢ count a l₁ ⊓ count a l₂ = count a (b :: l₁) ⊓ count a l₂

Tactic:
rw [count_eq_zero.2 hb, Nat.min_zero, Nat.min_zero]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : ¬b = a
⊢ (count a l₁ + if (b == a) = true then 1 else 0) ⊓
      ((count a l₂ - if (b == a) = true then 1 else 0) + if (b == a) = true then 1 else 0) =
    (count a l₁ + if (b == a) = true then 1 else 0) ⊓ count a l₂

Tactic:
simp only [beq_iff_eq]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : ¬b = a
⊢ (count a l₁ + if b = a then 1 else 0) ⊓ ((count a l₂ - if b = a then 1 else 0) + if b = a then 1 else 0) =
    (count a l₁ + if b = a then 1 else 0) ⊓ count a l₂

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ (count a l₁ + if (b == a) = true then 1 else 0) ⊓
      ((count a l₂ - if (b == a) = true then 1 else 0) + if (b == a) = true then 1 else 0) =
    (count a l₁ + if (b == a) = true then 1 else 0) ⊓ count a l₂

Tactic:
by_cases ba : b = a

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : b = a
⊢ (count a l₁ + if (b == a) = true then 1 else 0) ⊓
      ((count a l₂ - if (b == a) = true then 1 else 0) + if (b == a) = true then 1 else 0) =
    (count a l₁ + if (b == a) = true then 1 else 0) ⊓ count a l₂

case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : ¬b = a
⊢ (count a l₁ + if (b == a) = true then 1 else 0) ⊓
      ((count a l₂ - if (b == a) = true then 1 else 0) + if (b == a) = true then 1 else 0) =
    (count a l₁ + if (b == a) = true then 1 else 0) ⊓ count a l₂

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : b = a
⊢ (count a l₁ + if (b == a) = true then 1 else 0) ⊓
      ((count a l₂ - if (b == a) = true then 1 else 0) + if (b == a) = true then 1 else 0) =
    (count a l₁ + if (b == a) = true then 1 else 0) ⊓ count a l₂

Tactic:
simp only [beq_iff_eq]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : b = a
⊢ (count a l₁ + if b = a then 1 else 0) ⊓ ((count a l₂ - if b = a then 1 else 0) + if b = a then 1 else 0) =
    (count a l₁ + if b = a then 1 else 0) ⊓ count a l₂

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : a = b
⊢ count a l₁ ⊓ count a l₂ = count a (b :: l₁) ⊓ count a l₂

Tactic:
rw [← ab] at hb

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬a ∈ l₂
ab : a = b
⊢ count a l₁ ⊓ count a l₂ = count a (b :: l₁) ⊓ count a l₂

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : ¬b = a
⊢ (count a l₁ + if b = a then 1 else 0) ⊓ ((count a l₂ - if b = a then 1 else 0) + if b = a then 1 else 0) =
    (count a l₁ + if b = a then 1 else 0) ⊓ count a l₂

Tactic:
rw [if_neg ba, Nat.sub_zero, Nat.add_zero, Nat.add_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
⊢ count a ((b :: l₁).bagInter l₂) = count a (b :: l₁) ⊓ count a l₂

Tactic:
by_cases hb : b ∈ l₂

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
⊢ count a ((b :: l₁).bagInter l₂) = count a (b :: l₁) ⊓ count a l₂

case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ count a ((b :: l₁).bagInter l₂) = count a (b :: l₁) ⊓ count a l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₂ : List α
⊢ count a ([].bagInter l₂) = count a [] ⊓ count a l₂

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : b ∈ l₂
ba : b = a
⊢ 1 ≤ count a l₂

Tactic:
rwa [succ_le_iff, count_pos_iff, ← ba]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : ¬a = b
⊢ count a l₁ ⊓ count a l₂ = count a (b :: l₁) ⊓ count a l₂

Tactic:
rw [count_cons_of_ne ab]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
⊢ count a l₁ ⊓ count a l₂ = count a (b :: l₁) ⊓ count a l₂

Tactic:
by_cases ab : a = b

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : a = b
⊢ count a l₁ ⊓ count a l₂ = count a (b :: l₁) ⊓ count a l₂

case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
hb : ¬b ∈ l₂
ab : ¬a = b
⊢ count a l₁ ⊓ count a l₂ = count a (b :: l₁) ⊓ count a l₂