internlm/Lean-Github huggingface dataset:
Theorem: List.length_counts_aux
Proof state before:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: map Prod.fst (incrCounts as x))) =
    length (uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
rw [map_fst_incrCounts_eq_cons_fst _ _ hout]
Proof state after:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: (map Prod.fst as ++ [x]))) = length (uniqueAux xs (x :: a.fst :: map Prod.fst as))
Theorem: List.length_counts_aux
Proof state before:
case cons.cons.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
this : ¬x ∈ a.fst :: map Prod.fst as
⊢ length (uniqueAux xs (a.fst :: (map Prod.fst as ++ [x]))) = length (uniqueAux xs (x :: a.fst :: map Prod.fst as))
Tactic:
apply List.length_uniqueAux_congr_append_cons_acc _ _ _ _ []
Proof state after:
no goals
Theorem: List.length_counts_aux
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
⊢ ¬x ∈ a.fst :: map Prod.fst as
Tactic:
intros hneg
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
hneg : x ∈ a.fst :: map Prod.fst as
⊢ False
Theorem: List.length_counts_aux
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
hneg : x ∈ a.fst :: map Prod.fst as
⊢ False
Tactic:
cases hneg
Proof state after:
case head
α : Type u_1
inst✝ : DecidableEq α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = a.fst
hout : ¬a.fst ∈ map Prod.fst as
⊢ False

case tail
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
a✝ : Mem x (map Prod.fst as)
⊢ False
Theorem: List.length_counts_aux
Proof state before:
case head
α : Type u_1
inst✝ : DecidableEq α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = a.fst
hout : ¬a.fst ∈ map Prod.fst as
⊢ False

case tail
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
a✝ : Mem x (map Prod.fst as)
⊢ False
Tactic:
repeat contradiction
Proof state after:
no goals
Theorem: List.length_counts_aux
Proof state before:
case tail
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
hout : ¬x ∈ map Prod.fst as
a✝ : Mem x (map Prod.fst as)
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.length_uniqueAux_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
Tactic:
induction xs with
| nil => simp [uniqueAux]
| cons x xs ih =>
  intros as
  cases Decidable.em (x ∈ as) with
  | inl h =>
    simp only [length, uniqueAux, h, ite_true]
    apply Nat.le_trans
    apply ih
    rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
    apply Nat.le_step
    simp
  | inr h =>
    simp only [length, uniqueAux, h, ite_false]
    apply Nat.le_trans
    apply ih
    simp only [length]
    rw [Nat.add_comm _ 1, Nat.add_assoc]
    apply Nat.le_refl
Proof state after:
no goals
Theorem: List.length_uniqueAux_le
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (as : List α), length (uniqueAux [] as) ≤ length [] + length as
Tactic:
simp [uniqueAux]
Proof state after:
no goals
Theorem: List.length_uniqueAux_le
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
⊢ ∀ (as : List α), length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Tactic:
intros as
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Theorem: List.length_uniqueAux_le
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Tactic:
cases Decidable.em (x ∈ as) with
| inl h =>
  simp only [length, uniqueAux, h, ite_true]
  apply Nat.le_trans
  apply ih
  rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
  apply Nat.le_step
  simp
| inr h =>
  simp only [length, uniqueAux, h, ite_false]
  apply Nat.le_trans
  apply ih
  simp only [length]
  rw [Nat.add_comm _ 1, Nat.add_assoc]
  apply Nat.le_refl
Proof state after:
no goals
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Tactic:
simp only [length, uniqueAux, h, ite_true]
Proof state after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ length xs + 1 + length as
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ length xs + 1 + length as
Tactic:
apply Nat.le_trans
Proof state after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ ?cons.inl.m

case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ ?cons.inl.m ≤ length xs + 1 + length as

case cons.inl.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ Nat
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ ?cons.inl.m

case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ ?cons.inl.m ≤ length xs + 1 + length as

case cons.inl.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ Nat
Tactic:
apply ih
Proof state after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + 1 + length as
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + 1 + length as
Tactic:
rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
Proof state after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + length as + 1
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + length as + 1
Tactic:
apply Nat.le_step
Proof state after:
case cons.inl.a.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + length as
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inl.a.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + length as
Tactic:
simp
Proof state after:
no goals
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Tactic:
simp only [length, uniqueAux, h, ite_false]
Proof state after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux xs (x :: as)) ≤ length xs + 1 + length as
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux xs (x :: as)) ≤ length xs + 1 + length as
Tactic:
apply Nat.le_trans
Proof state after:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux xs (x :: as)) ≤ ?cons.inr.m

case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ ?cons.inr.m ≤ length xs + 1 + length as

case cons.inr.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ Nat
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux xs (x :: as)) ≤ ?cons.inr.m

case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ ?cons.inr.m ≤ length xs + 1 + length as

case cons.inr.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ Nat
Tactic:
apply ih
Proof state after:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + length (x :: as) ≤ length xs + 1 + length as
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + length (x :: as) ≤ length xs + 1 + length as
Tactic:
simp only [length]
Proof state after:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (length as + 1) ≤ length xs + 1 + length as
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (length as + 1) ≤ length xs + 1 + length as
Tactic:
rw [Nat.add_comm _ 1, Nat.add_assoc]
Proof state after:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (1 + length as) ≤ length xs + (1 + length as)
Theorem: List.length_uniqueAux_le
Proof state before:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (1 + length as) ≤ length xs + (1 + length as)
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get (x :: xs) { val := Nat.succ n, isLt := pf1 } ∈ sieve (true :: bs) (x :: xs)
⊢ get (true :: bs) { val := Nat.succ n, isLt := pf2 } = true
Tactic:
simp only [get, sieve] at *
Proof state after:
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
Tactic:
apply Iff.mp
Proof state after:
case self
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ ?a ↔ get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ ?a

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Prop
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
case self
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ ?a ↔ get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ ?a

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Prop
Tactic:
apply sieve_mem_iff_true_unique
Proof state after:
case self.pf1
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ n < length ?self.xs

case self.hu
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Unique ?self.xs

case self.α
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Type u_1

case self.xs
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ List ?self.α

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get ?self.xs { val := n, isLt := ?self.pf1 } ∈ sieve bs ?self.xs
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
case self.pf1
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ n < length ?self.xs

case self.hu
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Unique ?self.xs

case self.α
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Type u_1

case self.xs
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ List ?self.α

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get ?self.xs { val := n, isLt := ?self.pf1 } ∈ sieve bs ?self.xs
Tactic:
. apply Nat.lt_of_succ_lt_succ pf1
Proof state after:
case self.hu
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Unique xs

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get xs { val := n, isLt := (_ : n < length xs) } ∈ sieve bs xs
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
case self.hu
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Unique xs

case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get xs { val := n, isLt := (_ : n < length xs) } ∈ sieve bs xs
Tactic:
. exact hu'
Proof state after:
case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get xs { val := n, isLt := (_ : n < length xs) } ∈ sieve bs xs
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get xs { val := n, isLt := (_ : n < length xs) } ∈ sieve bs xs
Tactic:
. exact List.get_mem_cons_of_head_not_mem_getee hf hnmem
Proof state after:
no goals
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
case self.pf1
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ n < length ?self.xs
Tactic:
apply Nat.lt_of_succ_lt_succ pf1
Proof state after:
no goals
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
case self.hu
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ Unique xs
Tactic:
exact hu'
Proof state after:
no goals
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
case a
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hf : get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
⊢ get xs { val := n, isLt := (_ : n < length xs) } ∈ sieve bs xs
Tactic:
exact List.get_mem_cons_of_head_not_mem_getee hf hnmem
Proof state after:
no goals
Theorem: List.sieve_mem_iff_true_unique
Proof state before:
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hb : get (true :: bs) { val := Nat.succ n, isLt := pf2 } = true
⊢ get (x :: xs) { val := Nat.succ n, isLt := pf1 } ∈ sieve (true :: bs) (x :: xs)
Tactic:
simp only [get, sieve] at *
Proof state after:
α : Type u_1
n : Nat
x : α
xs : List α
bs : List Bool
pf1 : Nat.succ n < length (x :: xs)
pf2 : Nat.succ n < length (true :: bs)
hnmem : ¬x ∈ xs
hu' : Unique xs
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs