Theorem: List.Nodup.erase (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
l : List α
hnodup : Nodup l
⊢ Nodup (List.erase l a)
Tactic:
induction l with
| nil => exact .nil
| cons b l IH =>
  have ⟨hhead, (htail : l.Nodup)⟩ := pairwise_cons.mp hnodup
  dsimp [List.erase]
  match b == a with
  | true => dsimp; exact htail
  | false =>
    dsimp; refine pairwise_cons.mpr <| And.intro ?_ ?_
    . intro _ hb h; cases h
      exact hhead b (List.mem_of_mem_erase hb) rfl
    . exact IH htail
State after:
no goals

State before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
⊢ Nodup (List.erase [] a)
Tactic:
exact .nil
State after:
no goals

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
⊢ Nodup (List.erase (b :: 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 → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup (List.erase (b :: l) a)

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup (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 → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup
    (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 → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup
    (match b == a with
    | true => l
    | false => b :: List.erase l a)
Tactic:
match b == a with
| true => dsimp; exact htail
| false =>
  dsimp; refine pairwise_cons.mpr <| And.intro ?_ ?_
  . intro _ hb h; cases h
    exact hhead b (List.mem_of_mem_erase hb) rfl
  . exact IH htail
State after:
no goals

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup
    (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 → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup l

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

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup
    (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 → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup (b :: List.erase l a)

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Nodup (b :: List.erase l a)
Tactic:
refine pairwise_cons.mpr <| And.intro ?_ ?_
State after:
case refine_1
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ ∀ (a' : α), a' ∈ List.erase l a → b ≠ a'

case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)

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

case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)
Tactic:
. intro _ hb h; cases h
  exact hhead b (List.mem_of_mem_erase hb) rfl
State after:
case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)

State before:
case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)
Tactic:
. exact IH htail
State after:
no goals

State before:
case refine_1
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ ∀ (a' : α), a' ∈ List.erase l a → b ≠ a'
Tactic:
intro _ hb h
State after:
case refine_1
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
a'✝ : α
hb : a'✝ ∈ List.erase l a
h : b = a'✝
⊢ False

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

State before:
case refine_1.refl
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
hb : b ∈ List.erase l a
⊢ False
Tactic:
exact hhead b (List.mem_of_mem_erase hb) rfl
State after:
no goals

State before:
case refine_2
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : α
l : List α
IH : Nodup l → Nodup (List.erase l a)
hnodup : Nodup (b :: l)
hhead : ∀ (a' : α), a' ∈ l → b ≠ a'
htail : Nodup l
⊢ Pairwise (fun x x_1 => x ≠ x_1) (List.erase l a)
Tactic:
exact IH htail
State after:
no goals