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

State before:
α : Type u_1
b : Bool
bs : List Bool
h : length (b :: bs) = length []
⊢ length (sieve (b :: bs) []) = length (removeAllEq (b :: bs) [false])
Tactic:
cases h
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
h : length [] = length (x :: xs)
⊢ length (sieve [] (x :: xs)) = length (removeAllEq [] [false])
Tactic:
cases h
State after:
no goals

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (true :: bs) (x :: xs)) = length (removeAllEq (true :: bs) [false])
Tactic:
rw [removeAllEq_singleton_hd_neq]
State after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (true :: bs) (x :: xs)) = length (true :: removeAllEq bs [false])

case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (true :: bs) (x :: xs)) = length (true :: removeAllEq bs [false])

case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false
Tactic:
. simp only [length]
  apply congrArg (λ x => x + 1)
  exact ih
State after:
case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false

State before:
case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false
Tactic:
. apply Bool.noConfusion
State after:
no goals

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (true :: bs) (x :: xs)) = length (true :: removeAllEq bs [false])
Tactic:
simp only [length]
State after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) + 1 = length (removeAllEq bs [false]) + 1

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) + 1 = length (removeAllEq bs [false]) + 1
Tactic:
apply congrArg (λ x => x + 1)
State after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])
Tactic:
exact ih
State after:
no goals

State before:
case a
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (true :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ true ≠ false
Tactic:
apply Bool.noConfusion
State after:
no goals

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (false :: bs) (x :: xs)) = length (removeAllEq (false :: bs) [false])
Tactic:
rw [removeAllEq_singleton_hd_eq]
State after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (false :: bs) (x :: xs)) = length (removeAllEq bs [false])

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (false :: bs) (x :: xs)) = length (removeAllEq bs [false])
Tactic:
. simp only [length, sieve]
  exact ih
State after:
no goals

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve (false :: bs) (x :: xs)) = length (removeAllEq bs [false])
Tactic:
simp only [length, sieve]
State after:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])

State before:
α : Type u_1
bs : List Bool
x : α
xs : List α
h : length (false :: bs) = length (x :: xs)
ih : length (sieve bs xs) = length (removeAllEq bs [false])
⊢ length (sieve bs xs) = length (removeAllEq bs [false])
Tactic:
exact ih
State after:
no goals