-- Mathlib/Data/List/Lattice.lean
theorem mem_bagInter {a : α} : ∀ {l₁ l₂ : List α}, a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
  | [], l₂ => by simp only [nil_bagInter, not_mem_nil, false_and]
  | b :: l₁, l₂ => by
    by_cases h : b ∈ l₂
    · rw [cons_bagInter_of_pos _ h, mem_cons, mem_cons, mem_bagInter]
      by_cases ba : a = b
      · simp only [ba, h, eq_self_iff_true, true_or, true_and]
      · simp only [mem_erase_of_ne ba, ba, false_or]
    · rw [cons_bagInter_of_neg _ h, mem_bagInter, mem_cons, or_and_right]
      symm
      apply or_iff_right_of_imp
      rintro ⟨rfl, h'⟩
      exact h.elim h'

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₂ : List α
⊢ a ∈ [].bagInter l₂ ↔ a ∈ [] ∧ a ∈ l₂

Tactic:
simp only [nil_bagInter, not_mem_nil, false_and]

Result:
no goals

Proof state:
case neg.ha
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a = b ∧ a ∈ l₂ → a ∈ l₁ ∧ a ∈ l₂

Tactic:
rintro ⟨rfl, h'⟩

Result:
case neg.ha.intro
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h' : a ∈ l₂
h : ¬a ∈ l₂
⊢ a ∈ l₁ ∧ a ∈ l₂

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a ∈ (b :: l₁).bagInter l₂ ↔ a ∈ b :: l₁ ∧ a ∈ l₂

Tactic:
rw [cons_bagInter_of_neg _ h, mem_bagInter, mem_cons, or_and_right]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a ∈ l₁ ∧ a ∈ l₂ ↔ a = b ∧ a ∈ l₂ ∨ a ∈ l₁ ∧ a ∈ l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
⊢ a ∈ (b :: l₁).bagInter l₂ ↔ a ∈ b :: l₁ ∧ a ∈ l₂

Tactic:
by_cases h : b ∈ l₂

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ a ∈ (b :: l₁).bagInter l₂ ↔ a ∈ b :: l₁ ∧ a ∈ l₂

case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a ∈ (b :: l₁).bagInter l₂ ↔ a ∈ b :: l₁ ∧ a ∈ l₂

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
ba : ¬a = b
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ l₂.erase b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂

Tactic:
simp only [mem_erase_of_ne ba, ba, false_or]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ a ∈ (b :: l₁).bagInter l₂ ↔ a ∈ b :: l₁ ∧ a ∈ l₂

Tactic:
rw [cons_bagInter_of_pos _ h, mem_cons, mem_cons, mem_bagInter]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ l₂.erase b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
ba : a = b
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ l₂.erase b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂

Tactic:
simp only [ba, h, eq_self_iff_true, true_or, true_and]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a = b ∧ a ∈ l₂ ∨ a ∈ l₁ ∧ a ∈ l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

Tactic:
apply or_iff_right_of_imp

Result:
case neg.ha
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a = b ∧ a ∈ l₂ → a ∈ l₁ ∧ a ∈ l₂

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ l₂.erase b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂

Tactic:
by_cases ba : a = b

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
ba : a = b
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ l₂.erase b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂

case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b ∈ l₂
ba : ¬a = b
⊢ a = b ∨ a ∈ l₁ ∧ a ∈ l₂.erase b ↔ (a = b ∨ a ∈ l₁) ∧ a ∈ l₂

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a ∈ l₁ ∧ a ∈ l₂ ↔ a = b ∧ a ∈ l₂ ∨ a ∈ l₁ ∧ a ∈ l₂

Tactic:
symm

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ a = b ∧ a ∈ l₂ ∨ a ∈ l₁ ∧ a ∈ l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

Proof state:
case neg.ha.intro
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h' : a ∈ l₂
h : ¬a ∈ l₂
⊢ a ∈ l₁ ∧ a ∈ l₂

Tactic:
exact h.elim h'

Result:
no goals