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

case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
a_ih✝ : ∀ (t : List α), List.bagInter l₁✝ t ~ List.bagInter l₂✝ t
t : List α
⊢ List.bagInter (x :: l₁✝) t ~ List.bagInter (x :: l₂✝) t

case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t

case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih_1 : ∀ (t : List α), List.bagInter l₁✝ t ~ List.bagInter l₂✝ t
ih_2 : ∀ (t : List α), List.bagInter l₂✝ t ~ List.bagInter l₃✝ t
t : List α
⊢ List.bagInter l₁✝ t ~ List.bagInter l₃✝ t
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
⊢ List.bagInter l₁ t ~ List.bagInter l₂ t
induction' h with x _ _ _ _ x y _ _ _ _ _ _ ih_1 ih_2 generalizing t
no goals
case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ t : List α
⊢ List.bagInter [] t ~ List.bagInter [] t
simp
no goals
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
a_ih✝ : ∀ (t : List α), List.bagInter l₁✝ t ~ List.bagInter l₂✝ t
t : List α
⊢ List.bagInter (x :: l₁✝) t ~ List.bagInter (x :: l₂✝) t
by_cases x ∈ t <;> simp [*, Perm.cons]
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : x = y
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t

case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
by_cases h : x = y
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : x ∈ t
yt : y ∈ t
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t

case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : x ∈ t
yt : ¬y ∈ t
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t

case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : ¬x ∈ t
yt : y ∈ t
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t

case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : ¬x ∈ t
yt : ¬y ∈ t
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t
no goals
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : x = y
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
simp [h]
no goals
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : x ∈ t
yt : y ∈ t
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]
no goals
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : x ∈ t
yt : ¬y ∈ t
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
simp [xt, yt, mt mem_of_mem_erase, Perm.cons]
no goals
case pos
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : ¬x ∈ t
yt : y ∈ t
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
simp [xt, yt, mt mem_of_mem_erase, Perm.cons]
no goals
case neg
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : ¬x ∈ t
yt : ¬y ∈ t
⊢ List.bagInter (y :: x :: l✝) t ~ List.bagInter (x :: y :: l✝) t
simp [xt, yt]
no goals
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t✝ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih_1 : ∀ (t : List α), List.bagInter l₁✝ t ~ List.bagInter l₂✝ t
ih_2 : ∀ (t : List α), List.bagInter l₂✝ t ~ List.bagInter l₃✝ t
t : List α
⊢ List.bagInter l₁✝ t ~ List.bagInter l₃✝ t
exact (ih_1 _).trans (ih_2 _)