internlm/Lean-Github huggingface dataset:
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)
Tactic:
apply get_mem_cons_of_head_not_mem_getee hf hnmem
Proof state after:
no goals
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 false
α : 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 (false :: bs)
hf :
  get (map f (x :: xs)) { val := Nat.succ i, isLt := (_ : Nat.succ i < length (map f (x :: xs))) } ∈
    map f (sieve (false :: bs) (x :: xs))
⊢ get (false :: bs) { val := Nat.succ i, isLt := pf2 } = true
Tactic:
simp only [get, sieve, map] at *
Proof state after:
case false
α : 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 (false :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ 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 false.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 (false :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ map f (sieve bs xs)
⊢ get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)

case false.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 (false :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ map f (sieve bs xs)
⊢ i < length xs
Tactic:
. exact hf
Proof state after:
case false.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 (false :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ map f (sieve bs xs)
⊢ i < length xs
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false.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 (false :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ 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 false.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 (false :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ map f (sieve bs xs)
⊢ Unique (map f ?false.xs)
Tactic:
exact hu
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false.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 (false :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ map f (sieve bs xs)
⊢ get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
Tactic:
exact hf
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false.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 (false :: bs)
hf : get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ 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 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
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)
hget : 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)
hget : 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:
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 mpr.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)
hget : get bs { val := Nat.zero, isLt := pf2 } = true
⊢ get (map f xs) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f xs)) } ∈ map f (sieve bs xs)
Tactic:
match bs, xs with
| b :: bs, x :: xs =>
cases b with
| true => exact Mem.head _
| false => simp only [get, map] at hget
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
b : Bool
bs : List Bool
x : α
xs : List α
pf1 : Nat.zero < length (x :: xs)
pf2 : Nat.zero < length (b :: bs)
hu : Unique (map f (x :: xs))
hget : get (b :: bs) { val := Nat.zero, isLt := pf2 } = true
⊢ get (map f (x :: xs)) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f (x :: xs))) } ∈
    map f (sieve (b :: bs) (x :: xs))
Tactic:
cases b with
| true => exact Mem.head _
| false => simp only [get, map] at hget
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✝ bs : List Bool
x : α
xs : List α
pf1 : Nat.zero < length (x :: xs)
hu : Unique (map f (x :: xs))
pf2 : Nat.zero < length (true :: bs)
hget : get (true :: bs) { val := Nat.zero, isLt := pf2 } = true
⊢ get (map f (x :: xs)) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f (x :: xs))) } ∈
    map f (sieve (true :: bs) (x :: xs))
Tactic:
exact Mem.head _
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✝ bs : List Bool
x : α
xs : List α
pf1 : Nat.zero < length (x :: xs)
hu : Unique (map f (x :: xs))
pf2 : Nat.zero < length (false :: bs)
hget : get (false :: bs) { val := Nat.zero, isLt := pf2 } = true
⊢ get (map f (x :: xs)) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f (x :: xs))) } ∈
    map f (sieve (false :: bs) (x :: xs))
Tactic:
simp only [get, map] at hget
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case mpr.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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
xs : List α
bs : List Bool
pf1 : Nat.succ i < length xs
pf2 : Nat.succ i < length bs
hu : Unique (map f xs)
hget : get bs { val := Nat.succ i, isLt := pf2 } = true
⊢ get (map f xs) { val := Nat.succ i, isLt := (_ : Nat.succ i < length (map f xs)) } ∈ map f (sieve bs xs)
Tactic:
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:
α : 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get (b :: bs) { val := Nat.succ i, isLt := pf2 } = true
⊢ 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))
Tactic:
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 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get (true :: bs) { val := Nat.succ i, isLt := pf2 } = true
⊢ 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))
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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ f x :: map f (sieve bs xs)
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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ f x :: map f (sieve bs xs)
Tactic:
apply Mem.tail
Proof state after:
case true.a
α : 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ Mem (get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) }) (map f (sieve bs xs))
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case true.a.hget
α : 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ get bs { val := i, isLt := ?true.a.pf2 } = true

case true.a.pf2
α : 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ i < length bs
Tactic:
. exact hget
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case true.a.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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ 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.a.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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ Unique (map f xs)
Tactic:
exact hu
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case true.a.hget
α : 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ get bs { val := i, isLt := ?true.a.pf2 } = true
Tactic:
exact hget
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 : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    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)
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 (false :: bs)
hget : get (false :: bs) { val := Nat.succ i, isLt := pf2 } = true
⊢ get (map f (x :: xs)) { val := Nat.succ i, isLt := (_ : Nat.succ i < length (map f (x :: xs))) } ∈
    map f (sieve (false :: bs) (x :: xs))
Tactic:
simp only [get, map, sieve] at *
Proof state after:
case false
α : 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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 (false :: bs)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ get (map f xs) { val := i, isLt := (_ : Nat.succ i ≤ length (map f xs)) } ∈ map f (sieve bs xs)
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false.hget
α : 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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 (false :: bs)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ get bs { val := i, isLt := ?false.pf2 } = true

case false.pf2
α : 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 bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
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 (false :: bs)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ i < length bs
Tactic:
. exact hget
Proof state after:
no goals