internlm/Lean-Github huggingface dataset:
Theorem: List.get_pmap
Proof state before:
case nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ [] → p a
i : Fin (length (pmap f [] h))
⊢ get (pmap f [] h) i =
    f (get [] (Fin.cast (_ : length (pmap f [] h) = length []) i))
      (_ : p (get [] (Fin.cast (_ : length (pmap f [] h) = length []) i)))
Tactic:
exact i.elim0
Proof state after:
no goals
Theorem: List.get_pmap
Proof state before:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
⊢ get (pmap f (a :: l) h) i =
    f (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) i))
      (_ : p (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) i)))
Tactic:
let ⟨i,hi⟩ := i
Proof state after:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i✝ : Fin (length (pmap f (a :: l) h))
i : Nat
hi : i < length (pmap f (a :: l) h)
⊢ get (pmap f (a :: l) h) { val := i, isLt := hi } =
    f (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) { val := i, isLt := hi }))
      (_ : p (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) { val := i, isLt := hi })))
Theorem: List.get_pmap
Proof state before:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i✝ : Fin (length (pmap f (a :: l) h))
i : Nat
hi : i < length (pmap f (a :: l) h)
⊢ get (pmap f (a :: l) h) { val := i, isLt := hi } =
    f (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) { val := i, isLt := hi }))
      (_ : p (get (a :: l) (Fin.cast (_ : length (pmap f (a :: l) h) = length (a :: l)) { val := i, isLt := hi })))
Tactic:
cases i <;> dsimp
Proof state after:
case cons.zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
hi : Nat.zero < length (pmap f (a :: l) h)
⊢ f a (_ : p a) = f a (_ : p a)

case cons.succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
n✝ : Nat
hi : Nat.succ n✝ < length (pmap f (a :: l) h)
⊢ get (pmap f l (_ : ∀ (x : α), x ∈ l → p x))
      { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) } =
    f (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) })
      (_ : p (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }))
Theorem: List.get_pmap
Proof state before:
case cons.zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
hi : Nat.zero < length (pmap f (a :: l) h)
⊢ f a (_ : p a) = f a (_ : p a)

case cons.succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
n✝ : Nat
hi : Nat.succ n✝ < length (pmap f (a :: l) h)
⊢ get (pmap f l (_ : ∀ (x : α), x ∈ l → p x))
      { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) } =
    f (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) })
      (_ : p (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }))
Tactic:
rfl
Proof state after:
case cons.succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
n✝ : Nat
hi : Nat.succ n✝ < length (pmap f (a :: l) h)
⊢ get (pmap f l (_ : ∀ (x : α), x ∈ l → p x))
      { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) } =
    f (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) })
      (_ : p (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }))
Theorem: List.get_pmap
Proof state before:
case cons.succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH :
  ∀ (h : ∀ (a : α), a ∈ l → p a) (i : Fin (length (pmap f l h))),
    get (pmap f l h) i =
      f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
        (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
i : Fin (length (pmap f (a :: l) h))
n✝ : Nat
hi : Nat.succ n✝ < length (pmap f (a :: l) h)
⊢ get (pmap f l (_ : ∀ (x : α), x ∈ l → p x))
      { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) } =
    f (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) })
      (_ : p (get l { val := n✝, isLt := (_ : Nat.succ n✝ ≤ length l) }))
Tactic:
exact IH _ _
Proof state after:
no goals
Theorem: List.mem_pmap
Proof state before:
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
l : List α
hp : ∀ (a : α), a ∈ l → p a
⊢ b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
Tactic:
induction l with
| nil => simp
| cons a l IH =>
  dsimp [pmap]
  simp only [mem_cons, exists_and_left, exists_eq_or_imp, IH]
  apply or_congr_left
  constructor
  . intro h; exact .intro _ h
  . intro h; cases h; assumption
Proof state after:
no goals
Theorem: List.mem_pmap
Proof state before:
case nil
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
hp : ∀ (a : α), a ∈ [] → p a
⊢ b ∈ pmap f [] hp ↔ ∃ a h, a ∈ [] ∧ b = f a h
Tactic:
simp
Proof state after:
no goals
Theorem: List.mem_pmap
Proof state before:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b ∈ pmap f (a :: l) hp ↔ ∃ a_1 h, a_1 ∈ a :: l ∧ b = f a_1 h
Tactic:
dsimp [pmap]
Proof state after:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b ∈ f a (_ : p a) :: pmap f l (_ : ∀ (x : α), x ∈ l → p x) ↔ ∃ a_1 h, a_1 ∈ a :: l ∧ b = f a_1 h
Theorem: List.mem_pmap
Proof state before:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b ∈ f a (_ : p a) :: pmap f l (_ : ∀ (x : α), x ∈ l → p x) ↔ ∃ a_1 h, a_1 ∈ a :: l ∧ b = f a_1 h
Tactic:
simp only [mem_cons, exists_and_left, exists_eq_or_imp, IH]
Proof state after:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (b = f a (_ : p a) ∨ ∃ a, a ∈ l ∧ ∃ x, b = f a x) ↔ (∃ x, b = f a x) ∨ ∃ a, a ∈ l ∧ ∃ x, b = f a x
Theorem: List.mem_pmap
Proof state before:
case cons
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (b = f a (_ : p a) ∨ ∃ a, a ∈ l ∧ ∃ x, b = f a x) ↔ (∃ x, b = f a x) ∨ ∃ a, a ∈ l ∧ ∃ x, b = f a x
Tactic:
apply or_congr_left
Proof state after:
case cons.h
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) ↔ ∃ x, b = f a x
Theorem: List.mem_pmap
Proof state before:
case cons.h
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) ↔ ∃ x, b = f a x
Tactic:
constructor
Proof state after:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) → ∃ x, b = f a x

case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)
Theorem: List.mem_pmap
Proof state before:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) → ∃ x, b = f a x

case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)
Tactic:
. intro h; exact .intro _ h
Proof state after:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)
Theorem: List.mem_pmap
Proof state before:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)
Tactic:
. intro h; cases h; assumption
Proof state after:
no goals
Theorem: List.mem_pmap
Proof state before:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ b = f a (_ : p a) → ∃ x, b = f a x
Tactic:
intro h
Proof state after:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
h : b = f a (_ : p a)
⊢ ∃ x, b = f a x
Theorem: List.mem_pmap
Proof state before:
case cons.h.mp
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
h : b = f a (_ : p a)
⊢ ∃ x, b = f a x
Tactic:
exact .intro _ h
Proof state after:
no goals
Theorem: List.mem_pmap
Proof state before:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ (∃ x, b = f a x) → b = f a (_ : p a)
Tactic:
intro h
Proof state after:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
h : ∃ x, b = f a x
⊢ b = f a (_ : p a)
Theorem: List.mem_pmap
Proof state before:
case cons.h.mpr
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
h : ∃ x, b = f a x
⊢ b = f a (_ : p a)
Tactic:
cases h
Proof state after:
case cons.h.mpr.intro
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
w✝ : p a
h✝ : b = f a w✝
⊢ b = f a (_ : p a)
Theorem: List.mem_pmap
Proof state before:
case cons.h.mpr.intro
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ {hp : ∀ (a : α), a ∈ l → p a}, b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
hp : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
w✝ : p a
h✝ : b = f a w✝
⊢ b = f a (_ : p a)
Tactic:
assumption
Proof state after:
no goals
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof state after:
no goals
Theorem: List.not_mem_erase_of_nodup
Proof state before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
⊢ ¬a ∈ List.erase [] a
Tactic:
intro h
Proof state after:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
h : a ∈ List.erase [] a
⊢ False
Theorem: List.not_mem_erase_of_nodup
Proof state before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
h : a ∈ List.erase [] a
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: List.not_mem_erase_of_nodup
Proof 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]
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof state after:
no goals
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof state after:
no goals
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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]
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof 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
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof state after:
no goals
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof state after:
no goals
Theorem: List.not_mem_erase_of_nodup
Proof 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
Proof state after:
no goals
Theorem: List.Nodup.erase
Proof 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
Proof state after:
no goals
Theorem: List.Nodup.erase
Proof state before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
a : α
hnodup : Nodup []
⊢ Nodup (List.erase [] a)
Tactic:
exact .nil
Proof state after:
no goals
Theorem: List.Nodup.erase
Proof 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
Proof 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)
Theorem: List.Nodup.erase
Proof 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]
Proof 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)