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

Proof state:
case cons.isFalse.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : ¬x ∈ l₁
h✝ : x ∈ l₂
⊢ l₁.diff t <+~ (l₂.erase x).diff t

Tactic:
rw [← erase_of_not_mem hx1]

Result:
case cons.isFalse.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : ¬x ∈ l₁
h✝ : x ∈ l₂
⊢ (l₁.erase x).diff t <+~ (l₂.erase x).diff t

Proof state:
case cons.isFalse.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : ¬x ∈ l₁
h✝ : x ∈ l₂
⊢ (l₁.erase x).diff t <+~ (l₂.erase x).diff t

Tactic:
exact ih (h.erase _)

Result:
no goals

Proof state:
case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : x ∈ l₁
⊢ (l₁.erase x).diff t <+~ if x ∈ l₂ then (l₂.erase x).diff t else l₂.diff t

Tactic:
simp [h.subset hx1]

Result:
case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : x ∈ l₁
⊢ (l₁.erase x).diff t <+~ (l₂.erase x).diff t

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
⊢ (if x ∈ l₁ then (l₁.erase x).diff t else l₁.diff t) <+~ if x ∈ l₂ then (l₂.erase x).diff t else l₂.diff t

Tactic:
split <;> rename_i hx1

Result:
case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : x ∈ l₁
⊢ (l₁.erase x).diff t <+~ if x ∈ l₂ then (l₂.erase x).diff t else l₂.diff t

case cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : ¬x ∈ l₁
⊢ l₁.diff t <+~ if x ∈ l₂ then (l₂.erase x).diff t else l₂.diff t

Proof state:
case cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : ¬x ∈ l₁
⊢ l₁.diff t <+~ if x ∈ l₂ then (l₂.erase x).diff t else l₂.diff t

Tactic:
split

Result:
case cons.isFalse.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : ¬x ∈ l₁
h✝ : x ∈ l₂
⊢ l₁.diff t <+~ (l₂.erase x).diff t

case cons.isFalse.isFalse
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : ¬x ∈ l₁
h✝ : ¬x ∈ l₂
⊢ l₁.diff t <+~ l₂.diff t

Proof state:
case cons.isFalse.isFalse
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : ¬x ∈ l₁
h✝ : ¬x ∈ l₂
⊢ l₁.diff t <+~ l₂.diff t

Tactic:
exact ih h

Result:
no goals

Proof state:
case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
x : α
t : List α
ih : ∀ {l₁ l₂ : List α}, l₁ <+~ l₂ → l₁.diff t <+~ l₂.diff t
l₁ l₂ : List α
h : l₁ <+~ l₂
hx1 : x ∈ l₁
⊢ (l₁.erase x).diff t <+~ (l₂.erase x).diff t

Tactic:
exact ih (h.erase _)

Result:
no goals