case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁✝ t₂✝ : List α
p✝ : t₁✝ ~ t₂✝
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ List.bagInter [] t₁ = List.bagInter [] t₂

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁✝ t₂✝ : List α
p✝ : t₁✝ ~ t₂✝
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → List.bagInter l t₁ = List.bagInter l t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ List.bagInter (a :: l) t₁ = List.bagInter (a :: l) t₂
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
l t₁ t₂ : List α
p : t₁ ~ t₂
⊢ List.bagInter l t₁ = List.bagInter l t₂
induction' l with a l IH generalizing t₁ t₂ p
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁✝ t₂✝ : List α
p✝ : t₁✝ ~ t₂✝
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → List.bagInter l t₁ = List.bagInter l t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : a ∈ t₁
⊢ List.bagInter (a :: l) t₁ = List.bagInter (a :: l) t₂

case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁✝ t₂✝ : List α
p✝ : t₁✝ ~ t₂✝
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → List.bagInter l t₁ = List.bagInter l t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : ¬a ∈ t₁
⊢ List.bagInter (a :: l) t₁ = List.bagInter (a :: l) t₂
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁✝ t₂✝ : List α
p✝ : t₁✝ ~ t₂✝
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → List.bagInter l t₁ = List.bagInter l t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ List.bagInter (a :: l) t₁ = List.bagInter (a :: l) t₂
by_cases h : a ∈ t₁
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁✝ t₂✝ : List α
p✝ : t₁✝ ~ t₂✝
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ List.bagInter [] t₁ = List.bagInter [] t₂
simp
no goals
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁✝ t₂✝ : List α
p✝ : t₁✝ ~ t₂✝
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → List.bagInter l t₁ = List.bagInter l t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : a ∈ t₁
⊢ List.bagInter (a :: l) t₁ = List.bagInter (a :: l) t₂
simp [h, p.subset h, IH (p.erase _)]
no goals
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁✝ t₂✝ : List α
p✝ : t₁✝ ~ t₂✝
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → List.bagInter l t₁ = List.bagInter l t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : ¬a ∈ t₁
⊢ List.bagInter (a :: l) t₁ = List.bagInter (a :: l) t₂
simp [h, mt p.mem_iff.2 h, IH p]