internlm/Lean-Github huggingface dataset:
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 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
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
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)
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
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
Proof 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
Theorem: List.sieve_mem_iff_true_unique
Proof 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
Proof 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
Theorem: List.sieve_mem_iff_true_unique
Proof 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
Proof 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
Theorem: List.sieve_mem_iff_true_unique
Proof 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'
Proof 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
Theorem: List.sieve_mem_iff_true_unique
Proof 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
Proof state after:
no goals
Theorem: List.sieve_mem_iff_true_unique
Proof 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
Proof state after:
no goals
Theorem: List.sieve_mem_iff_true_unique
Proof 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'
Proof state after:
no goals
Theorem: List.sieve_mem_iff_true_unique
Proof 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
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
α : Type u_1
β : Type u_2
⊢ ∀ {i : Nat} {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs) (f : α → β),
    Unique (map f xs) →
      (get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) ↔
        get bs { val := i, isLt := pf2 } = true)
Tactic:
intro i xs bs pf1 pf2 f hu
Proof state after:
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) ↔
    get bs { val := i, isLt := pf2 } = true
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) ↔
    get bs { val := i, isLt := pf2 } = true
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
    get bs { val := i, isLt := pf2 } = true

case mpr
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get bs { val := i, isLt := pf2 } = true →
    get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case mp
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
    get bs { val := i, isLt := pf2 } = true

case mpr
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get bs { val := i, isLt := pf2 } = true →
    get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
Tactic:
. intro hf
  induction i generalizing xs bs with
  | zero =>
    match bs, xs, hu with
    | b :: bs, x :: xs, .cons hnmem hu =>
    cases b with
    | true => simp only [get, sieve] at *
    | false =>
      simp only [get, sieve] at *
      exact mt mem_map_sieve_of_mem_map hnmem hf
  | succ i ih =>
    match bs, xs, hu with
    | b :: bs, x :: xs, .cons hnmem hu =>
    cases b with
    | true =>
      simp only [get, sieve, map] at *
      apply ih
      . exact hu
      . apply get_mem_cons_of_head_not_mem_getee hf hnmem
      . apply Nat.lt_of_succ_lt_succ pf1
    | false =>
      simp only [get, sieve, map] at *
      apply ih
      . exact hu
      . exact hf
      . apply Nat.lt_of_succ_lt_succ pf1
Proof state after:
case mpr
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get bs { val := i, isLt := pf2 } = true →
    get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case mpr
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get bs { val := i, isLt := pf2 } = true →
    get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
Tactic:
. intro hget
  induction i generalizing xs bs with
  | zero =>
    match bs, xs with
    | b :: bs, x :: xs =>
    cases b with
    | true => exact Mem.head _
    | false => simp only [get, map] at hget
  | succ i ih =>
    match bs, xs, hu with
    | b :: bs, x :: xs, .cons hnmem hu =>
    cases b with
    | true =>
      simp only [get, sieve, map] at *
      apply Mem.tail
      apply ih
      . apply Nat.lt_of_succ_lt_succ pf1
      . exact hu
      . exact hget
    | false =>
      simp only [get, map, sieve] at *
      apply ih
      . apply Nat.lt_of_succ_lt_succ pf1
      . exact hu
      . exact hget
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case mp
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
⊢ get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
    get bs { val := i, isLt := pf2 } = true
Tactic:
intro hf
Proof state after:
case mp
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
hf : get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
⊢ get bs { val := i, isLt := pf2 } = true
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case mp
α : Type u_1
β : Type u_2
i : Nat
xs : List α
bs : List Bool
pf1 : i < length xs
pf2 : i < length bs
f : α → β
hu : Unique (map f xs)
hf : get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
⊢ get bs { val := i, isLt := pf2 } = true
Tactic:
induction i generalizing xs bs with
| zero =>
  match bs, xs, hu with
  | b :: bs, x :: xs, .cons hnmem hu =>
  cases b with
  | true => simp only [get, sieve] at *
  | false =>
    simp only [get, sieve] at *
    exact mt mem_map_sieve_of_mem_map hnmem hf
| succ i ih =>
  match bs, xs, hu with
  | b :: bs, x :: xs, .cons hnmem hu =>
  cases b with
  | true =>
    simp only [get, sieve, map] at *
    apply ih
    . exact hu
    . apply get_mem_cons_of_head_not_mem_getee hf hnmem
    . apply Nat.lt_of_succ_lt_succ pf1
  | false =>
    simp only [get, sieve, map] at *
    apply ih
    . exact hu
    . exact hf
    . apply Nat.lt_of_succ_lt_succ pf1
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case mp.zero
α : Type u_1
β : Type u_2
f : α → β
xs : List α
bs : List Bool
pf1 : Nat.zero < length xs
pf2 : Nat.zero < length bs
hu : Unique (map f xs)
hf : get (map f xs) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f xs)) } ∈ map f (sieve bs xs)
⊢ get bs { val := Nat.zero, isLt := pf2 } = true
Tactic:
match bs, xs, hu with
| b :: bs, x :: xs, .cons hnmem hu =>
cases b with
| true => simp only [get, sieve] at *
| false =>
  simp only [get, sieve] at *
  exact mt mem_map_sieve_of_mem_map hnmem hf
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
b : Bool
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.zero < length (x :: xs)
pf2 : Nat.zero < length (b :: bs)
hf :
  get (map f (x :: xs)) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f (x :: xs))) } ∈
    map f (sieve (b :: bs) (x :: xs))
⊢ get (b :: bs) { val := Nat.zero, isLt := pf2 } = true
Tactic:
cases b with
| true => simp only [get, sieve] at *
| false =>
  simp only [get, sieve] at *
  exact mt mem_map_sieve_of_mem_map hnmem hf
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case true
α : Type u_1
β : Type u_2
f : α → β
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.zero < length (x :: xs)
pf2 : Nat.zero < length (true :: bs)
hf :
  get (map f (x :: xs)) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f (x :: xs))) } ∈
    map f (sieve (true :: bs) (x :: xs))
⊢ get (true :: bs) { val := Nat.zero, isLt := pf2 } = true
Tactic:
simp only [get, sieve] at *
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false
α : Type u_1
β : Type u_2
f : α → β
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.zero < length (x :: xs)
pf2 : Nat.zero < length (false :: bs)
hf :
  get (map f (x :: xs)) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f (x :: xs))) } ∈
    map f (sieve (false :: bs) (x :: xs))
⊢ get (false :: bs) { val := Nat.zero, isLt := pf2 } = true
Tactic:
simp only [get, sieve] at *
Proof state after:
case false
α : Type u_1
β : Type u_2
f : α → β
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.zero < length (x :: xs)
pf2 : Nat.zero < length (false :: bs)
hf : f x ∈ map f (sieve bs xs)
⊢ False
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false
α : Type u_1
β : Type u_2
f : α → β
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.zero < length (x :: xs)
pf2 : Nat.zero < length (false :: bs)
hf : f x ∈ map f (sieve bs xs)
⊢ False
Tactic:
exact mt mem_map_sieve_of_mem_map hnmem hf
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case mp.succ
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs : List α
bs : List Bool
pf1 : Nat.succ i < length xs
pf2 : Nat.succ i < length bs
hu : Unique (map f xs)
hf : get (map f xs) { val := Nat.succ i, isLt := (_ : Nat.succ i < length (map f xs)) } ∈ map f (sieve bs xs)
⊢ get bs { val := Nat.succ i, isLt := pf2 } = true
Tactic:
match bs, xs, hu with
| b :: bs, x :: xs, .cons hnmem hu =>
cases b with
| true =>
  simp only [get, sieve, map] at *
  apply ih
  . exact hu
  . apply get_mem_cons_of_head_not_mem_getee hf hnmem
  . apply Nat.lt_of_succ_lt_succ pf1
| false =>
  simp only [get, sieve, map] at *
  apply ih
  . exact hu
  . exact hf
  . apply Nat.lt_of_succ_lt_succ pf1
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
b : Bool
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (b :: bs)
hf :
  get (map f (x :: xs)) { val := Nat.succ i, isLt := (_ : Nat.succ i < length (map f (x :: xs))) } ∈
    map f (sieve (b :: bs) (x :: xs))
⊢ get (b :: bs) { val := Nat.succ i, isLt := pf2 } = true
Tactic:
cases b with
| true =>
  simp only [get, sieve, map] at *
  apply ih
  . exact hu
  . apply get_mem_cons_of_head_not_mem_getee hf hnmem
  . apply Nat.lt_of_succ_lt_succ pf1
| false =>
  simp only [get, sieve, map] at *
  apply ih
  . exact hu
  . exact hf
  . apply Nat.lt_of_succ_lt_succ pf1
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case true
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (true :: bs)
hf :
  get (map f (x :: xs)) { val := Nat.succ i, isLt := (_ : Nat.succ i < length (map f (x :: xs))) } ∈
    map f (sieve (true :: bs) (x :: xs))
⊢ get (true :: bs) { val := Nat.succ i, isLt := pf2 } = true
Tactic:
simp only [get, sieve, map] at *
Proof state after:
case true
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (true :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ f x :: map f (sieve bs xs)
⊢ get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case true.hf
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (true :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ f x :: map f (sieve bs xs)
⊢ get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)

case true.pf1
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (true :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ f x :: map f (sieve bs xs)
⊢ i < length xs
Tactic:
. apply get_mem_cons_of_head_not_mem_getee hf hnmem
Proof state after:
case true.pf1
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (true :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ f x :: map f (sieve bs xs)
⊢ i < length xs
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case true.pf1
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (true :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ f x :: map f (sieve bs xs)
⊢ i < length xs
Tactic:
. apply Nat.lt_of_succ_lt_succ pf1
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case true.hu
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs) →
        get bs { val := i, isLt := pf2 } = true
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (true :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ f x :: map f (sieve bs xs)
⊢ Unique (map f ?true.xs)
Tactic:
exact hu
Proof state after:
no goals