Theorem: List.not_mem_erase_of_nodup (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
l : List α
hnodup : Nodup l
⊢ ¬a ∈ List.erase l a
Tactic:
induction l with
| nil => intro h; cases h
| cons b l IH =>
  dsimp [List.erase]
  have ⟨hhead, (htail : l.Nodup)⟩ := pairwise_cons.mp hnodup
  match hba : b == a with
  | true =>
    dsimp; cases of_decide_eq_true hba
    intro ha; exact hhead _ ha rfl
  | false =>
    dsimp; simp [not_or]
    apply And.intro
    . exact Ne.symm <| of_decide_eq_false hba
    . exact IH htail
State after:
no goals

State before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
⊢ ¬a ∈ List.erase [] a
Tactic:
intro h
State after:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
h : a ∈ List.erase [] a
⊢ False

State before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
h : a ∈ List.erase [] a
⊢ False
Tactic:
cases h
State after:
no goals

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
⊢ ¬a ∈ List.erase (b :: l) a
Tactic:
dsimp [List.erase]
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
⊢ ¬a ∈
      match b == a with
      | true => l
      | false => b :: List.erase l a

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
⊢ ¬a ∈
      match b == a with
      | true => l
      | false => b :: List.erase l a
Tactic:
have ⟨hhead, (htail : l.Nodup)⟩ := pairwise_cons.mp hnodup
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ ¬a ∈
      match b == a with
      | true => l
      | false => b :: List.erase l a

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ ¬a ∈
      match b == a with
      | true => l
      | false => b :: List.erase l a
Tactic:
match hba : b == a with
| true =>
  dsimp; cases of_decide_eq_true hba
  intro ha; exact hhead _ ha rfl
| false =>
  dsimp; simp [not_or]
  apply And.intro
  . exact Ne.symm <| of_decide_eq_false hba
  . exact IH htail
State after:
no goals

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = true
⊢ ¬a ∈
      match true with
      | true => l
      | false => b :: List.erase l a
Tactic:
dsimp
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = true
⊢ ¬a ∈ l

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = true
⊢ ¬a ∈ l
Tactic:
cases of_decide_eq_true hba
State after:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
htail : Nodup l
hnodup : Nodup (a :: l)
hhead : ∀ (a' : α), a' ∈ l → a ≠ a'
hba : (a == a) = true
⊢ ¬a ∈ l

State before:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
htail : Nodup l
hnodup : Nodup (a :: l)
hhead : ∀ (a' : α), a' ∈ l → a ≠ a'
hba : (a == a) = true
⊢ ¬a ∈ l
Tactic:
intro ha
State after:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
htail : Nodup l
hnodup : Nodup (a :: l)
hhead : ∀ (a' : α), a' ∈ l → a ≠ a'
hba : (a == a) = true
ha : a ∈ l
⊢ False

State before:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
htail : Nodup l
hnodup : Nodup (a :: l)
hhead : ∀ (a' : α), a' ∈ l → a ≠ a'
hba : (a == a) = true
ha : a ∈ l
⊢ False
Tactic:
exact hhead _ ha rfl
State after:
no goals

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a ∈
      match false with
      | true => l
      | false => b :: List.erase l a
Tactic:
dsimp
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a ∈ b :: List.erase l a

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a ∈ b :: List.erase l a
Tactic:
simp [not_or]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a = b ∧ ¬a ∈ List.erase l a

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a = b ∧ ¬a ∈ List.erase l a
Tactic:
apply And.intro
State after:
case left
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a = b

case right
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a ∈ List.erase l a

State before:
case left
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a = b

case right
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a ∈ List.erase l a
Tactic:
. exact Ne.symm <| of_decide_eq_false hba
State after:
case right
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a ∈ List.erase l a

State before:
case right
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a ∈ List.erase l a
Tactic:
. exact IH htail
State after:
no goals

State before:
case left
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a = b
Tactic:
exact Ne.symm <| of_decide_eq_false hba
State after:
no goals

State before:
case right
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → ¬a ∈ List.erase l a
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hba : (b == a) = false
⊢ ¬a ∈ List.erase l a
Tactic:
exact IH htail
State after:
no goals