[GOAL]
n : ℕ
⊢ bodd (succ n) = !bodd n
[PROOFSTEP]
simp only [bodd, boddDiv2]
[GOAL]
n : ℕ
⊢ (match boddDiv2 n with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(boddDiv2 n).fst
[PROOFSTEP]
let ⟨b, m⟩ := boddDiv2 n
[GOAL]
n : ℕ
b : Bool
m : ℕ
⊢ (match (b, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(b, m).fst
[PROOFSTEP]
cases b
[GOAL]
case false
n m : ℕ
⊢ (match (false, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(false, m).fst
[PROOFSTEP]
rfl
[GOAL]
case true
n m : ℕ
⊢ (match (true, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(true, m).fst
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ bodd (m + n) = bxor (bodd m) (bodd n)
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
m : ℕ
⊢ bodd (m + zero) = bxor (bodd m) (bodd zero)
[PROOFSTEP]
simp
[GOAL]
case succ
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ bodd (m + succ n) = bxor (bodd m) (bodd (succ n))
[PROOFSTEP]
simp [add_succ, IH]
[GOAL]
case succ
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor (bodd m) (bodd n)) = bxor (bodd m) !bodd n
[PROOFSTEP]
cases bodd m
[GOAL]
case succ.false
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor false (bodd n)) = bxor false !bodd n
[PROOFSTEP]
cases bodd n
[GOAL]
case succ.true
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor true (bodd n)) = bxor true !bodd n
[PROOFSTEP]
cases bodd n
[GOAL]
case succ.false.false
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor false false) = bxor false !false
[PROOFSTEP]
rfl
[GOAL]
case succ.false.true
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor false true) = bxor false !true
[PROOFSTEP]
rfl
[GOAL]
case succ.true.false
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor true false) = bxor true !false
[PROOFSTEP]
rfl
[GOAL]
case succ.true.true
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor true true) = bxor true !true
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ bodd (m * n) = (bodd m && bodd n)
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
m : ℕ
⊢ bodd (m * zero) = (bodd m && bodd zero)
[PROOFSTEP]
simp
[GOAL]
case succ
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bodd (m * succ n) = (bodd m && bodd (succ n))
[PROOFSTEP]
simp [mul_succ, IH]
[GOAL]
case succ
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (bodd m && bodd n) (bodd m) = (bodd m && !bodd n)
[PROOFSTEP]
cases bodd m
[GOAL]
case succ.false
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (false && bodd n) false = (false && !bodd n)
[PROOFSTEP]
cases bodd n
[GOAL]
case succ.true
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (true && bodd n) true = (true && !bodd n)
[PROOFSTEP]
cases bodd n
[GOAL]
case succ.false.false
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (false && false) false = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case succ.false.true
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (false && true) false = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case succ.true.false
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (true && false) true = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case succ.true.true
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (true && true) true = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
have := congr_arg bodd (mod_add_div n 2)
[GOAL]
n : ℕ
this : bodd (n % 2 + 2 * (n / 2)) = bodd n
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
simp [not] at this 
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
have _ : ∀ b, and false b = false := by
  intro b
  cases b <;> rfl
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
⊢ ∀ (b : Bool), (false && b) = false
[PROOFSTEP]
intro b
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
b : Bool
⊢ (false && b) = false
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
this : bodd (n % 2) = bodd n
⊢ (false && false) = false
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
this : bodd (n % 2) = bodd n
⊢ (false && true) = false
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
have _ : ∀ b, bxor b false = b := by
  intro b
  cases b <;> rfl
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ ∀ (b : Bool), bxor b false = b
[PROOFSTEP]
intro b
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
b : Bool
⊢ bxor b false = b
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ bxor false false = false
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ bxor true false = true
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
rw [← this]
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
⊢ n % 2 = bif bodd (n % 2) then 1 else 0
[PROOFSTEP]
cases' mod_two_eq_zero_or_one n with h h
[GOAL]
case inl
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
h : n % 2 = 0
⊢ n % 2 = bif bodd (n % 2) then 1 else 0
[PROOFSTEP]
rw [h]
[GOAL]
case inr
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
h : n % 2 = 1
⊢ n % 2 = bif bodd (n % 2) then 1 else 0
[PROOFSTEP]
rw [h]
[GOAL]
case inl
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
h : n % 2 = 0
⊢ 0 = bif bodd 0 then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
case inr
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
h : n % 2 = 1
⊢ 1 = bif bodd 1 then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ div2 (succ n) = bif bodd n then succ (div2 n) else div2 n
[PROOFSTEP]
simp only [bodd, boddDiv2, div2]
[GOAL]
n : ℕ
⊢ (match boddDiv2 n with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (boddDiv2 n).fst then succ (boddDiv2 n).snd else (boddDiv2 n).snd
[PROOFSTEP]
cases' boddDiv2 n with fst snd
[GOAL]
case mk
n : ℕ
fst : Bool
snd : ℕ
⊢ (match (fst, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (fst, snd).fst then succ (fst, snd).snd else (fst, snd).snd
[PROOFSTEP]
cases fst
[GOAL]
case mk.false
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd
case mk.true
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
[PROOFSTEP]
case mk.false => simp
[GOAL]
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd
[PROOFSTEP]
case mk.false => simp
[GOAL]
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd
[PROOFSTEP]
simp
[GOAL]
case mk.true
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
[PROOFSTEP]
case mk.true => simp
[GOAL]
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
[PROOFSTEP]
case mk.true => simp
[GOAL]
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ (bif bodd (succ n) then 1 else 0) + 2 * div2 (succ n) = succ n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ (bif bodd n then 0 else 1) + (bif bodd n then succ (div2 n) else div2 n) * 2 = succ n
[PROOFSTEP]
refine' Eq.trans _ (congr_arg succ (bodd_add_div2 n))
[GOAL]
n : ℕ
⊢ (bif bodd n then 0 else 1) + (bif bodd n then succ (div2 n) else div2 n) * 2 =
    succ ((bif bodd n then 1 else 0) + 2 * div2 n)
[PROOFSTEP]
cases bodd n
[GOAL]
case false
n : ℕ
⊢ (bif false then 0 else 1) + (bif false then succ (div2 n) else div2 n) * 2 =
    succ ((bif false then 1 else 0) + 2 * div2 n)
[PROOFSTEP]
simp [cond, not]
[GOAL]
case true
n : ℕ
⊢ (bif true then 0 else 1) + (bif true then succ (div2 n) else div2 n) * 2 =
    succ ((bif true then 1 else 0) + 2 * div2 n)
[PROOFSTEP]
simp [cond, not]
[GOAL]
case false
n : ℕ
⊢ 1 + div2 n * 2 = succ (div2 n * 2)
[PROOFSTEP]
rw [Nat.add_comm, Nat.add_succ]
[GOAL]
case true
n : ℕ
⊢ succ (div2 n) * 2 = succ (1 + div2 n * 2)
[PROOFSTEP]
rw [succ_mul, Nat.add_comm 1, Nat.add_succ]
[GOAL]
n : ℕ
⊢ div2 n = n / 2
[PROOFSTEP]
refine' Nat.eq_of_mul_eq_mul_left (by decide) (Nat.add_left_cancel (Eq.trans _ (Nat.mod_add_div n 2).symm))
[GOAL]
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ n % 2 + 2 * div2 n = n
[PROOFSTEP]
rw [mod_two_of_bodd, bodd_add_div2]
[GOAL]
n : ℕ
⊢ n + n = 0 + n + n
[PROOFSTEP]
rw [Nat.zero_add]
[GOAL]
b : Bool
n : ℕ
⊢ bit b n = 2 * n + bif b then 1 else 0
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ bit false n = 2 * n + bif false then 1 else 0
case true n : ℕ ⊢ bit true n = 2 * n + bif true then 1 else 0
[PROOFSTEP]
apply bit0_val
[GOAL]
case true
n : ℕ
⊢ bit true n = 2 * n + bif true then 1 else 0
[PROOFSTEP]
apply bit1_val
[GOAL]
⊢ ∀ (n : ℕ), shiftr 0 n = 0
[PROOFSTEP]
intro n
[GOAL]
n : ℕ
⊢ shiftr 0 n = 0
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ shiftr 0 zero = 0
case succ n : ℕ IH : shiftr 0 n = 0 ⊢ shiftr 0 (succ n) = 0
[PROOFSTEP]
case zero => rw [shiftr]
[GOAL]
⊢ shiftr 0 zero = 0
[PROOFSTEP]
case zero => rw [shiftr]
[GOAL]
⊢ shiftr 0 zero = 0
[PROOFSTEP]
rw [shiftr]
[GOAL]
case succ
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
[PROOFSTEP]
case succ =>
  rw [shiftr, div2, IH]
  rfl
[GOAL]
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
[PROOFSTEP]
case succ =>
  rw [shiftr, div2, IH]
  rfl
[GOAL]
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
[PROOFSTEP]
rw [shiftr, div2, IH]
[GOAL]
n : ℕ
IH : shiftr 0 n = 0
⊢ (boddDiv2 0).snd = 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
h : n ≠ 0
⊢ div2 n < n
[PROOFSTEP]
rw [div2_val]
[GOAL]
n : ℕ
h : n ≠ 0
⊢ n / 2 < n
[PROOFSTEP]
apply (div_lt_iff_lt_mul <| succ_pos 1).2
[GOAL]
n : ℕ
h : n ≠ 0
⊢ n < n * succ 1
[PROOFSTEP]
have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1) (lt_of_le_of_ne n.zero_le h.symm)
[GOAL]
n : ℕ
h : n ≠ 0
this : n * 1 < n * succ 1
⊢ n < n * succ 1
[PROOFSTEP]
rwa [Nat.mul_one] at this 
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : n = 0
⊢ C n
[PROOFSTEP]
simp [n0]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : n = 0
⊢ C 0
[PROOFSTEP]
exact z
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
⊢ C n
[PROOFSTEP]
let n' := div2 n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
⊢ C n
[PROOFSTEP]
have _x : bit (bodd n) n' = n := by apply bit_decomp n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
⊢ bit (bodd n) n' = n
[PROOFSTEP]
apply bit_decomp n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
_x : bit (bodd n) n' = n
⊢ C n
[PROOFSTEP]
rw [← _x]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
_x : bit (bodd n) n' = n
⊢ C (bit (bodd n) n')
[PROOFSTEP]
exact f (bodd n) n' (binaryRec z f n')
[GOAL]
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
_x : bit (bodd n) n' = n
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n' n
[PROOFSTEP]
exact binaryRec_decreasing n0
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
⊢ binaryRec z f 0 = z
[PROOFSTEP]
rw [binaryRec]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
⊢ (if n0 : 0 = 0 then Eq.mpr (_ : C 0 = C 0) z
    else
      let n' := div2 0;
      let_fun _x := (_ : bit (bodd 0) (div2 0) = 0);
      Eq.mpr (_ : C 0 = C (bit (bodd 0) n')) (f (bodd 0) n' (binaryRec z f n'))) =
    z
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℕ
⊢ bodd (bit b n) = b
[PROOFSTEP]
rw [bit_val]
[GOAL]
b : Bool
n : ℕ
⊢ bodd (2 * n + bif b then 1 else 0) = b
[PROOFSTEP]
simp
[GOAL]
b : Bool
n : ℕ
⊢ bodd (bif b then 1 else 0) = b
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ bodd (bif false then 1 else 0) = false
[PROOFSTEP]
cases bodd n
[GOAL]
case true
n : ℕ
⊢ bodd (bif true then 1 else 0) = true
[PROOFSTEP]
cases bodd n
[GOAL]
case false.false
n : ℕ
⊢ bodd (bif false then 1 else 0) = false
[PROOFSTEP]
rfl
[GOAL]
case false.true
n : ℕ
⊢ bodd (bif false then 1 else 0) = false
[PROOFSTEP]
rfl
[GOAL]
case true.false
n : ℕ
⊢ bodd (bif true then 1 else 0) = true
[PROOFSTEP]
rfl
[GOAL]
case true.true
n : ℕ
⊢ bodd (bif true then 1 else 0) = true
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℕ
⊢ div2 (bit b n) = n
[PROOFSTEP]
rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
[GOAL]
b : Bool
n : ℕ
⊢ (bif b then 1 else 0) < 2
[PROOFSTEP]
cases b
[GOAL]
case H
b : Bool
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ (bif false then 1 else 0) < 2
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
⊢ (bif false then 1 else 0) < 2
[PROOFSTEP]
decide
[GOAL]
case true
n : ℕ
⊢ (bif true then 1 else 0) < 2
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
⊢ (bif true then 1 else 0) < 2
[PROOFSTEP]
decide
[GOAL]
case H.false
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
case H.true
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n + 1 - (k + 1)) = shiftr (shiftl' b m (n + 1)) (k + 1)
[PROOFSTEP]
simp [shiftl']
[GOAL]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (bit b (shiftl' b m n)) (k + 1)
[PROOFSTEP]
rw [Nat.add_comm, shiftr_add]
[GOAL]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (shiftr (bit b (shiftl' b m n)) 1) k
[PROOFSTEP]
simp [shiftr, div2_bit]
[GOAL]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (shiftl' b m n) k
[PROOFSTEP]
simp [shiftl'_sub, (Nat.le_of_succ_le_succ h)]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b n) (succ m) = testBit n m
[PROOFSTEP]
have : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m) :=
  by
  dsimp [shiftr]
  rw [div2_bit]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m)
[PROOFSTEP]
dsimp [shiftr]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ bodd (shiftr (div2 (bit b n)) m) = bodd (shiftr n m)
[PROOFSTEP]
rw [div2_bit]
[GOAL]
m : ℕ
b : Bool
n : ℕ
this : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m)
⊢ testBit (bit b n) (succ m) = testBit n m
[PROOFSTEP]
rw [← shiftr_add, Nat.add_comm] at this 
[GOAL]
m : ℕ
b : Bool
n : ℕ
this : bodd (shiftr (bit b n) (m + 1)) = bodd (shiftr n m)
⊢ testBit (bit b n) (succ m) = testBit n m
[PROOFSTEP]
exact this
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h : f false 0 z = z
b : Bool
n : ℕ
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)
[PROOFSTEP]
rw [binaryRec]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h : f false 0 z = z
b : Bool
n : ℕ
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
by_cases h :
  bit b n =
    0
      -- Note: this renames the original `h : f false 0 z = z` to `h'` and leaves `h : bit b n = 0`
[GOAL]
case pos
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h✝ : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
case neg
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h✝ : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
case pos h' =>
  simp [dif_pos h]
  generalize binaryRec z f (bit b n) = e
  revert e
  have bf := bodd_bit b n
  have n0 := div2_bit b n
  rw [h] at bf n0 
  simp at bf n0 
  subst bf n0
  rw [binaryRec_zero]
  intros
  rw [h']
  rfl
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
case pos h' =>
  simp [dif_pos h]
  generalize binaryRec z f (bit b n) = e
  revert e
  have bf := bodd_bit b n
  have n0 := div2_bit b n
  rw [h] at bf n0 
  simp at bf n0 
  subst bf n0
  rw [binaryRec_zero]
  intros
  rw [h']
  rfl
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
simp [dif_pos h]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
generalize binaryRec z f (bit b n) = e
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
e : C (bit b n)
⊢ Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
revert e
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
have bf := bodd_bit b n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
bf : bodd (bit b n) = b
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
have n0 := div2_bit b n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
bf : bodd (bit b n) = b
n0 : div2 (bit b n) = n
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
rw [h] at bf n0 
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
bf : bodd 0 = b
n0 : div2 0 = n
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
simp at bf n0 
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
bf : false = b
n0 : 0 = n
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
subst bf n0
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
h : bit false 0 = 0
⊢ C (bit false 0) → Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 (binaryRec z f 0)
[PROOFSTEP]
rw [binaryRec_zero]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
h : bit false 0 = 0
⊢ C (bit false 0) → Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 z
[PROOFSTEP]
intros
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
h : bit false 0 = 0
e✝ : C (bit false 0)
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 z
[PROOFSTEP]
rw [h']
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
h : bit false 0 = 0
e✝ : C (bit false 0)
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = z
[PROOFSTEP]
rfl
[GOAL]
case neg
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h✝ : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
case neg h' =>
  simp [dif_neg h]
  generalize
    @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) =
    e
  revert e
  rw [bodd_bit, div2_bit]
  intros; rfl
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
case neg h' =>
  simp [dif_neg h]
  generalize
    @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) =
    e
  revert e
  rw [bodd_bit, div2_bit]
  intros; rfl
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
simp [dif_neg h]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
generalize
  @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
    (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) =
  e
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
e : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n)))
⊢ Eq.mpr e (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) = f b n (binaryRec z f n)
[PROOFSTEP]
revert e
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ ∀ (e : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n)))),
    Eq.mpr e (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) = f b n (binaryRec z f n)
[PROOFSTEP]
rw [bodd_bit, div2_bit]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ ∀ (e : C (bit b n) = C (bit b n)), Eq.mpr e (f b n (binaryRec z f n)) = f b n (binaryRec z f n)
[PROOFSTEP]
intros
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
e✝ : C (bit b n) = C (bit b n)
⊢ Eq.mpr e✝ (f b n (binaryRec z f n)) = f b n (binaryRec z f n)
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
⊢ (binaryRec (bif f true false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
funext n
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
n : ℕ
⊢ binaryRec (bif f true false then bit false 0 else 0) (fun b n x => bit (f false b) (bif f false true then n else 0))
      n =
    bif f false true then n else 0
[PROOFSTEP]
apply bitCasesOn n
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (bif f true false then bit false 0 else 0) (fun b n x => bit (f false b) (bif f false true then n else 0))
        (bit b n) =
      bif f false true then bit b n else 0
[PROOFSTEP]
intro b n
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ binaryRec (bif f true false then bit false 0 else 0) (fun b n x => bit (f false b) (bif f false true then n else 0))
      (bit b n) =
    bif f false true then bit b n else 0
[PROOFSTEP]
rw [binaryRec_eq]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ bit (f false b) (bif f false true then n else 0) = bif f false true then bit b n else 0
[PROOFSTEP]
cases b
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false false) (bif f false true then n else 0) = bif f false true then bit false n else 0
[PROOFSTEP]
try rw [h] <;> induction' fft : f false true <;> simp [cond]
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false false) (bif f false true then n else 0) = bif f false true then bit false n else 0
[PROOFSTEP]
rw [h]
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit false (bif f false true then n else 0) = bif f false true then bit false n else 0
[PROOFSTEP]
induction' fft : f false true
[GOAL]
case h.false.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
x✝ : Bool
fft✝ : f false true = x✝
fft : f false true = false
⊢ bit false (bif false then n else 0) = bif false then bit false n else 0
[PROOFSTEP]
simp [cond]
[GOAL]
case h.false.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
x✝ : Bool
fft✝ : f false true = x✝
fft : f false true = true
⊢ bit false (bif true then n else 0) = bif true then bit false n else 0
[PROOFSTEP]
simp [cond]
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false true) (bif f false true then n else 0) = bif f false true then bit true n else 0
[PROOFSTEP]
try rw [h] <;> induction' fft : f false true <;> simp [cond]
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false true) (bif f false true then n else 0) = bif f false true then bit true n else 0
[PROOFSTEP]
rw [h]
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false true) (bif f false true then n else 0) = bif f false true then bit true n else 0
[PROOFSTEP]
cases f false true
[GOAL]
case h.true.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit false (bif false then n else 0) = bif false then bit true n else 0
case h.true.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit true (bif true then n else 0) = bif true then bit true n else 0
[PROOFSTEP]
case h.true.false => simp
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit false (bif false then n else 0) = bif false then bit true n else 0
[PROOFSTEP]
case h.true.false => simp
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit false (bif false then n else 0) = bif false then bit true n else 0
[PROOFSTEP]
simp
[GOAL]
case h.true.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit true (bif true then n else 0) = bif true then bit true n else 0
[PROOFSTEP]
case h.true.true => simp
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit true (bif true then n else 0) = bif true then bit true n else 0
[PROOFSTEP]
case h.true.true => simp
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit true (bif true then n else 0) = bif true then bit true n else 0
[PROOFSTEP]
simp
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ bit (f false false) (bif f false true then 0 else 0) = bif f true false then bit false 0 else 0
[PROOFSTEP]
rw [h, show cond (f false true) 0 0 = 0 by cases f false true <;> rfl,
  show cond (f true false) (bit false 0) 0 = 0 by cases f true false <;> rfl]
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif f false true then 0 else 0) = 0
[PROOFSTEP]
cases f false true
[GOAL]
case false
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif false then 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case true
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif true then 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif f true false then bit false 0 else 0) = 0
[PROOFSTEP]
cases f true false
[GOAL]
case false
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif false then bit false 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case true
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif true then bit false 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ bit false 0 = 0
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
n : ℕ
⊢ bitwise' f 0 n = bif f false true then n else 0
[PROOFSTEP]
unfold bitwise'
[GOAL]
f : Bool → Bool → Bool
n : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) 0 n =
    bif f false true then n else 0
[PROOFSTEP]
rw [binaryRec_zero]
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ bitwise' f m 0 = bif f true false then m else 0
[PROOFSTEP]
unfold bitwise'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    bif f true false then m else 0
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b n) 0 =
      bif f true false then bit b n else 0
[PROOFSTEP]
intros
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b✝ : Bool
n✝ : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b✝ n✝) 0 =
    bif f true false then bit b✝ n✝ else 0
[PROOFSTEP]
rw [binaryRec_eq, binaryRec_zero]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b✝ : Bool
n✝ : ℕ
⊢ (binaryRec (bif f true false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
exact bitwise'_bit_aux h
[GOAL]
f : Bool → Bool → Bool
⊢ bitwise' f 0 0 = 0
[PROOFSTEP]
rw [bitwise'_zero_left]
[GOAL]
f : Bool → Bool → Bool
⊢ (bif f false true then 0 else 0) = 0
[PROOFSTEP]
cases f false true
[GOAL]
case false
f : Bool → Bool → Bool
⊢ (bif false then 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case true
f : Bool → Bool → Bool
⊢ (bif true then 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bitwise' f (bit a m) (bit b n) = bit (f a b) (bitwise' f m n)
[PROOFSTEP]
unfold bitwise'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit a m)
      (bit b n) =
    bit (f a b)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m n)
[PROOFSTEP]
rw [binaryRec_eq, binaryRec_eq]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif f true false then bit a m else 0
[PROOFSTEP]
induction' ftf : f true false
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif false then bit a m else 0
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
[PROOFSTEP]
rw [show f a false = false by cases a <;> assumption]
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ f a false = false
[PROOFSTEP]
cases a
[GOAL]
case false
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ f false false = false
[PROOFSTEP]
assumption
[GOAL]
case true
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ f true false = false
[PROOFSTEP]
assumption
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ bit false
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif false then bit a m else 0
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
[PROOFSTEP]
apply @congr_arg _ _ _ 0 (bit false)
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
[PROOFSTEP]
swap
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
rw [show f a false = a by cases a <;> assumption]
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ f a false = a
[PROOFSTEP]
cases a
[GOAL]
case false
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ f false false = false
[PROOFSTEP]
assumption
[GOAL]
case true
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ f true false = true
[PROOFSTEP]
assumption
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit a
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
apply congr_arg (bit a)
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    m
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
all_goals {
  apply bitCasesOn m
  intro a m
  rw [binaryRec_eq, binaryRec_zero]
  · rfl
  · rw [← bitwise'_bit_aux h, ftf]
}
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    m
[PROOFSTEP]
{ apply bitCasesOn m
  intro a m
  rw [binaryRec_eq, binaryRec_zero]
  · rfl
  · rw [← bitwise'_bit_aux h, ftf]
}
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    m
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b n) 0 =
      bit b n
[PROOFSTEP]
intro a m
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
a : Bool
m : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit a m) 0 =
    bit a m
[PROOFSTEP]
rw [binaryRec_eq, binaryRec_zero]
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
a : Bool
m : ℕ
⊢ (bif true then bit a m else 0) = bit a m
[PROOFSTEP]
rfl
[GOAL]
case h.true.h
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
a : Bool
m : ℕ
⊢ (binaryRec (bif true then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
rw [← bitwise'_bit_aux h, ftf]
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
{ apply bitCasesOn m
  intro a m
  rw [binaryRec_eq, binaryRec_zero]
  · rfl
  · rw [← bitwise'_bit_aux h, ftf]
}
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b n) 0 =
      0
[PROOFSTEP]
intro a m
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
a : Bool
m : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit a m) 0 =
    0
[PROOFSTEP]
rw [binaryRec_eq, binaryRec_zero]
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
a : Bool
m : ℕ
⊢ (bif false then bit a m else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case h.false.h
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
a : Bool
m : ℕ
⊢ (binaryRec (bif false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
rw [← bitwise'_bit_aux h, ftf]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ (binaryRec (bif f true false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
exact bitwise'_bit_aux h
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
⊢ bitwise' (Function.swap f) = Function.swap (bitwise' f)
[PROOFSTEP]
funext m n
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ bitwise' (Function.swap f) m n = Function.swap (bitwise' f) m n
[PROOFSTEP]
revert n
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (Function.swap f) m n = Function.swap (bitwise' f) m n
[PROOFSTEP]
dsimp [Function.swap]
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (fun y x => f x y) m n = bitwise' f n m
[PROOFSTEP]
apply binaryRec _ _ m
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (fun y x => f x y) 0 n = bitwise' f n 0
[PROOFSTEP]
intro n
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    (∀ (n_1 : ℕ), bitwise' (fun y x => f x y) n n_1 = bitwise' f n_1 n) →
      ∀ (n_1 : ℕ), bitwise' (fun y x => f x y) (bit b n) n_1 = bitwise' f n_1 (bit b n)
[PROOFSTEP]
intro n
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ bitwise' (fun y x => f x y) 0 n = bitwise' f n 0
[PROOFSTEP]
rw [bitwise'_zero_left, bitwise'_zero_right]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ f false false = false
[PROOFSTEP]
exact h
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
⊢ ∀ (n_1 : ℕ),
    (∀ (n : ℕ), bitwise' (fun y x => f x y) n_1 n = bitwise' f n n_1) →
      ∀ (n_2 : ℕ), bitwise' (fun y x => f x y) (bit n n_1) n_2 = bitwise' f n_2 (bit n n_1)
[PROOFSTEP]
intros a ih m'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
⊢ bitwise' (fun y x => f x y) (bit n a) m' = bitwise' f m' (bit n a)
[PROOFSTEP]
apply bitCasesOn m'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
⊢ ∀ (b : Bool) (n_1 : ℕ), bitwise' (fun y x => f x y) (bit n a) (bit b n_1) = bitwise' f (bit b n_1) (bit n a)
[PROOFSTEP]
intro b n'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
b : Bool
n' : ℕ
⊢ bitwise' (fun y x => f x y) (bit n a) (bit b n') = bitwise' f (bit b n') (bit n a)
[PROOFSTEP]
rw [bitwise'_bit, bitwise'_bit, ih]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
b : Bool
n' : ℕ
⊢ f false false = false
[PROOFSTEP]
exact h
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
b : Bool
n' : ℕ
⊢ f false false = false
[PROOFSTEP]
exact h
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m n k : ℕ
⊢ testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
[PROOFSTEP]
revert m n
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
⊢ ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
⊢ ∀ (m n : ℕ), testBit (bitwise' f m n) zero = f (testBit m zero) (testBit n zero)
[PROOFSTEP]
intros m n
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
⊢ ∀ (m n : ℕ), testBit (bitwise' f m n) (succ k) = f (testBit m (succ k)) (testBit n (succ k))
[PROOFSTEP]
intros m n
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ testBit (bitwise' f m n) zero = f (testBit m zero) (testBit n zero)
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
⊢ testBit (bitwise' f m n) (succ k) = f (testBit m (succ k)) (testBit n (succ k))
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ ∀ (b : Bool) (n_1 : ℕ), testBit (bitwise' f (bit b n_1) n) zero = f (testBit (bit b n_1) zero) (testBit n zero)
[PROOFSTEP]
intros a m'
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
⊢ ∀ (b : Bool) (n_1 : ℕ),
    testBit (bitwise' f (bit b n_1) n) (succ k) = f (testBit (bit b n_1) (succ k)) (testBit n (succ k))
[PROOFSTEP]
intros a m'
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
⊢ testBit (bitwise' f (bit a m') n) zero = f (testBit (bit a m') zero) (testBit n zero)
[PROOFSTEP]
apply bitCasesOn n
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
⊢ testBit (bitwise' f (bit a m') n) (succ k) = f (testBit (bit a m') (succ k)) (testBit n (succ k))
[PROOFSTEP]
apply bitCasesOn n
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    testBit (bitwise' f (bit a m') (bit b n)) zero = f (testBit (bit a m') zero) (testBit (bit b n) zero)
[PROOFSTEP]
intros b n'
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    testBit (bitwise' f (bit a m') (bit b n)) (succ k) = f (testBit (bit a m') (succ k)) (testBit (bit b n) (succ k))
[PROOFSTEP]
intros b n'
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bitwise' f (bit a m') (bit b n')) zero = f (testBit (bit a m') zero) (testBit (bit b n') zero)
[PROOFSTEP]
rw [bitwise'_bit h]
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bitwise' f (bit a m') (bit b n')) (succ k) = f (testBit (bit a m') (succ k)) (testBit (bit b n') (succ k))
[PROOFSTEP]
rw [bitwise'_bit h]
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bit (f a b) (bitwise' f m' n')) zero = f (testBit (bit a m') zero) (testBit (bit b n') zero)
[PROOFSTEP]
simp [testBit_zero]
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bit (f a b) (bitwise' f m' n')) (succ k) = f (testBit (bit a m') (succ k)) (testBit (bit b n') (succ k))
[PROOFSTEP]
simp [testBit_succ, IH]
