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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 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
Tactic:
apply ih
State after:
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)

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 ?true.xs) { val := i, isLt := (_ : i < length (map f ?true.xs)) } ∈ map f (sieve bs ?true.xs)

case true.xs
α : 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)
⊢ List α

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 ?true.xs

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)

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 ?true.xs) { val := i, isLt := (_ : i < length (map f ?true.xs)) } ∈ map f (sieve bs ?true.xs)

case true.xs
α : 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)
⊢ List α

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 ?true.xs
Tactic:
. exact hu
State after:
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

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

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

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

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

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

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

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 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
Tactic:
apply ih
State after:
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)

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 ?false.xs) { val := i, isLt := (_ : i < length (map f ?false.xs)) } ∈ map f (sieve bs ?false.xs)

case false.xs
α : 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)
⊢ List α

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 ?false.xs

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)

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 ?false.xs) { val := i, isLt := (_ : i < length (map f ?false.xs)) } ∈ map f (sieve bs ?false.xs)

case false.xs
α : 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)
⊢ List α

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 ?false.xs
Tactic:
. exact hu
State after:
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
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))
Tactic:
apply ih
State after:
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

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)

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

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

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)

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:
. apply Nat.lt_of_succ_lt_succ pf1
State after:
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)

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

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)

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 hu
State after:
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

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

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

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

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

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

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 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)
Tactic:
apply ih
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 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 xs

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 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
⊢ Unique (map f xs)

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

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

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 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
⊢ Unique (map f xs)

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:
. apply Nat.lt_of_succ_lt_succ pf1
State after:
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 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
⊢ Unique (map f xs)

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

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 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
⊢ Unique (map f xs)

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 hu
State after:
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

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

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 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 xs
Tactic:
apply Nat.lt_of_succ_lt_succ pf1
State after:
no goals

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 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
⊢ Unique (map f xs)
Tactic:
exact hu
State after:
no goals

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