internlm/Lean-Github huggingface dataset:
Theorem: List.mem_singleton_iff
Proof state before:
case mp
α : Type u_1
x y : α
⊢ x ∈ [y] → x = y
Tactic:
intro hmem
Proof state after:
case mp
α : Type u_1
x y : α
hmem : x ∈ [y]
⊢ x = y
Theorem: List.mem_singleton_iff
Proof state before:
case mp
α : Type u_1
x y : α
hmem : x ∈ [y]
⊢ x = y
Tactic:
cases hmem
Proof state after:
case mp.head
α : Type u_1
x : α
⊢ x = x

case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y
Theorem: List.mem_singleton_iff
Proof state before:
case mp.head
α : Type u_1
x : α
⊢ x = x

case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y
Tactic:
. rfl
Proof state after:
case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y
Theorem: List.mem_singleton_iff
Proof state before:
case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y
Tactic:
. contradiction
Proof state after:
no goals
Theorem: List.mem_singleton_iff
Proof state before:
case mp.head
α : Type u_1
x : α
⊢ x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: List.mem_singleton_iff
Proof state before:
case mp.tail
α : Type u_1
x y : α
a✝ : Mem x []
⊢ x = y
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_singleton_iff
Proof state before:
case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]
Tactic:
intro heq
Proof state after:
case mpr
α : Type u_1
x y : α
heq : x = y
⊢ x ∈ [y]
Theorem: List.mem_singleton_iff
Proof state before:
case mpr
α : Type u_1
x y : α
heq : x = y
⊢ x ∈ [y]
Tactic:
rw [heq]
Proof state after:
case mpr
α : Type u_1
x y : α
heq : x = y
⊢ y ∈ [y]
Theorem: List.mem_singleton_iff
Proof state before:
case mpr
α : Type u_1
x y : α
heq : x = y
⊢ y ∈ [y]
Tactic:
constructor
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_hd_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : α) (xs : List α), removeAllEq (x :: xs) [x] = removeAllEq xs [x]
Tactic:
intros x xs
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ removeAllEq (x :: xs) [x] = removeAllEq xs [x]
Theorem: List.removeAllEq_singleton_hd_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ removeAllEq (x :: xs) [x] = removeAllEq xs [x]
Tactic:
simp [removeAllEq, filter, notElem, elem]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (match !decide (x ∈ [x]) with
    | true => x :: filter (fun x_1 => !decide (x_1 ∈ [x])) xs
    | false => filter (fun x_1 => !decide (x_1 ∈ [x])) xs) =
    filter (fun x_1 => !decide (x_1 ∈ [x])) xs
Theorem: List.removeAllEq_singleton_hd_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (match !decide (x ∈ [x]) with
    | true => x :: filter (fun x_1 => !decide (x_1 ∈ [x])) xs
    | false => filter (fun x_1 => !decide (x_1 ∈ [x])) xs) =
    filter (fun x_1 => !decide (x_1 ∈ [x])) xs
Tactic:
have hmem : x ∈ [x] := by constructor
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
hmem : x ∈ [x]
⊢ (match !decide (x ∈ [x]) with
    | true => x :: filter (fun x_1 => !decide (x_1 ∈ [x])) xs
    | false => filter (fun x_1 => !decide (x_1 ∈ [x])) xs) =
    filter (fun x_1 => !decide (x_1 ∈ [x])) xs
Theorem: List.removeAllEq_singleton_hd_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
hmem : x ∈ [x]
⊢ (match !decide (x ∈ [x]) with
    | true => x :: filter (fun x_1 => !decide (x_1 ∈ [x])) xs
    | false => filter (fun x_1 => !decide (x_1 ∈ [x])) xs) =
    filter (fun x_1 => !decide (x_1 ∈ [x])) xs
Tactic:
simp only [hmem, decide_true, not]
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_hd_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ x ∈ [x]
Tactic:
constructor
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_hd_neq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x y : α) (xs : List α), x ≠ y → removeAllEq (x :: xs) [y] = x :: removeAllEq xs [y]
Tactic:
intro x y xs hneq
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
⊢ removeAllEq (x :: xs) [y] = x :: removeAllEq xs [y]
Theorem: List.removeAllEq_singleton_hd_neq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
⊢ removeAllEq (x :: xs) [y] = x :: removeAllEq xs [y]
Tactic:
simp only [removeAllEq, filter, notElem, elem, hneq, not]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Theorem: List.removeAllEq_singleton_hd_neq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Tactic:
cases Decidable.em (x ∈ [y]) with
| inl hmem =>
   rw [mem_singleton_iff] at hmem
   contradiction
| inr hnmem =>
   simp [hnmem, decide_true, not_false_eq_true]
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_hd_neq
Proof state before:
case inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hmem : x ∈ [y]
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Tactic:
rw [mem_singleton_iff] at hmem
Proof state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hmem : x = y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Theorem: List.removeAllEq_singleton_hd_neq
Proof state before:
case inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hmem : x = y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_hd_neq
Proof state before:
case inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hnmem : ¬x ∈ [y]
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
Tactic:
simp [hnmem, decide_true, not_false_eq_true]
Proof state after:
no goals
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
b : Bool
bs : List Bool
h : length (b :: bs) = length []
⊢ length (sieve (b :: bs) []) = length (removeAllEq (b :: bs) [false])
Tactic:
cases h
Proof state after:
no goals
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
x : α
xs : List α
h : length [] = length (x :: xs)
⊢ length (sieve [] (x :: xs)) = length (removeAllEq [] [false])
Tactic:
cases h
Proof state after:
no goals
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (true :: bs) (x :: xs)) = length (removeAllEq (true :: bs) [false])
Tactic:
rw [removeAllEq_singleton_hd_neq]
Proof state after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (true :: bs) (x :: xs)) = length (true :: removeAllEq bs [false])

case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (true :: bs) (x :: xs)) = length (true :: removeAllEq bs [false])

case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false
Tactic:
. simp only [length]
  apply congrArg (λ x => x + 1)
  exact ih
Proof state after:
case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false
Theorem: List.sieve_removeAllEq
Proof state before:
case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false
Tactic:
. apply Bool.noConfusion
Proof state after:
no goals
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (true :: bs) (x :: xs)) = length (true :: removeAllEq bs [false])
Tactic:
simp only [length]
Proof state after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) + 1 = length (removeAllEq bs [false]) + 1
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) + 1 = length (removeAllEq bs [false]) + 1
Tactic:
apply congrArg (λ x => x + 1)
Proof state after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.sieve_removeAllEq
Proof state before:
case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false
Tactic:
apply Bool.noConfusion
Proof state after:
no goals
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (false :: bs) (x :: xs)) = length (removeAllEq (false :: bs) [false])
Tactic:
rw [removeAllEq_singleton_hd_eq]
Proof state after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (false :: bs) (x :: xs)) = length (removeAllEq bs [false])
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (false :: bs) (x :: xs)) = length (removeAllEq bs [false])
Tactic:
. simp only [length, sieve]
  exact ih
Proof state after:
no goals
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (false :: bs) (x :: xs)) = length (removeAllEq bs [false])
Tactic:
simp only [length, sieve]
Proof state after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])
Theorem: List.sieve_removeAllEq
Proof state before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (xs : List α) (x : α), ¬x ∈ xs → removeAllEq xs [x] = xs
Tactic:
intro xs x hnmem
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x : α
hnmem : ¬x ∈ xs
⊢ removeAllEq xs [x] = xs
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x : α
hnmem : ¬x ∈ xs
⊢ removeAllEq xs [x] = xs
Tactic:
induction xs with
| nil => rfl
| cons x' xs ih =>
  rw [removeAllEq_singleton_hd_neq]
  congr
  apply ih
  intro hneg
  apply hnmem
  apply Mem.tail
  . exact hneg
  . intro hneg'
    rw [hneg'] at hnmem
    apply hnmem
    apply Mem.head
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
hnmem : ¬x ∈ []
⊢ removeAllEq [] [x] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ removeAllEq (x' :: xs) [x] = x' :: xs
Tactic:
rw [removeAllEq_singleton_hd_neq]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' :: removeAllEq xs [x] = x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' :: removeAllEq xs [x] = x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
congr
Proof state after:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ removeAllEq xs [x] = xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ removeAllEq xs [x] = xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
apply ih
Proof state after:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ ¬x ∈ xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ ¬x ∈ xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
intro hneg
Proof state after:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ False

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ False

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
apply hnmem
Proof state after:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ x ∈ x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ x ∈ x' :: xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
apply Mem.tail
Proof state after:
case cons.e_tail.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ Mem x xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.e_tail.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ Mem x xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
. exact hneg
Proof state after:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
. intro hneg'
  rw [hneg'] at hnmem
  apply hnmem
  apply Mem.head
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.e_tail.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg : x ∈ xs
⊢ Mem x xs
Tactic:
exact hneg
Proof state after:
no goals
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
Tactic:
intro hneg'
Proof state after:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg' : x' = x
⊢ False
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
hneg' : x' = x
⊢ False
Tactic:
rw [hneg'] at hnmem
Proof state after:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x :: xs
hneg' : x' = x
⊢ False
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x :: xs
hneg' : x' = x
⊢ False
Tactic:
apply hnmem
Proof state after:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x :: xs
hneg' : x' = x
⊢ x ∈ x :: xs
Theorem: List.removeAllEq_singleton_nonelem_eq
Proof state before:
case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x :: xs
hneg' : x' = x
⊢ x ∈ x :: xs
Tactic:
apply Mem.head
Proof state after:
no goals
Theorem: List.length_mergeWith
Proof state before:
α : Type u_1
cmp : α → α → Ordering
ys : List α
⊢ length (mergeWith cmp ([], ys)) = length [] + length ys
Tactic:
simp only [mergeWith, length, Nat.zero_add]
Proof state after:
no goals
Theorem: List.length_mergeWith
Proof state before:
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (mergeWith cmp (x :: xs, y :: ys)) = length (x :: xs) + length (y :: ys)
Tactic:
simp only [mergeWith]
Proof state after:
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length
      (match cmp x y with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)
Theorem: List.length_mergeWith
Proof state before:
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length
      (match cmp x y with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)
Tactic:
cases cmp x y with
| lt =>
  simp only
  have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
            length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
  have h₂ : length (x :: xs) = length xs + 1 := rfl
  rw [h₁, h₂, Nat.add_comm (length xs + 1), ←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  exact ih₁
| eq =>
  simp only
  have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
            length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
  have h₂ : length (x :: xs) = length xs + 1 := rfl
  rw [h₁, h₂, Nat.add_comm (length xs + 1), ←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  exact ih₁
| gt =>
  simp only [length]
  simp only [length] at ih₂
  rw [←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  rw [Nat.add_comm]
  exact ih₂
Proof state after:
no goals
Theorem: List.length_mergeWith
Proof state before:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length
      (match Ordering.lt with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)
Tactic:
simp only
Proof state after:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Theorem: List.length_mergeWith
Proof state before:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Tactic:
have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
          length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
Proof state after:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)