-- Mathlib/Data/List/Perm/Lattice.lean
theorem Perm.bagInter_right {l₁ l₂ : List α} (t : List α) (h : l₁ ~ l₂) :
    l₁.bagInter t ~ l₂.bagInter t

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

Tactic:
simp [xt, yt, mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm, swap]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : x ∉ t
yt : y ∈ t
⊢ (y :: x :: l✝).bagInter t ~ (x :: y :: l✝).bagInter t

Tactic:
simp [xt, yt, mt mem_of_mem_erase, Perm.cons]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x y : α
l✝ t : List α
h : ¬x = y
⊢ (y :: x :: l✝).bagInter t ~ (x :: y :: l✝).bagInter t

Tactic:
by_cases xt : x ∈ t <;> by_cases yt : y ∈ t

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

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

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

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

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : x ∈ t
yt : y ∉ t
⊢ (y :: x :: l✝).bagInter t ~ (x :: y :: l✝).bagInter t

Tactic:
simp [xt, yt, mt mem_of_mem_erase, Perm.cons]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
a_ih✝ : ∀ (t : List α), l₁✝.bagInter t ~ l₂✝.bagInter t
t : List α
⊢ (x :: l₁✝).bagInter t ~ (x :: l₂✝).bagInter t

Tactic:
by_cases x ∈ t <;> simp [*, Perm.cons]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x y : α
l✝ t : List α
h : x = y
⊢ (y :: x :: l✝).bagInter t ~ (x :: y :: l✝).bagInter t

Tactic:
simp [h]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t : List α
⊢ [].bagInter t ~ [].bagInter t

Tactic:
simp

Result:
no goals

Proof state:
case swap
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x y : α
l✝ t : List α
⊢ (y :: x :: l✝).bagInter t ~ (x :: y :: l✝).bagInter t

Tactic:
by_cases h : x = y

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x y : α
l✝ t : List α
h : x = y
⊢ (y :: x :: l✝).bagInter t ~ (x :: y :: l✝).bagInter t

case neg
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x y : α
l✝ t : List α
h : ¬x = y
⊢ (y :: x :: l✝).bagInter t ~ (x :: y :: l✝).bagInter t

Proof state:
case trans
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih_1 : ∀ (t : List α), l₁✝.bagInter t ~ l₂✝.bagInter t
ih_2 : ∀ (t : List α), l₂✝.bagInter t ~ l₃✝.bagInter t
t : List α
⊢ l₁✝.bagInter t ~ l₃✝.bagInter t

Tactic:
exact (ih_1 _).trans (ih_2 _)

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x y : α
l✝ t : List α
h : ¬x = y
xt : x ∉ t
yt : y ∉ t
⊢ (y :: x :: l✝).bagInter t ~ (x :: y :: l✝).bagInter t

Tactic:
simp [xt, yt]

Result:
no goals