case nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
h2 : Even (length [])
⊢ count (!b) [] = count b []

case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : Even (length (x :: l))
⊢ count (!b) (x :: l) = count b (x :: l)
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
h2 : Even (length l)
b : Bool
⊢ count (!b) l = count b l
cases' l with x l
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
⊢ count (!b) (x :: l) = count b (x :: l)
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : Even (length (x :: l))
⊢ count (!b) (x :: l) = count b (x :: l)
rw [length_cons, Nat.even_add_one, Nat.not_even_iff] at h2
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
⊢ count (!x) (x :: l) = count x (x :: l)
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
⊢ count (!b) (x :: l) = count b (x :: l)
suffices count (!x) (x :: l) = count x (x :: l) by
  cases b <;> cases x <;>
  revert this <;> simp only [Bool.not_false, Bool.not_true] <;> intro this <;>
  (try exact this) <;> exact this.symm
no goals
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
⊢ count (!x) (x :: l) = count x (x :: l)
rw [count_cons_of_ne x.not_ne_self, hl.count_not, h2, count_cons_self]
no goals
case nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
h2 : Even (length [])
⊢ count (!b) [] = count b []
rfl
no goals
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
this : count (!x) (x :: l) = count x (x :: l)
⊢ count (!b) (x :: l) = count b (x :: l)
cases b <;> cases x <;>
revert this <;> simp only [Bool.not_false, Bool.not_true] <;> intro this <;>
(try exact this) <;> exact this.symm
no goals
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count false (true :: l) = count true (true :: l)
try exact this
no goals
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count false (true :: l) = count true (true :: l)
exact this