-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem cons_diff (a : α) (l₁ l₂ : List α) :
    (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂

Proof state:
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

Tactic:
by_cases h : a = b

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : a = b
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : ¬a = b
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : ¬a = b
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

Tactic:
next =>
  have := Ne.symm h
  simp[*]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
⊢ (a :: l₁).diff [] = if a ∈ [] then l₁.diff ([].erase a) else a :: l₁.diff []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : a = b
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : ¬a = b
this : b ≠ a
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

Tactic:
simp[*]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : a = b
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : ¬a = b
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

Tactic:
next => simp [*]

Result:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : ¬a = b
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
⊢ (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂

Tactic:
induction l₂ generalizing l₁ with
| nil => rfl
| cons b l₂ ih =>
  by_cases h : a = b
  next => simp [*]
  next =>
    have := Ne.symm h
    simp[*]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : ¬a = b
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)

Tactic:
have := Ne.symm h

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l₂ : List α
ih : ∀ (l₁ : List α), (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
l₁ : List α
h : ¬a = b
this : b ≠ a
⊢ (a :: l₁).diff (b :: l₂) = if a ∈ b :: l₂ then l₁.diff ((b :: l₂).erase a) else a :: l₁.diff (b :: l₂)