case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h2 : Even (length l)
⊢ 2 * count b l =
    if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1

case neg
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h2 : ¬Even (length l)
⊢ 2 * count b l =
    if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ 2 * count b l =
    if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
by_cases h2 : Even (length l)
no goals
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h2 : Even (length l)
⊢ 2 * count b l =
    if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
rw [if_pos h2, hl.two_mul_count_bool_of_even h2]
case neg.nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
h2 : ¬Even (length [])
⊢ 2 * count b [] =
    if Even (length []) then length [] else if (some b == head? []) = true then length [] + 1 else length [] - 1

case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : ¬Even (length (x :: l))
⊢ 2 * count b (x :: l) =
    if Even (length (x :: l)) then length (x :: l)
    else if (some b == head? (x :: l)) = true then length (x :: l) + 1 else length (x :: l) - 1
case neg
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h2 : ¬Even (length l)
⊢ 2 * count b l =
    if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
cases' l with x l
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : ¬Even (length (x :: l))
⊢ (2 * count b l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : ¬Even (length (x :: l))
⊢ 2 * count b (x :: l) =
    if Even (length (x :: l)) then length (x :: l)
    else if (some b == head? (x :: l)) = true then length (x :: l) + 1 else length (x :: l) - 1
simp only [if_neg h2, count_cons', mul_add, head?, Option.mem_some_iff, @eq_comm _ x]
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : Even (length l)
⊢ (2 * count b l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : ¬Even (length (x :: l))
⊢ (2 * count b l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
rw [length_cons, Nat.even_add_one, not_not] at h2
case neg.cons
b x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
case neg.cons
b x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (2 * count b l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
rw [hl.two_mul_count_bool_of_even h2]
no goals
case neg.cons
b x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
cases b <;> cases x <;> split_ifs <;> simp <;> contradiction
no goals
case neg.nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
h2 : ¬Even (length [])
⊢ 2 * count b [] =
    if Even (length []) then length [] else if (some b == head? []) = true then length [] + 1 else length [] - 1
exact (h2 even_zero).elim