[GOAL]
l : List Bool
b : Bool
⊢ count (!b) l + count b l = length l
[PROOFSTEP]
simp only [length_eq_countp_add_countp (· == !b), count, add_right_inj]
[GOAL]
l : List Bool
b : Bool
⊢ countp (fun x => x == b) l = countp (fun a => decide ¬(a == !b) = true) l
[PROOFSTEP]
suffices : (fun x => x == b) = (fun a => decide ¬(a == !b) = true)
[GOAL]
l : List Bool
b : Bool
this : (fun x => x == b) = fun a => decide ¬(a == !b) = true
⊢ countp (fun x => x == b) l = countp (fun a => decide ¬(a == !b) = true) l
case this l : List Bool b : Bool ⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
[PROOFSTEP]
rw [this]
[GOAL]
case this
l : List Bool
b : Bool
⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
[PROOFSTEP]
ext x
[GOAL]
case this.h
l : List Bool
b x : Bool
⊢ (x == b) = decide ¬(x == !b) = true
[PROOFSTEP]
cases x
[GOAL]
case this.h.false
l : List Bool
b : Bool
⊢ (false == b) = decide ¬(false == !b) = true
[PROOFSTEP]
cases b
[GOAL]
case this.h.true
l : List Bool
b : Bool
⊢ (true == b) = decide ¬(true == !b) = true
[PROOFSTEP]
cases b
[GOAL]
case this.h.false.false
l : List Bool
⊢ (false == false) = decide ¬(false == !false) = true
[PROOFSTEP]
rfl
[GOAL]
case this.h.false.true
l : List Bool
⊢ (false == true) = decide ¬(false == !true) = true
[PROOFSTEP]
rfl
[GOAL]
case this.h.true.false
l : List Bool
⊢ (true == false) = decide ¬(true == !false) = true
[PROOFSTEP]
rfl
[GOAL]
case this.h.true.true
l : List Bool
⊢ (true == true) = decide ¬(true == !true) = true
[PROOFSTEP]
rfl
[GOAL]
l : List Bool
b : Bool
⊢ count b l + count (!b) l = length l
[PROOFSTEP]
rw [add_comm, count_not_add_count]
[GOAL]
b x : Bool
l : List Bool
h : Chain (fun x x_1 => x ≠ x_1) b (x :: l)
⊢ count (!b) (x :: l) = count b (x :: l) + length (x :: l) % 2
[PROOFSTEP]
obtain rfl : b = !x := Bool.eq_not_iff.2 (rel_of_chain_cons h)
[GOAL]
x : Bool
l : List Bool
h : Chain (fun x x_1 => x ≠ x_1) (!x) (x :: l)
⊢ count (!!x) (x :: l) = count (!x) (x :: l) + length (x :: l) % 2
[PROOFSTEP]
rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self, Chain.count_not (chain_of_chain_cons h), length,
  add_assoc, Nat.mod_two_add_succ_mod_two]
[GOAL]
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
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
h2 : Even (length [])
⊢ count (!b) [] = count b []
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
rw [length_cons, Nat.even_add_one, Nat.not_even_iff] at h2 
[GOAL]
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)
[PROOFSTEP]
suffices count (!x) (x :: l) = count x (x :: l) by
  -- Porting note: old proof is
      -- cases b <;> cases x <;> try exact this;cases b <;> cases x <;> revert this <;>
          simp only [Bool.not_false, Bool.not_true] <;>
        intro this <;>
      (try exact this) <;>
    exact this.symm
[GOAL]
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)
[PROOFSTEP]
cases b
[GOAL]
case false
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 (!false) (x :: l) = count false (x :: l)
[PROOFSTEP]
cases x
[GOAL]
case true
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 (!true) (x :: l) = count true (x :: l)
[PROOFSTEP]
cases x
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count (!false) (false :: l) = count false (false :: l)
⊢ count (!false) (false :: l) = count false (false :: l)
[PROOFSTEP]
revert this
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count (!true) (true :: l) = count true (true :: l)
⊢ count (!false) (true :: l) = count false (true :: l)
[PROOFSTEP]
revert this
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count (!false) (false :: l) = count false (false :: l)
⊢ count (!true) (false :: l) = count true (false :: l)
[PROOFSTEP]
revert this
[GOAL]
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count (!true) (true :: l) = count true (true :: l)
⊢ count (!true) (true :: l) = count true (true :: l)
[PROOFSTEP]
revert this
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
⊢ count (!false) (false :: l) = count false (false :: l) → count (!false) (false :: l) = count false (false :: l)
[PROOFSTEP]
simp only [Bool.not_false, Bool.not_true]
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
⊢ count (!true) (true :: l) = count true (true :: l) → count (!false) (true :: l) = count false (true :: l)
[PROOFSTEP]
simp only [Bool.not_false, Bool.not_true]
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
⊢ count (!false) (false :: l) = count false (false :: l) → count (!true) (false :: l) = count true (false :: l)
[PROOFSTEP]
simp only [Bool.not_false, Bool.not_true]
[GOAL]
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
⊢ count (!true) (true :: l) = count true (true :: l) → count (!true) (true :: l) = count true (true :: l)
[PROOFSTEP]
simp only [Bool.not_false, Bool.not_true]
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
⊢ count true (false :: l) = count false (false :: l) → count true (false :: l) = count false (false :: l)
[PROOFSTEP]
intro this
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
⊢ count false (true :: l) = count true (true :: l) → count true (true :: l) = count false (true :: l)
[PROOFSTEP]
intro this
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
⊢ count true (false :: l) = count false (false :: l) → count false (false :: l) = count true (false :: l)
[PROOFSTEP]
intro this
[GOAL]
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
⊢ count false (true :: l) = count true (true :: l) → count false (true :: l) = count true (true :: l)
[PROOFSTEP]
intro this
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count true (false :: l) = count false (false :: l)
[PROOFSTEP]
try exact this
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count true (false :: l) = count false (false :: l)
[PROOFSTEP]
exact this
[GOAL]
case false.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 true (true :: l) = count false (true :: l)
[PROOFSTEP]
try exact this
[GOAL]
case false.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 true (true :: l) = count false (true :: l)
[PROOFSTEP]
exact this
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count false (false :: l) = count true (false :: l)
[PROOFSTEP]
try exact this
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count false (false :: l) = count true (false :: l)
[PROOFSTEP]
exact this
[GOAL]
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)
[PROOFSTEP]
try exact this
[GOAL]
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)
[PROOFSTEP]
exact this
[GOAL]
case false.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 true (true :: l) = count false (true :: l)
[PROOFSTEP]
exact this.symm
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count false (false :: l) = count true (false :: l)
[PROOFSTEP]
exact this.symm
[GOAL]
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)
[PROOFSTEP]
rw [count_cons_of_ne x.not_ne_self, hl.count_not, h2, count_cons_self]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ count (!b) l ≤ count b l + 1
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
⊢ count (!b) [] ≤ count b [] + 1
[PROOFSTEP]
exact zero_le _
[GOAL]
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
[PROOFSTEP]
obtain rfl | rfl : b = x ∨ b = !x := by simp only [Bool.eq_not_iff, em]
[GOAL]
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ b = x ∨ b = !x
[PROOFSTEP]
simp only [Bool.eq_not_iff, em]
[GOAL]
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
[PROOFSTEP]
rw [count_cons_of_ne b.not_ne_self, count_cons_self, hl.count_not, add_assoc]
[GOAL]
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)
[PROOFSTEP]
exact add_le_add_left (Nat.mod_lt _ two_pos).le _
[GOAL]
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
[PROOFSTEP]
rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self, hl.count_not]
[GOAL]
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
[PROOFSTEP]
exact add_le_add_right (le_add_right le_rfl) _
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
h2 : Even (length l)
b : Bool
⊢ 2 * count b l = length l
[PROOFSTEP]
rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]
[GOAL]
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
[PROOFSTEP]
by_cases h2 : Even (length l)
[GOAL]
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
[PROOFSTEP]
rw [if_pos h2, hl.two_mul_count_bool_of_even h2]
[GOAL]
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
[PROOFSTEP]
cases' l with x l
[GOAL]
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
[PROOFSTEP]
exact (h2 even_zero).elim
[GOAL]
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
[PROOFSTEP]
simp only [if_neg h2, count_cons', mul_add, head?, Option.mem_some_iff, @eq_comm _ x]
[GOAL]
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
[PROOFSTEP]
rw [length_cons, Nat.even_add_one, not_not] at h2 
[GOAL]
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
[PROOFSTEP]
replace hl : l.Chain' (· ≠ ·) := hl.tail
[GOAL]
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
[PROOFSTEP]
rw [hl.two_mul_count_bool_of_even h2]
[GOAL]
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
[PROOFSTEP]
cases b
[GOAL]
case neg.cons.false
x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if false = x then 1 else 0) =
    if (some false == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
cases x
[GOAL]
case neg.cons.true
x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if true = x then 1 else 0) =
    if (some true == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
cases x
[GOAL]
case neg.cons.false.false
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if false = false then 1 else 0) =
    if (some false == some false) = true then length (false :: l) + 1 else length (false :: l) - 1
[PROOFSTEP]
split_ifs
[GOAL]
case neg.cons.false.true
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if false = true then 1 else 0) =
    if (some false == some true) = true then length (true :: l) + 1 else length (true :: l) - 1
[PROOFSTEP]
split_ifs
[GOAL]
case neg.cons.true.false
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if true = false then 1 else 0) =
    if (some true == some false) = true then length (false :: l) + 1 else length (false :: l) - 1
[PROOFSTEP]
split_ifs
[GOAL]
case neg.cons.true.true
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if true = true then 1 else 0) =
    if (some true == some true) = true then length (true :: l) + 1 else length (true :: l) - 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : false = false
h✝ : (some false == some false) = true
⊢ length l + 2 * 1 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : false = false
h✝ : ¬(some false == some false) = true
⊢ length l + 2 * 1 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬false = false
h✝ : (some false == some false) = true
⊢ length l + 2 * 0 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬false = false
h✝ : ¬(some false == some false) = true
⊢ length l + 2 * 0 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : False
h✝ : (some false == some true) = true
⊢ length l + 2 * 1 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : False
h✝ : ¬(some false == some true) = true
⊢ length l + 2 * 1 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : ¬False
h✝ : (some false == some true) = true
⊢ length l + 2 * 0 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : ¬False
h✝ : ¬(some false == some true) = true
⊢ length l + 2 * 0 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : False
h✝ : (some false == some true) = true
⊢ length l + 2 * 1 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : False
h✝ : ¬(some false == some true) = true
⊢ length l + 2 * 1 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : ¬False
h✝ : (some false == some true) = true
⊢ length l + 2 * 0 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : ¬False
h✝ : ¬(some false == some true) = true
⊢ length l + 2 * 0 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : False
h✝ : (some true == some false) = true
⊢ length l + 2 * 1 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : False
h✝ : ¬(some true == some false) = true
⊢ length l + 2 * 1 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : ¬False
h✝ : (some true == some false) = true
⊢ length l + 2 * 0 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : ¬False
h✝ : ¬(some true == some false) = true
⊢ length l + 2 * 0 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : False
h✝ : (some true == some false) = true
⊢ length l + 2 * 1 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : False
h✝ : ¬(some true == some false) = true
⊢ length l + 2 * 1 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : ¬False
h✝ : (some true == some false) = true
⊢ length l + 2 * 0 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : ¬False
h✝ : ¬(some true == some false) = true
⊢ length l + 2 * 0 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : true = true
h✝ : (some true == some true) = true
⊢ length l + 2 * 1 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : true = true
h✝ : ¬(some true == some true) = true
⊢ length l + 2 * 1 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬true = true
h✝ : (some true == some true) = true
⊢ length l + 2 * 0 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬true = true
h✝ : ¬(some true == some true) = true
⊢ length l + 2 * 0 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : false = false
h✝ : ¬(some false == some false) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬false = false
h✝ : (some false == some false) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : False
h✝ : ¬(some false == some true) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : ¬False
h✝ : (some false == some true) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : False
h✝ : ¬(some false == some true) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : ¬False
h✝ : (some false == some true) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : False
h✝ : ¬(some true == some false) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : ¬False
h✝ : (some true == some false) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : False
h✝ : ¬(some true == some false) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : ¬False
h✝ : (some true == some false) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : true = true
h✝ : ¬(some true == some true) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬true = true
h✝ : (some true == some true) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - 1 ≤ 2 * count b l
[PROOFSTEP]
rw [hl.two_mul_count_bool_eq_ite]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - 1 ≤ if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝ : Even (length l)
⊢ length l - 1 ≤ length l
[PROOFSTEP]
simp [le_tsub_add, Nat.le_succ_of_le]
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝¹ : ¬Even (length l)
h✝ : (some b == head? l) = true
⊢ length l - 1 ≤ length l + 1
[PROOFSTEP]
simp [le_tsub_add, Nat.le_succ_of_le]
[GOAL]
case neg
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝¹ : ¬Even (length l)
h✝ : ¬(some b == head? l) = true
⊢ length l - 1 ≤ length l - 1
[PROOFSTEP]
simp [le_tsub_add, Nat.le_succ_of_le]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l / 2 ≤ count b l
[PROOFSTEP]
rw [Nat.div_le_iff_le_mul_add_pred two_pos, ← tsub_le_iff_right]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - (2 - 1) ≤ 2 * count b l
[PROOFSTEP]
exact length_sub_one_le_two_mul_count_bool hl b
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ 2 * count b l ≤ length l + 1
[PROOFSTEP]
rw [hl.two_mul_count_bool_eq_ite]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ (if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1) ≤
    length l + 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝ : Even (length l)
⊢ length l ≤ length l + 1
[PROOFSTEP]
simp [Nat.le_succ_of_le]
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝¹ : ¬Even (length l)
h✝ : (some b == head? l) = true
⊢ length l + 1 ≤ length l + 1
[PROOFSTEP]
simp [Nat.le_succ_of_le]
[GOAL]
case neg
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝¹ : ¬Even (length l)
h✝ : ¬(some b == head? l) = true
⊢ length l - 1 ≤ length l + 1
[PROOFSTEP]
simp [Nat.le_succ_of_le]
