case nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
⊢ count (!b) [] ≤ count b [] + 1

case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count (!b) (x :: l) ≤ count b (x :: l) + 1
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ count (!b) l ≤ count b l + 1
cases' l with x l
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (b :: l)
⊢ count (!b) (b :: l) ≤ count b (b :: l) + 1

case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count (!!x) (x :: l) ≤ count (!x) (x :: l) + 1
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count (!b) (x :: l) ≤ count b (x :: l) + 1
obtain rfl | rfl : b = x ∨ b = !x := by simp only [Bool.eq_not_iff, em]
no goals
case nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
⊢ count (!b) [] ≤ count b [] + 1
exact zero_le _
no goals
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ b = x ∨ b = !x
simp only [Bool.eq_not_iff, em]
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (b :: l)
⊢ count b l + length l % 2 ≤ count b l + (1 + 1)
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (b :: l)
⊢ count (!b) (b :: l) ≤ count b (b :: l) + 1
rw [count_cons_of_ne b.not_ne_self, count_cons_self, hl.count_not, add_assoc]
no goals
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (b :: l)
⊢ count b l + length l % 2 ≤ count b l + (1 + 1)
exact add_le_add_left (Nat.mod_lt _ two_pos).le _
case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count x l + 1 ≤ count x l + length l % 2 + 1
case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count (!!x) (x :: l) ≤ count (!x) (x :: l) + 1
rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self, hl.count_not]
no goals
case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count x l + 1 ≤ count x l + length l % 2 + 1
exact add_le_add_right (le_add_right le_rfl) _