no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
⊢ List.diff (List.erase l₂ a) (List.erase (b :: l₁) a) <+ List.diff l₂ (b :: l₁)
if heq : b = a then
  simp [heq]
else
  simp [heq, erase_comm a]
  exact (erase_cons_head b _ ▸ h.erase b).erase_diff_erase_sublist
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : b = a
⊢ List.diff (List.erase l₂ a) (List.erase (b :: l₁) a) <+ List.diff l₂ (b :: l₁)
simp [heq]
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ List.diff (List.erase (List.erase l₂ b) a) (List.erase l₁ a) <+ List.diff (List.erase l₂ b) l₁
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ List.diff (List.erase l₂ a) (List.erase (b :: l₁) a) <+ List.diff l₂ (b :: l₁)
simp [heq, erase_comm a]
no goals
α : Type u_1
inst✝ : DecidableEq α
a b : α
l₁ l₂ : List α
h : b :: l₁ <+ l₂
heq : ¬b = a
⊢ List.diff (List.erase (List.erase l₂ b) a) (List.erase l₁ a) <+ List.diff (List.erase l₂ b) l₁
exact (erase_cons_head b _ ▸ h.erase b).erase_diff_erase_sublist