Theorem: List.sieve_mem_iff_true_unique (Table/BuiltinExtensions.lean)

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 *
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

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
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

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
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

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
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

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'
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

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
State after:
no goals

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
State after:
no goals

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'
State after:
no goals

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
State after:
no goals

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 *
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

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 bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) } ∈ x :: sieve bs xs
Tactic:
apply Mem.tail
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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Mem (get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) }) (sieve bs xs)

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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Mem (get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) }) (sieve bs xs)
Tactic:
apply Iff.mpr
State after:
case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Mem (get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) }) (sieve bs xs) ↔ ?a.b✝

case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ ?a.b✝

case a.b
α : 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
⊢ Prop

State before:
case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Mem (get xs { val := n, isLt := (_ : Nat.succ n ≤ length xs) }) (sieve bs xs) ↔ ?a.b✝

case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ ?a.b✝

case a.b
α : 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
⊢ Prop
Tactic:
apply sieve_mem_iff_true_unique
State after:
case a.self.pf2
α : 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
⊢ n < length bs

case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Unique xs

case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get bs { val := n, isLt := ?a.self.pf2✝ } = true

State before:
case a.self.pf2
α : 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
⊢ n < length bs

case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Unique xs

case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get bs { val := n, isLt := ?a.self.pf2✝ } = true
Tactic:
. apply Nat.lt_of_succ_lt_succ pf2
State after:
case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Unique xs

case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get bs { val := n, isLt := (_ : n < length bs) } = true

State before:
case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Unique xs

case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get bs { val := n, isLt := (_ : n < length bs) } = true
Tactic:
. exact hu'
State after:
case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get bs { val := n, isLt := (_ : n < length bs) } = true

State before:
case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get bs { val := n, isLt := (_ : n < length bs) } = true
Tactic:
. exact hb
State after:
no goals

State before:
case a.self.pf2
α : 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
⊢ n < length bs
Tactic:
apply Nat.lt_of_succ_lt_succ pf2
State after:
no goals

State before:
case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ Unique xs
Tactic:
exact hu'
State after:
no goals

State before:
case a.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
hb : get bs { val := n, isLt := (_ : Nat.succ n ≤ length bs) } = true
⊢ get bs { val := n, isLt := (_ : n < length bs) } = true
Tactic:
exact hb
State after:
no goals