-- Mathlib/Data/Bool/Count.lean
theorem two_mul_count_bool_eq_ite (hl : Chain' (· ≠ ·) l) (b : Bool) :
    2 * count b l =
      if Even (length l) then length l else
      if Option.some b == l.head? then length l + 1 else length l - 1

Proof state:
case neg.cons
b x : Bool
l : List Bool
h2 : Even l.length
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
⊢ (2 * count b l + 2 * if (x == b) = true then 1 else 0) =
    if (some b == some x) = true then (x :: l).length + 1 else (x :: l).length - 1

Tactic:
rw [hl.two_mul_count_bool_of_even h2]

Result:
case neg.cons
b x : Bool
l : List Bool
h2 : Even l.length
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
⊢ (l.length + 2 * if (x == b) = true then 1 else 0) =
    if (some b == some x) = true then (x :: l).length + 1 else (x :: l).length - 1

Proof state:
case neg
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
h2 : ¬Even l.length
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
rcases l with - | ⟨x, l⟩

Result:
case neg.nil
b : Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) []
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 x1 x2 => x1 ≠ x2) (x :: l)
h2 : ¬Even (x :: l).length
⊢ 2 * count b (x :: l) =
    if Even (x :: l).length then (x :: l).length
    else if (some b == (x :: l).head?) = true then (x :: l).length + 1 else (x :: l).length - 1

Proof state:
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : ¬Even (x :: l).length
⊢ (2 * count b l + 2 * if (x == b) = true then 1 else 0) =
    if (some b == some x) = true then (x :: l).length + 1 else (x :: l).length - 1

Tactic:
rw [length_cons, Nat.even_add_one, not_not] at h2

Result:
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : Even l.length
⊢ (2 * count b l + 2 * if (x == b) = true then 1 else 0) =
    if (some b == some x) = true then (x :: l).length + 1 else (x :: l).length - 1

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
by_cases h2 : Even (length l)

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

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

Proof state:
case neg.nil
b : Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) []
h2 : ¬Even [].length
⊢ 2 * count b [] =
    if Even [].length then [].length else if (some b == [].head?) = true then [].length + 1 else [].length - 1

Tactic:
exact (h2 .zero).elim

Result:
no goals

Proof state:
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : ¬Even (x :: l).length
⊢ 2 * count b (x :: l) =
    if Even (x :: l).length then (x :: l).length
    else if (some b == (x :: l).head?) = true then (x :: l).length + 1 else (x :: l).length - 1

Tactic:
simp only [if_neg h2, count_cons, mul_add, head?, Option.mem_some_iff, @eq_comm _ x]

Result:
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
h2 : ¬Even (x :: l).length
⊢ (2 * count b l + 2 * if (x == b) = true then 1 else 0) =
    if (some b == some x) = true then (x :: l).length + 1 else (x :: l).length - 1

Proof state:
case neg.cons
b x : Bool
l : List Bool
h2 : Even l.length
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
⊢ (l.length + 2 * if (x == b) = true then 1 else 0) =
    if (some b == some x) = true then (x :: l).length + 1 else (x :: l).length - 1

Tactic:
cases b <;> cases x <;> split_ifs <;> simp <;> contradiction

Result:
no goals

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

Tactic:
rw [if_pos h2, hl.two_mul_count_bool_of_even h2]

Result:
no goals