-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Perm.diff_left (l : List α) {t₁ t₂ : List α} (h : t₁ ~ t₂) : l.diff t₁ = l.diff t₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x y : α
l✝ l : List α
h : ¬x = y
⊢ (if y ∈ l then if x ∈ l.erase y then ((l.erase y).erase x).diff l✝ else (l.erase y).diff l✝
    else if x ∈ l then (l.erase x).diff l✝ else l.diff l✝) =
    if x ∈ l then if y ∈ l.erase x then ((l.erase x).erase y).diff l✝ else (l.erase x).diff l✝
    else if y ∈ l then (l.erase y).diff l✝ else l.diff l✝

Tactic:
simp [mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm x y]

Result:
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x y : α
l✝ l : List α
h : ¬x = y
⊢ (if y ∈ l then if x ∈ l then ((l.erase y).erase x).diff l✝ else (l.erase y).diff l✝
    else if x ∈ l then (l.erase x).diff l✝ else l.diff l✝) =
    if x ∈ l then if y ∈ l then ((l.erase y).erase x).diff l✝ else (l.erase x).diff l✝
    else if y ∈ l then (l.erase y).diff l✝ else l.diff l✝

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

Tactic:
simp only [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l t₁ t₂ : List α
h : t₁ ~ t₂
⊢ l.diff t₁ = l.diff t₂

Tactic:
induction h generalizing l with try simp [List.diff]
| cons x _ ih => apply ite_congr rfl <;> (intro; apply ih)
| swap x y =>
  if h : x = y then
    simp [h]
  else
    simp [mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm x y]
    split <;> simp [h]
| trans => simp only [*]

Result:
no goals

Proof state:
case cons.h₃
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : ∀ (l : List α), l.diff l₁✝ = l.diff l₂✝
l : List α
⊢ ¬x ∈ l → l.diff l₁✝ = l.diff l₂✝

Tactic:
intro

Result:
case cons.h₃
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x : α
l₁✝ l₂✝ : List α
a✝¹ : l₁✝ ~ l₂✝
ih : ∀ (l : List α), l.diff l₁✝ = l.diff l₂✝
l : List α
a✝ : ¬x ∈ l
⊢ l.diff l₁✝ = l.diff l₂✝

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : ∀ (l : List α), l.diff l₁✝ = l.diff l₂✝
l : List α
⊢ (if x ∈ l then (l.erase x).diff l₁✝ else l.diff l₁✝) = if x ∈ l then (l.erase x).diff l₂✝ else l.diff l₂✝

Tactic:
apply ite_congr rfl <;> (intro; apply ih)

Result:
no goals

Proof state:
case cons.h₃
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x : α
l₁✝ l₂✝ : List α
a✝¹ : l₁✝ ~ l₂✝
ih : ∀ (l : List α), l.diff l₁✝ = l.diff l₂✝
l : List α
a✝ : ¬x ∈ l
⊢ l.diff l₁✝ = l.diff l₂✝

Tactic:
apply ih

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x y : α
l✝ l : List α
h : ¬x = y
⊢ (if y ∈ l then if x ∈ l then ((l.erase y).erase x).diff l✝ else (l.erase y).diff l✝
    else if x ∈ l then (l.erase x).diff l✝ else l.diff l✝) =
    if x ∈ l then if y ∈ l then ((l.erase y).erase x).diff l✝ else (l.erase x).diff l✝
    else if y ∈ l then (l.erase y).diff l✝ else l.diff l✝

Tactic:
split <;> simp [h]

Result:
no goals

Proof state:
case swap
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x y : α
l✝ l : List α
⊢ (if y ∈ l then if x ∈ l.erase y then ((l.erase y).erase x).diff l✝ else (l.erase y).diff l✝
    else if x ∈ l then (l.erase x).diff l✝ else l.diff l✝) =
    if x ∈ l then if y ∈ l.erase x then ((l.erase x).erase y).diff l✝ else (l.erase x).diff l✝
    else if y ∈ l then (l.erase y).diff l✝ else l.diff l✝

Tactic:
if h : x = y then
  simp [h]
else
  simp [mem_erase_of_ne h, mem_erase_of_ne (Ne.symm h), erase_comm x y]
  split <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
x y : α
l✝ l : List α
h : x = y
⊢ (if y ∈ l then if x ∈ l.erase y then ((l.erase y).erase x).diff l✝ else (l.erase y).diff l✝
    else if x ∈ l then (l.erase x).diff l✝ else l.diff l✝) =
    if x ∈ l then if y ∈ l.erase x then ((l.erase x).erase y).diff l✝ else (l.erase x).diff l✝
    else if y ∈ l then (l.erase y).diff l✝ else l.diff l✝

Tactic:
simp [h]

Result:
no goals

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

Tactic:
simp [List.diff]

Result:
no goals