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

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