[GOAL]
n : ℕ
b : Bool
⊢ bit b n = 0 ↔ n = 0 ∧ b = false
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ bit false n = 0 ↔ n = 0 ∧ false = false
[PROOFSTEP]
simp [Nat.bit0_eq_zero, Nat.bit1_ne_zero]
[GOAL]
case true
n : ℕ
⊢ bit true n = 0 ↔ n = 0 ∧ true = false
[PROOFSTEP]
simp [Nat.bit0_eq_zero, Nat.bit1_ne_zero]
[GOAL]
n : ℕ
h : ∀ (i : ℕ), testBit n i = false
⊢ n = 0
[PROOFSTEP]
induction' n using Nat.binaryRec with b n hn
[GOAL]
case z
n : ℕ
h✝ : ∀ (i : ℕ), testBit n i = false
h : ∀ (i : ℕ), testBit 0 i = false
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case f
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
⊢ bit b n = 0
[PROOFSTEP]
have : b = false := by simpa using h 0
[GOAL]
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
⊢ b = false
[PROOFSTEP]
simpa using h 0
[GOAL]
case f
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
this : b = false
⊢ bit b n = 0
[PROOFSTEP]
rw [this, bit_false, bit0_val, hn fun i => by rw [← h (i + 1), testBit_succ], mul_zero]
[GOAL]
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
this : b = false
i : ℕ
⊢ testBit n i = false
[PROOFSTEP]
rw [← h (i + 1), testBit_succ]
[GOAL]
i : ℕ
⊢ testBit 0 i = false
[PROOFSTEP]
simp only [testBit, shiftr_zero, bodd_zero]
[GOAL]
n i : ℕ
⊢ testBit n i = List.getI (bits n) i
[PROOFSTEP]
induction' i with i ih generalizing n
[GOAL]
case zero
n✝ n : ℕ
⊢ testBit n zero = List.getI (bits n) zero
[PROOFSTEP]
simp [testBit, shiftr, bodd_eq_bits_head, List.getI_zero_eq_headI]
[GOAL]
case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ testBit n (succ i) = List.getI (bits n) (succ i)
[PROOFSTEP]
conv_lhs => rw [← bit_decomp n]
[GOAL]
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
| testBit n (succ i)
[PROOFSTEP]
rw [← bit_decomp n]
[GOAL]
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
| testBit n (succ i)
[PROOFSTEP]
rw [← bit_decomp n]
[GOAL]
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
| testBit n (succ i)
[PROOFSTEP]
rw [← bit_decomp n]
[GOAL]
case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ testBit (bit (bodd n) (div2 n)) (succ i) = List.getI (bits n) (succ i)
[PROOFSTEP]
rw [testBit_succ, ih n.div2, div2_bits_eq_tail]
[GOAL]
case succ
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ List.getI (List.tail (bits n)) i = List.getI (bits n) (succ i)
[PROOFSTEP]
cases n.bits
[GOAL]
case succ.nil
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
⊢ List.getI (List.tail []) i = List.getI [] (succ i)
[PROOFSTEP]
simp
[GOAL]
case succ.cons
n✝ i : ℕ
ih : ∀ (n : ℕ), testBit n i = List.getI (bits n) i
n : ℕ
head✝ : Bool
tail✝ : List Bool
⊢ List.getI (List.tail (head✝ :: tail✝)) i = List.getI (head✝ :: tail✝) (succ i)
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
h : ∀ (i : ℕ), testBit n i = testBit m i
⊢ n = m
[PROOFSTEP]
induction' n using Nat.binaryRec with b n hn generalizing m
[GOAL]
case z
n m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n i = testBit m✝ i
m : ℕ
h : ∀ (i : ℕ), testBit 0 i = testBit m i
⊢ 0 = m
[PROOFSTEP]
simp only [zero_testBit] at h
[GOAL]
case z
n m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n i = testBit m✝ i
m : ℕ
h : ∀ (i : ℕ), false = testBit m i
⊢ 0 = m
[PROOFSTEP]
exact (zero_of_testBit_eq_false fun i => (h i).symm).symm
[GOAL]
case f
n✝ m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = testBit m✝ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m : ℕ
h : ∀ (i : ℕ), testBit (bit b n) i = testBit m i
⊢ bit b n = m
[PROOFSTEP]
induction' m using Nat.binaryRec with b' m
[GOAL]
case f.z
n✝ m✝ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m i
h : ∀ (i : ℕ), testBit (bit b n) i = testBit 0 i
⊢ bit b n = 0
[PROOFSTEP]
simp only [zero_testBit] at h
[GOAL]
case f.z
n✝ m✝ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m i
h : ∀ (i : ℕ), testBit (bit b n) i = false
⊢ bit b n = 0
[PROOFSTEP]
exact zero_of_testBit_eq_false h
[GOAL]
case f.f
n✝ m✝¹ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝¹ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m✝ i
b' : Bool
m : ℕ
a✝ : (∀ (i : ℕ), testBit (bit b n) i = testBit m i) → bit b n = m
h : ∀ (i : ℕ), testBit (bit b n) i = testBit (bit b' m) i
⊢ bit b n = bit b' m
[PROOFSTEP]
suffices h' : n = m
[GOAL]
case f.f
n✝ m✝¹ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝¹ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m✝ i
b' : Bool
m : ℕ
a✝ : (∀ (i : ℕ), testBit (bit b n) i = testBit m i) → bit b n = m
h : ∀ (i : ℕ), testBit (bit b n) i = testBit (bit b' m) i
h' : n = m
⊢ bit b n = bit b' m
[PROOFSTEP]
rw [h', show b = b' by simpa using h 0]
[GOAL]
n✝ m✝¹ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝¹ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m✝ i
b' : Bool
m : ℕ
a✝ : (∀ (i : ℕ), testBit (bit b n) i = testBit m i) → bit b n = m
h : ∀ (i : ℕ), testBit (bit b n) i = testBit (bit b' m) i
h' : n = m
⊢ b = b'
[PROOFSTEP]
simpa using h 0
[GOAL]
case h'
n✝ m✝¹ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝¹ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m✝ i
b' : Bool
m : ℕ
a✝ : (∀ (i : ℕ), testBit (bit b n) i = testBit m i) → bit b n = m
h : ∀ (i : ℕ), testBit (bit b n) i = testBit (bit b' m) i
⊢ n = m
[PROOFSTEP]
exact hn fun i => by convert h (i + 1) using 1 <;> rw [testBit_succ]
[GOAL]
n✝ m✝¹ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝¹ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m✝ i
b' : Bool
m : ℕ
a✝ : (∀ (i : ℕ), testBit (bit b n) i = testBit m i) → bit b n = m
h : ∀ (i : ℕ), testBit (bit b n) i = testBit (bit b' m) i
i : ℕ
⊢ testBit n i = testBit m i
[PROOFSTEP]
convert h (i + 1) using 1
[GOAL]
case h.e'_2
n✝ m✝¹ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝¹ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m✝ i
b' : Bool
m : ℕ
a✝ : (∀ (i : ℕ), testBit (bit b n) i = testBit m i) → bit b n = m
h : ∀ (i : ℕ), testBit (bit b n) i = testBit (bit b' m) i
i : ℕ
⊢ testBit n i = testBit (bit b n) (i + 1)
[PROOFSTEP]
rw [testBit_succ]
[GOAL]
case h.e'_3
n✝ m✝¹ : ℕ
h✝¹ : ∀ (i : ℕ), testBit n✝ i = testBit m✝¹ i
b : Bool
n : ℕ
hn : ∀ {m : ℕ}, (∀ (i : ℕ), testBit n i = testBit m i) → n = m
m✝ : ℕ
h✝ : ∀ (i : ℕ), testBit (bit b n) i = testBit m✝ i
b' : Bool
m : ℕ
a✝ : (∀ (i : ℕ), testBit (bit b n) i = testBit m i) → bit b n = m
h : ∀ (i : ℕ), testBit (bit b n) i = testBit (bit b' m) i
i : ℕ
⊢ testBit m i = testBit (bit b' m) (i + 1)
[PROOFSTEP]
rw [testBit_succ]
[GOAL]
n : ℕ
h : n ≠ 0
⊢ ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
[PROOFSTEP]
induction' n using Nat.binaryRec with b n hn
[GOAL]
case z
n : ℕ
h✝ : n ≠ 0
h : 0 ≠ 0
⊢ ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
[PROOFSTEP]
exact False.elim (h rfl)
[GOAL]
case f
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
[PROOFSTEP]
by_cases h' : n = 0
[GOAL]
case pos
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : n = 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
[PROOFSTEP]
subst h'
[GOAL]
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, testBit (bit b 0) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b 0) j = false
[PROOFSTEP]
rw [show b = true by
    revert h
    cases b <;> simp]
[GOAL]
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ b = true
[PROOFSTEP]
revert h
[GOAL]
n : ℕ
h : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit b 0 ≠ 0 → b = true
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
h : n ≠ 0
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit false 0 ≠ 0 → false = true
[PROOFSTEP]
simp
[GOAL]
case true
n : ℕ
h : n ≠ 0
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
⊢ bit true 0 ≠ 0 → true = true
[PROOFSTEP]
simp
[GOAL]
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, testBit (bit true 0) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit true 0) j = false
[PROOFSTEP]
refine' ⟨0, ⟨by rw [testBit_zero], fun j hj => _⟩⟩
[GOAL]
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ testBit (bit true 0) 0 = true
[PROOFSTEP]
rw [testBit_zero]
[GOAL]
case pos
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
j : ℕ
hj : 0 < j
⊢ testBit (bit true 0) j = false
[PROOFSTEP]
obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)
[GOAL]
case pos.intro
n : ℕ
h✝ : n ≠ 0
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
j' : ℕ
hj : 0 < succ j'
⊢ testBit (bit true 0) (succ j') = false
[PROOFSTEP]
rw [testBit_succ, zero_testBit]
[GOAL]
case neg
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
[PROOFSTEP]
obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
[GOAL]
case neg.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
⊢ ∃ i, testBit (bit b n) i = true ∧ ∀ (j : ℕ), i < j → testBit (bit b n) j = false
[PROOFSTEP]
refine' ⟨k + 1, ⟨by rw [testBit_succ, hk], fun j hj => _⟩⟩
[GOAL]
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
⊢ testBit (bit b n) (k + 1) = true
[PROOFSTEP]
rw [testBit_succ, hk]
[GOAL]
case neg.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j : ℕ
hj : k + 1 < j
⊢ testBit (bit b n) j = false
[PROOFSTEP]
obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj )
[GOAL]
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j : ℕ
hj : k + 1 < j
⊢ j ≠ 0
[PROOFSTEP]
intro x
[GOAL]
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j : ℕ
hj : k + 1 < j
x : j = 0
⊢ False
[PROOFSTEP]
subst x
[GOAL]
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
hj : k + 1 < 0
⊢ False
[PROOFSTEP]
simp at hj
[GOAL]
case neg.intro.intro.intro
n✝ : ℕ
h✝ : n✝ ≠ 0
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, testBit n i = true ∧ ∀ (j : ℕ), i < j → testBit n j = false
h : bit b n ≠ 0
h' : ¬n = 0
k : ℕ
hk : testBit n k = true
hk' : ∀ (j : ℕ), k < j → testBit n j = false
j' : ℕ
hj : k + 1 < succ j'
⊢ testBit (bit b n) (succ j') = false
[PROOFSTEP]
exact (testBit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))
[GOAL]
n m i : ℕ
hn : testBit n i = false
hm : testBit m i = true
hnm : ∀ (j : ℕ), i < j → testBit n j = testBit m j
⊢ n < m
[PROOFSTEP]
induction' n using Nat.binaryRec with b n hn' generalizing i m
[GOAL]
case z
n m✝ i✝ : ℕ
hn✝ : testBit n i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n j = testBit m✝ j
m i : ℕ
hn : testBit 0 i = false
hm : testBit m i = true
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit m j
⊢ 0 < m
[PROOFSTEP]
contrapose! hm
[GOAL]
case z
n m✝ i✝ : ℕ
hn✝ : testBit n i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n j = testBit m✝ j
m i : ℕ
hn : testBit 0 i = false
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit m j
hm : m ≤ 0
⊢ testBit m i ≠ true
[PROOFSTEP]
rw [le_zero_iff] at hm
[GOAL]
case z
n m✝ i✝ : ℕ
hn✝ : testBit n i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n j = testBit m✝ j
m i : ℕ
hn : testBit 0 i = false
hnm : ∀ (j : ℕ), i < j → testBit 0 j = testBit m j
hm : m = 0
⊢ testBit m i ≠ true
[PROOFSTEP]
simp [hm]
[GOAL]
case f
n✝ m✝ i✝ : ℕ
hn✝ : testBit n✝ i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m i : ℕ
hn : testBit (bit b n) i = false
hm : testBit m i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j
⊢ bit b n < m
[PROOFSTEP]
induction' m using Nat.binaryRec with b' m hm' generalizing i
[GOAL]
case f.z
n✝ m✝ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m j
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit 0 i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit 0 j
⊢ bit b n < 0
[PROOFSTEP]
exact False.elim (Bool.ff_ne_tt ((zero_testBit i).symm.trans hm))
[GOAL]
case f.f
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
⊢ bit b n < bit b' m
[PROOFSTEP]
by_cases hi : i = 0
[GOAL]
case pos
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
hi : i = 0
⊢ bit b n < bit b' m
[PROOFSTEP]
subst hi
[GOAL]
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hn : testBit (bit b n) 0 = false
hm : testBit (bit b' m) 0 = true
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
⊢ bit b n < bit b' m
[PROOFSTEP]
simp only [testBit_zero] at hn hm
[GOAL]
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
⊢ bit b n < bit b' m
[PROOFSTEP]
have : n = m := eq_of_testBit_eq fun i => by convert hnm (i + 1) (Nat.zero_lt_succ _) using 1 <;> rw [testBit_succ]
[GOAL]
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
i : ℕ
⊢ testBit n i = testBit m i
[PROOFSTEP]
convert hnm (i + 1) (Nat.zero_lt_succ _) using 1
[GOAL]
case h.e'_2
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
i : ℕ
⊢ testBit n i = testBit (bit b n) (i + 1)
[PROOFSTEP]
rw [testBit_succ]
[GOAL]
case h.e'_3
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
i : ℕ
⊢ testBit m i = testBit (bit b' m) (i + 1)
[PROOFSTEP]
rw [testBit_succ]
[GOAL]
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
this : n = m
⊢ bit b n < bit b' m
[PROOFSTEP]
rw [hn, hm, this, bit_false, bit_true, bit0_val, bit1_val]
[GOAL]
case pos
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
hnm : ∀ (j : ℕ), 0 < j → testBit (bit b n) j = testBit (bit b' m) j
hn : b = false
hm : b' = true
this : n = m
⊢ 2 * m < 2 * m + 1
[PROOFSTEP]
exact lt_add_one _
[GOAL]
case neg
n✝ m✝¹ i✝¹ : ℕ
hn✝¹ : testBit n✝ i✝¹ = false
hm✝¹ : testBit m✝¹ i✝¹ = true
hnm✝¹ : ∀ (j : ℕ), i✝¹ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i✝ : ℕ
hn✝ : testBit (bit b n) i✝ = false
hm✝ : testBit m✝ i✝ = true
hnm✝ : ∀ (j : ℕ), i✝ < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i : ℕ
hn : testBit (bit b n) i = false
hm : testBit (bit b' m) i = true
hnm : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬i = 0
⊢ bit b n < bit b' m
[PROOFSTEP]
obtain ⟨i', rfl⟩ := exists_eq_succ_of_ne_zero hi
[GOAL]
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hn : testBit (bit b n) (succ i') = false
hm : testBit (bit b' m) (succ i') = true
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
⊢ bit b n < bit b' m
[PROOFSTEP]
simp only [testBit_succ] at hn hm
[GOAL]
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
⊢ bit b n < bit b' m
[PROOFSTEP]
have := hn' _ hn hm fun j hj => by convert hnm j.succ (succ_lt_succ hj) using 1 <;> rw [testBit_succ]
[GOAL]
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
j : ℕ
hj : i' < j
⊢ testBit n j = testBit m j
[PROOFSTEP]
convert hnm j.succ (succ_lt_succ hj) using 1
[GOAL]
case h.e'_2
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
j : ℕ
hj : i' < j
⊢ testBit n j = testBit (bit b n) (succ j)
[PROOFSTEP]
rw [testBit_succ]
[GOAL]
case h.e'_3
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
j : ℕ
hj : i' < j
⊢ testBit m j = testBit (bit b' m) (succ j)
[PROOFSTEP]
rw [testBit_succ]
[GOAL]
case neg.intro
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
b : Bool
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hn✝ : testBit (bit b n) i = false
hm✝ : testBit m✝ i = true
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m✝ j
b' : Bool
m : ℕ
hm' :
  ∀ (i : ℕ),
    testBit (bit b n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit b n) j = testBit m j) → bit b n < m
i' : ℕ
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit b n) j = testBit (bit b' m) j
hi : ¬succ i' = 0
hn : testBit n i' = false
hm : testBit m i' = true
this : n < m
⊢ bit b n < bit b' m
[PROOFSTEP]
cases b
[GOAL]
case neg.intro.false
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
b' : Bool
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit false n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit false n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m j) → bit false n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit false n) j = testBit (bit b' m) j
⊢ bit false n < bit b' m
[PROOFSTEP]
cases b'
[GOAL]
case neg.intro.true
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
b' : Bool
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit true n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit true n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m j) → bit true n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit true n) j = testBit (bit b' m) j
⊢ bit true n < bit b' m
[PROOFSTEP]
cases b'
[GOAL]
case neg.intro.false.false
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit false n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit false n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m j) → bit false n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit false n) j = testBit (bit false m) j
⊢ bit false n < bit false m
[PROOFSTEP]
simp only [bit_false, bit_true, bit0_val n, bit1_val n, bit0_val m, bit1_val m]
[GOAL]
case neg.intro.false.true
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit false n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit false n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m j) → bit false n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit false n) j = testBit (bit true m) j
⊢ bit false n < bit true m
[PROOFSTEP]
simp only [bit_false, bit_true, bit0_val n, bit1_val n, bit0_val m, bit1_val m]
[GOAL]
case neg.intro.true.false
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit true n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit true n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m j) → bit true n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit true n) j = testBit (bit false m) j
⊢ bit true n < bit false m
[PROOFSTEP]
simp only [bit_false, bit_true, bit0_val n, bit1_val n, bit0_val m, bit1_val m]
[GOAL]
case neg.intro.true.true
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit true n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit true n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m j) → bit true n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit true n) j = testBit (bit true m) j
⊢ bit true n < bit true m
[PROOFSTEP]
simp only [bit_false, bit_true, bit0_val n, bit1_val n, bit0_val m, bit1_val m]
[GOAL]
case neg.intro.false.false
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit false n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit false n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m j) → bit false n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit false n) j = testBit (bit false m) j
⊢ 2 * n < 2 * m
[PROOFSTEP]
linarith only [this]
[GOAL]
case neg.intro.false.true
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit false n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit false n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit false n) j = testBit m j) → bit false n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit false n) j = testBit (bit true m) j
⊢ 2 * n < 2 * m + 1
[PROOFSTEP]
linarith only [this]
[GOAL]
case neg.intro.true.false
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit true n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit true n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m j) → bit true n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit true n) j = testBit (bit false m) j
⊢ 2 * n + 1 < 2 * m
[PROOFSTEP]
linarith only [this]
[GOAL]
case neg.intro.true.true
n✝ m✝¹ i✝ : ℕ
hn✝¹ : testBit n✝ i✝ = false
hm✝¹ : testBit m✝¹ i✝ = true
hnm✝¹ : ∀ (j : ℕ), i✝ < j → testBit n✝ j = testBit m✝¹ j
n : ℕ
hn' :
  ∀ {m : ℕ} (i : ℕ), testBit n i = false → testBit m i = true → (∀ (j : ℕ), i < j → testBit n j = testBit m j) → n < m
m✝ i : ℕ
hm✝ : testBit m✝ i = true
m i' : ℕ
hi : ¬succ i' = 0
hn✝ : testBit n i' = false
hm : testBit m i' = true
this : n < m
hn : testBit (bit true n) i = false
hnm✝ : ∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m✝ j
hm' :
  ∀ (i : ℕ),
    testBit (bit true n) i = false →
      testBit m i = true → (∀ (j : ℕ), i < j → testBit (bit true n) j = testBit m j) → bit true n < m
hnm : ∀ (j : ℕ), succ i' < j → testBit (bit true n) j = testBit (bit true m) j
⊢ 2 * n + 1 < 2 * m + 1
[PROOFSTEP]
linarith only [this]
[GOAL]
n : ℕ
⊢ testBit (2 ^ n) n = true
[PROOFSTEP]
rw [testBit, shiftr_eq_div_pow, Nat.div_self (pow_pos (α := ℕ) zero_lt_two n), bodd_one]
[GOAL]
n m : ℕ
hm : n ≠ m
⊢ testBit (2 ^ n) m = false
[PROOFSTEP]
rw [testBit, shiftr_eq_div_pow]
[GOAL]
n m : ℕ
hm : n ≠ m
⊢ bodd (2 ^ n / 2 ^ m) = false
[PROOFSTEP]
cases' hm.lt_or_lt with hm hm
[GOAL]
case inl
n m : ℕ
hm✝ : n ≠ m
hm : n < m
⊢ bodd (2 ^ n / 2 ^ m) = false
[PROOFSTEP]
rw [Nat.div_eq_zero, bodd_zero]
[GOAL]
case inl
n m : ℕ
hm✝ : n ≠ m
hm : n < m
⊢ 2 ^ n < 2 ^ m
[PROOFSTEP]
exact Nat.pow_lt_pow_of_lt_right one_lt_two hm
[GOAL]
case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ n / 2 ^ m) = false
[PROOFSTEP]
rw [pow_div hm.le zero_lt_two, ← tsub_add_cancel_of_le (succ_le_of_lt <| tsub_pos_of_lt hm)]
  -- Porting note: XXX why does this make it work?
[GOAL]
case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ (n - m - succ 0 + succ 0)) = false
[PROOFSTEP]
rw [(rfl : succ 0 = 1)]
[GOAL]
case inr
n m : ℕ
hm✝ : n ≠ m
hm : m < n
⊢ bodd (2 ^ (n - m - succ 0 + succ 0)) = false
[PROOFSTEP]
simp only [ge_iff_le, tsub_le_iff_right, pow_succ, bodd_mul, Bool.and_eq_false_eq_eq_false_or_eq_false, or_true]
[GOAL]
n m : ℕ
⊢ (testBit (2 ^ n) m = true) = (n = m)
[PROOFSTEP]
by_cases h : n = m
[GOAL]
case pos
n m : ℕ
h : n = m
⊢ (testBit (2 ^ n) m = true) = (n = m)
[PROOFSTEP]
cases h
[GOAL]
case pos.refl
n : ℕ
⊢ (testBit (2 ^ n) n = true) = (n = n)
[PROOFSTEP]
simp
[GOAL]
case neg
n m : ℕ
h : ¬n = m
⊢ (testBit (2 ^ n) m = true) = (n = m)
[PROOFSTEP]
rw [testBit_two_pow_of_ne h]
[GOAL]
case neg
n m : ℕ
h : ¬n = m
⊢ (false = true) = (n = m)
[PROOFSTEP]
simp [h]
[GOAL]
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
hf' : f false false = false
n m : ℕ
this : bitwise' f = swap (bitwise' f)
⊢ bitwise' f n m = bitwise' f m n
[PROOFSTEP]
conv_lhs => rw [this]
[GOAL]
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
hf' : f false false = false
n m : ℕ
this : bitwise' f = swap (bitwise' f)
| bitwise' f n m
[PROOFSTEP]
rw [this]
[GOAL]
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
hf' : f false false = false
n m : ℕ
this : bitwise' f = swap (bitwise' f)
| bitwise' f n m
[PROOFSTEP]
rw [this]
[GOAL]
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
hf' : f false false = false
n m : ℕ
this : bitwise' f = swap (bitwise' f)
| bitwise' f n m
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
⊢ lxor' 0 n = n
[PROOFSTEP]
simp only [Bool.xor_false_left, Nat.bitwise'_zero_left, eq_self_iff_true, Bool.cond_true, lxor']
[GOAL]
n : ℕ
⊢ lxor' n 0 = n
[PROOFSTEP]
simp [lxor']
[GOAL]
n : ℕ
⊢ land' 0 n = 0
[PROOFSTEP]
simp only [Nat.bitwise'_zero_left, Bool.cond_false, eq_self_iff_true, land', Bool.false_and]
[GOAL]
n : ℕ
⊢ land' n 0 = 0
[PROOFSTEP]
simp [land']
[GOAL]
n : ℕ
⊢ lor' 0 n = n
[PROOFSTEP]
simp only [Nat.bitwise'_zero_left, Bool.false_or, eq_self_iff_true, Bool.cond_true, Nat.lor']
[GOAL]
n : ℕ
⊢ lor' n 0 = n
[PROOFSTEP]
simp [lor']
[GOAL]
n m k : ℕ
⊢ lxor' (lxor' n m) k = lxor' n (lxor' m k)
[PROOFSTEP]
bitwise_assoc_tac
[GOAL]
n m k : ℕ
⊢ land' (land' n m) k = land' n (land' m k)
[PROOFSTEP]
bitwise_assoc_tac
[GOAL]
n m k : ℕ
⊢ lor' (lor' n m) k = lor' n (lor' m k)
[PROOFSTEP]
bitwise_assoc_tac
[GOAL]
n i : ℕ
⊢ testBit (lxor' n n) i = false
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
⊢ lxor' (lxor' m n) n = m
[PROOFSTEP]
rw [lxor'_assoc, lxor'_self, lxor'_zero]
[GOAL]
n m : ℕ
⊢ lxor' n (lxor' n m) = m
[PROOFSTEP]
rw [← lxor'_assoc, lxor'_self, zero_lxor']
[GOAL]
n m m' : ℕ
h : lxor' n m = lxor' n m'
⊢ m = m'
[PROOFSTEP]
rw [← lxor'_cancel_left n m, ← lxor'_cancel_left n m', h]
[GOAL]
n m m' : ℕ
h : lxor' m n = lxor' m' n
⊢ m = m'
[PROOFSTEP]
rw [← lxor_cancel_right n m, ← lxor_cancel_right n m', h]
[GOAL]
n m : ℕ
⊢ lxor' n m = 0 ↔ n = m
[PROOFSTEP]
rw [← lxor'_self n, lxor'_right_inj, eq_comm]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
set v := lxor' a (lxor' b c) with hv
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
have hab : lxor' a b = lxor' c v := by
  rw [hv]
  conv_rhs =>
    rw [lxor'_comm]
    simp [lxor'_assoc]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
⊢ lxor' a b = lxor' c v
[PROOFSTEP]
rw [hv]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
⊢ lxor' a b = lxor' c (lxor' a (lxor' b c))
[PROOFSTEP]
conv_rhs =>
  rw [lxor'_comm]
  simp [lxor'_assoc]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
| lxor' c (lxor' a (lxor' b c))
[PROOFSTEP]
  rw [lxor'_comm]
  simp [lxor'_assoc]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
| lxor' c (lxor' a (lxor' b c))
[PROOFSTEP]
  rw [lxor'_comm]
  simp [lxor'_assoc]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
| lxor' c (lxor' a (lxor' b c))
[PROOFSTEP]
rw [lxor'_comm]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
| lxor' (lxor' a (lxor' b c)) c
[PROOFSTEP]
simp [lxor'_assoc]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
have hac : lxor' a c = lxor' b v := by
  rw [hv]
  conv_rhs =>
    right
    rw [← lxor'_comm]
  rw [← lxor'_assoc, ← lxor'_assoc, lxor'_self, zero_lxor', lxor'_comm]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
⊢ lxor' a c = lxor' b v
[PROOFSTEP]
rw [hv]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
⊢ lxor' a c = lxor' b (lxor' a (lxor' b c))
[PROOFSTEP]
conv_rhs =>
  right
  rw [← lxor'_comm]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
| lxor' b (lxor' a (lxor' b c))
[PROOFSTEP]
  right
  rw [← lxor'_comm]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
| lxor' b (lxor' a (lxor' b c))
[PROOFSTEP]
  right
  rw [← lxor'_comm]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
| lxor' b (lxor' a (lxor' b c))
[PROOFSTEP]
right
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
| lxor' a (lxor' b c)
[PROOFSTEP]
rw [← lxor'_comm]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
⊢ lxor' a c = lxor' b (lxor' (lxor' b c) a)
[PROOFSTEP]
rw [← lxor'_assoc, ← lxor'_assoc, lxor'_self, zero_lxor', lxor'_comm]
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
have hbc : lxor' b c = lxor' a v := by
  simp [hv, ← lxor'_assoc]
    -- If `i` is the position of the most significant bit of `v`, then at least one of `a`, `b`, `c`
      -- has a one bit at position `i`.
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
⊢ lxor' b c = lxor' a v
[PROOFSTEP]
simp [hv, ← lxor'_assoc]
  -- If `i` is the position of the most significant bit of `v`, then at least one of `a`, `b`, `c`
    -- has a one bit at position `i`.
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
obtain ⟨i, ⟨hi, hi'⟩⟩ := exists_most_significant_bit (lxor'_ne_zero.2 h)
[GOAL]
case intro.intro
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
have : testBit a i = true ∨ testBit b i = true ∨ testBit c i = true :=
  by
  contrapose! hi
  simp only [Bool.eq_false_eq_not_eq_true, Ne, testBit_lxor'] at hi ⊢
  rw [hi.1, hi.2.1, hi.2.2, Bool.xor_false, Bool.xor_false]
    -- If, say, `a` has a one bit at position `i`, then `a xor v` has a zero bit at position `i`, but
      -- the same bits as `a` in positions greater than `j`, so `a xor v < a`.
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
⊢ testBit a i = true ∨ testBit b i = true ∨ testBit c i = true
[PROOFSTEP]
contrapose! hi
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
hi : testBit a i ≠ true ∧ testBit b i ≠ true ∧ testBit c i ≠ true
⊢ testBit (lxor' a (lxor' b c)) i ≠ true
[PROOFSTEP]
simp only [Bool.eq_false_eq_not_eq_true, Ne, testBit_lxor'] at hi ⊢
[GOAL]
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
hi : testBit a i = false ∧ testBit b i = false ∧ testBit c i = false
⊢ _root_.xor (testBit a i) (_root_.xor (testBit b i) (testBit c i)) = false
[PROOFSTEP]
rw [hi.1, hi.2.1, hi.2.2, Bool.xor_false, Bool.xor_false]
  -- If, say, `a` has a one bit at position `i`, then `a xor v` has a zero bit at position `i`, but
    -- the same bits as `a` in positions greater than `j`, so `a xor v < a`.
[GOAL]
case intro.intro
a b c : ℕ
h : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
this : testBit a i = true ∨ testBit b i = true ∨ testBit c i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
rcases this with (h | h | h)
[GOAL]
case intro.intro.inl
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
case intro.intro.inr.inl
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
case intro.intro.inr.inr
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
on_goal 1 => left; rw [hbc]
[GOAL]
case intro.intro.inl
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
case intro.intro.inr.inl
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
case intro.intro.inr.inr
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
on_goal 1 => left; rw [hbc]
[GOAL]
case intro.intro.inl
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
left
[GOAL]
case intro.intro.inl.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' b c < a
[PROOFSTEP]
rw [hbc]
[GOAL]
case intro.intro.inl.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' a v < a
case intro.intro.inr.inl
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
case intro.intro.inr.inr
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
on_goal 2 => right; left; rw [hac]
[GOAL]
case intro.intro.inl.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' a v < a
case intro.intro.inr.inl
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
case intro.intro.inr.inr
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
on_goal 2 => right; left; rw [hac]
[GOAL]
case intro.intro.inr.inl
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
right
[GOAL]
case intro.intro.inr.inl.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
left
[GOAL]
case intro.intro.inr.inl.h.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' a c < b
[PROOFSTEP]
rw [hac]
[GOAL]
case intro.intro.inl.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' a v < a
case intro.intro.inr.inl.h.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b v < b
case intro.intro.inr.inr
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
on_goal 3 => right; right; rw [hab]
[GOAL]
case intro.intro.inl.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' a v < a
case intro.intro.inr.inl.h.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b v < b
case intro.intro.inr.inr
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
on_goal 3 => right; right; rw [hab]
[GOAL]
case intro.intro.inr.inr
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
right
[GOAL]
case intro.intro.inr.inr.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' a c < b ∨ lxor' a b < c
[PROOFSTEP]
right
[GOAL]
case intro.intro.inr.inr.h.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' a b < c
[PROOFSTEP]
rw [hab]
[GOAL]
case intro.intro.inl.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' a v < a
case intro.intro.inr.inl.h.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b v < b
case intro.intro.inr.inr.h.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' c v < c
[PROOFSTEP]
all_goals
  exact
    lt_of_testBit i
      (by
        -- Porting note: this was originally `simp [h, hi]`
        rw [Nat.testBit_lxor', h, Bool.true_xor, hi]
        rfl)
      h fun j hj => by
      -- Porting note: this was originally `simp [hi' _ hj]`
      rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
      trivial
[GOAL]
case intro.intro.inl.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ lxor' a v < a
[PROOFSTEP]
exact
  lt_of_testBit i
    (by
      -- Porting note: this was originally `simp [h, hi]`
      rw [Nat.testBit_lxor', h, Bool.true_xor, hi]
      rfl)
    h fun j hj => by
    -- Porting note: this was originally `simp [hi' _ hj]`
    rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
    trivial
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ testBit (lxor' a v) i = false
[PROOFSTEP]
rw [Nat.testBit_lxor', h, Bool.true_xor, hi]
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
⊢ (!true) = false
[PROOFSTEP]
rfl
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
j : ℕ
hj : i < j
⊢ testBit (lxor' a v) j = testBit a j
[PROOFSTEP]
rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit a i = true
j : ℕ
hj : i < j
⊢ True
[PROOFSTEP]
trivial
[GOAL]
case intro.intro.inr.inl.h.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ lxor' b v < b
[PROOFSTEP]
exact
  lt_of_testBit i
    (by
      -- Porting note: this was originally `simp [h, hi]`
      rw [Nat.testBit_lxor', h, Bool.true_xor, hi]
      rfl)
    h fun j hj => by
    -- Porting note: this was originally `simp [hi' _ hj]`
    rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
    trivial
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ testBit (lxor' b v) i = false
[PROOFSTEP]
rw [Nat.testBit_lxor', h, Bool.true_xor, hi]
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
⊢ (!true) = false
[PROOFSTEP]
rfl
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
j : ℕ
hj : i < j
⊢ testBit (lxor' b v) j = testBit b j
[PROOFSTEP]
rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit b i = true
j : ℕ
hj : i < j
⊢ True
[PROOFSTEP]
trivial
[GOAL]
case intro.intro.inr.inr.h.h
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ lxor' c v < c
[PROOFSTEP]
exact
  lt_of_testBit i
    (by
      -- Porting note: this was originally `simp [h, hi]`
      rw [Nat.testBit_lxor', h, Bool.true_xor, hi]
      rfl)
    h fun j hj => by
    -- Porting note: this was originally `simp [hi' _ hj]`
    rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
    trivial
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ testBit (lxor' c v) i = false
[PROOFSTEP]
rw [Nat.testBit_lxor', h, Bool.true_xor, hi]
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
⊢ (!true) = false
[PROOFSTEP]
rfl
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
j : ℕ
hj : i < j
⊢ testBit (lxor' c v) j = testBit c j
[PROOFSTEP]
rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
[GOAL]
a b c : ℕ
h✝ : a ≠ lxor' b c
v : ℕ := lxor' a (lxor' b c)
hv : v = lxor' a (lxor' b c)
hab : lxor' a b = lxor' c v
hac : lxor' a c = lxor' b v
hbc : lxor' b c = lxor' a v
i : ℕ
hi : testBit (lxor' a (lxor' b c)) i = true
hi' : ∀ (j : ℕ), i < j → testBit (lxor' a (lxor' b c)) j = false
h : testBit c i = true
j : ℕ
hj : i < j
⊢ True
[PROOFSTEP]
trivial


[GOAL]
m k : ℕ
⊢ shiftl m (k + 1) = m * 2 ^ (k + 1)
[PROOFSTEP]
show bit0 (shiftl m k) = m * (2 ^ k * 2)
[GOAL]
m k : ℕ
⊢ bit0 (shiftl m k) = m * (2 ^ k * 2)
[PROOFSTEP]
rw [bit0_val, shiftl_eq_mul_pow m k, mul_comm 2, mul_assoc]
[GOAL]
m : ℕ
⊢ shiftl' true m 0 + 1 = (m + 1) * 2 ^ 0
[PROOFSTEP]
simp [shiftl, shiftl', pow_zero, Nat.one_mul]
[GOAL]
m k : ℕ
⊢ shiftl' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)
[PROOFSTEP]
change bit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2)
[GOAL]
m k : ℕ
⊢ bit1 (shiftl' true m k) + 1 = (m + 1) * (2 ^ k * 2)
[PROOFSTEP]
rw [bit1_val]
[GOAL]
m k : ℕ
⊢ 2 * shiftl' true m k + 1 + 1 = (m + 1) * (2 ^ k * 2)
[PROOFSTEP]
change 2 * (shiftl' true m k + 1) = _
[GOAL]
m k : ℕ
⊢ 2 * (shiftl' true m k + 1) = (m + 1) * (2 ^ k * 2)
[PROOFSTEP]
rw [shiftl'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2]
[GOAL]
m k : ℕ
⊢ div2 (m / 2 ^ k) = m / 2 ^ (k + 1)
[PROOFSTEP]
rw [div2_val, Nat.div_div_eq_div_mul, Nat.pow_succ]
[GOAL]
b : Bool
m : ℕ
h : m ≠ 0
n : ℕ
⊢ shiftl' b m n ≠ 0
[PROOFSTEP]
induction n
[GOAL]
case zero
b : Bool
m : ℕ
h : m ≠ 0
⊢ shiftl' b m zero ≠ 0
[PROOFSTEP]
simp [bit_ne_zero, shiftl', *]
[GOAL]
case succ
b : Bool
m : ℕ
h : m ≠ 0
n✝ : ℕ
n_ih✝ : shiftl' b m n✝ ≠ 0
⊢ shiftl' b m (succ n✝) ≠ 0
[PROOFSTEP]
simp [bit_ne_zero, shiftl', *]
[GOAL]
⊢ size 0 = 0
[PROOFSTEP]
simp [size]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ size (bit b n) = succ (size n)
[PROOFSTEP]
rw [size]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
conv =>
  lhs
  rw [binaryRec]
  simp [h]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
  lhs
  rw [binaryRec]
  simp [h]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
  lhs
  rw [binaryRec]
  simp [h]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
lhs
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| binaryRec 0 (fun x x => succ) (bit b n)
[PROOFSTEP]
rw [binaryRec]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
| if n0 : bit b n = 0 then Eq.mpr (_ : ℕ = ℕ) 0
  else
    let n' := div2 (bit b n);
    let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
    Eq.mpr (_ : ℕ = ℕ) (succ (binaryRec 0 (fun x x => succ) n'))
[PROOFSTEP]
simp [h]
[GOAL]
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ succ (binaryRec 0 (fun x x => succ) (div2 (bit b n))) = succ (binaryRec 0 (fun x x => succ) n)
[PROOFSTEP]
rw [div2_bit]
[GOAL]
⊢ size (bit1 0) = 1
[PROOFSTEP]
rw [size_bit1, size_zero]
[GOAL]
b : Bool
m n : ℕ
h : shiftl' b m n ≠ 0
⊢ size (shiftl' b m n) = size m + n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
b : Bool
m n : ℕ
h✝ : shiftl' b m n ≠ 0
h : shiftl' b m zero ≠ 0
⊢ size (shiftl' b m zero) = size m + zero
[PROOFSTEP]
simp [shiftl'] at h ⊢
[GOAL]
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : shiftl' b m (succ n) ≠ 0
⊢ size (shiftl' b m (succ n)) = size m + succ n
[PROOFSTEP]
simp [shiftl'] at h ⊢
[GOAL]
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ size (bit b (shiftl' b m n)) = size m + succ n
[PROOFSTEP]
rw [size_bit h, Nat.add_succ]
[GOAL]
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
by_cases s0 : shiftl' b m n = 0 <;> [skip; rw [IH s0]]
[GOAL]
case succ
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
by_cases s0 : shiftl' b m n = 0
[GOAL]
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
s0 : shiftl' b m n = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
skip
[GOAL]
case neg
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
s0 : ¬shiftl' b m n = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
rw [IH s0]
[GOAL]
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b (shiftl' b m n) = 0
s0 : shiftl' b m n = 0
⊢ succ (size (shiftl' b m n)) = succ (size m + n)
[PROOFSTEP]
rw [s0] at h ⊢
[GOAL]
case pos
b : Bool
m n✝ : ℕ
h✝ : shiftl' b m n✝ ≠ 0
n : ℕ
IH : shiftl' b m n ≠ 0 → size (shiftl' b m n) = size m + n
h : ¬bit b 0 = 0
s0 : shiftl' b m n = 0
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
cases b
[GOAL]
case pos.false
m n✝ n : ℕ
h✝ : shiftl' false m n✝ ≠ 0
IH : shiftl' false m n ≠ 0 → size (shiftl' false m n) = size m + n
h : ¬bit false 0 = 0
s0 : shiftl' false m n = 0
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
exact absurd rfl h
[GOAL]
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
have : shiftl' true m n + 1 = 1 := congr_arg (· + 1) s0
[GOAL]
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
this : shiftl' true m n + 1 = 1
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
rw [shiftl'_tt_eq_mul_pow] at this
[GOAL]
case pos.true
m n✝ n : ℕ
h✝ : shiftl' true m n✝ ≠ 0
IH : shiftl' true m n ≠ 0 → size (shiftl' true m n) = size m + n
h : ¬bit true 0 = 0
s0 : shiftl' true m n = 0
this : (m + 1) * 2 ^ n = 1
⊢ succ (size 0) = succ (size m + n)
[PROOFSTEP]
obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
[GOAL]
case pos.true
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : (0 + 1) * 2 ^ n = 1
⊢ succ (size 0) = succ (size 0 + n)
[PROOFSTEP]
simp only [zero_add, one_mul] at this
[GOAL]
case pos.true
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : 2 ^ n = 1
⊢ succ (size 0) = succ (size 0 + n)
[PROOFSTEP]
obtain rfl : n = 0 :=
  Nat.eq_zero_of_le_zero (le_of_not_gt fun hn => ne_of_gt (pow_lt_pow_of_lt_right (by decide) hn) this)
[GOAL]
n✝ n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n✝ ≠ 0
IH : shiftl' true 0 n ≠ 0 → size (shiftl' true 0 n) = size 0 + n
s0 : shiftl' true 0 n = 0
this : 2 ^ n = 1
hn : n > 0
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
case pos.true
n : ℕ
h✝ : ¬bit true 0 = 0
h : shiftl' true 0 n ≠ 0
IH : shiftl' true 0 0 ≠ 0 → size (shiftl' true 0 0) = size 0 + 0
s0 : shiftl' true 0 0 = 0
this : 2 ^ 0 = 1
⊢ succ (size 0) = succ (size 0 + 0)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ n < 2 ^ size n
[PROOFSTEP]
rw [← one_shiftl]
[GOAL]
n : ℕ
⊢ n < shiftl 1 (size n)
[PROOFSTEP]
have : ∀ {n}, n = 0 → n < shiftl 1 (size n) := by simp
[GOAL]
n : ℕ
⊢ ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ n < shiftl 1 (size n)
[PROOFSTEP]
apply binaryRec _ _ n
[GOAL]
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ 0 < shiftl 1 (size 0)
[PROOFSTEP]
apply this rfl
[GOAL]
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ ∀ (b : Bool) (n : ℕ), n < shiftl 1 (size n) → bit b n < shiftl 1 (size (bit b n))
[PROOFSTEP]
intro b n IH
[GOAL]
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
⊢ bit b n < shiftl 1 (size (bit b n))
[PROOFSTEP]
by_cases h : bit b n = 0
[GOAL]
case pos
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : bit b n = 0
⊢ bit b n < shiftl 1 (size (bit b n))
[PROOFSTEP]
apply this h
[GOAL]
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : ¬bit b n = 0
⊢ bit b n < shiftl 1 (size (bit b n))
[PROOFSTEP]
rw [size_bit h, shiftl_succ]
[GOAL]
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : ¬bit b n = 0
⊢ bit b n < bit0 (shiftl 1 (size n))
[PROOFSTEP]
exact bit_lt_bit0 _ IH
[GOAL]
m n : ℕ
h : size m ≤ n
⊢ 2 > 0
[PROOFSTEP]
decide
[GOAL]
m n : ℕ
⊢ m < 2 ^ n → size m ≤ n
[PROOFSTEP]
rw [← one_shiftl]
[GOAL]
m n : ℕ
⊢ m < shiftl 1 n → size m ≤ n
[PROOFSTEP]
revert n
[GOAL]
m : ℕ
⊢ ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
[PROOFSTEP]
apply binaryRec _ _ m
[GOAL]
m : ℕ
⊢ ∀ {n : ℕ}, 0 < shiftl 1 n → size 0 ≤ n
[PROOFSTEP]
intro n
[GOAL]
m n : ℕ
⊢ 0 < shiftl 1 n → size 0 ≤ n
[PROOFSTEP]
simp
[GOAL]
m : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    (∀ {n_1 : ℕ}, n < shiftl 1 n_1 → size n ≤ n_1) → ∀ {n_1 : ℕ}, bit b n < shiftl 1 n_1 → size (bit b n) ≤ n_1
[PROOFSTEP]
intro b m IH n h
[GOAL]
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
n : ℕ
h : bit b m < shiftl 1 n
⊢ size (bit b m) ≤ n
[PROOFSTEP]
by_cases e : bit b m = 0
[GOAL]
case pos
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
n : ℕ
h : bit b m < shiftl 1 n
e : bit b m = 0
⊢ size (bit b m) ≤ n
[PROOFSTEP]
simp [e]
[GOAL]
case neg
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
n : ℕ
h : bit b m < shiftl 1 n
e : ¬bit b m = 0
⊢ size (bit b m) ≤ n
[PROOFSTEP]
rw [size_bit e]
[GOAL]
case neg
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
n : ℕ
h : bit b m < shiftl 1 n
e : ¬bit b m = 0
⊢ succ (size m) ≤ n
[PROOFSTEP]
cases' n with n
[GOAL]
case neg.zero
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
e : ¬bit b m = 0
h : bit b m < shiftl 1 zero
⊢ succ (size m) ≤ zero
[PROOFSTEP]
exact e.elim (Nat.eq_zero_of_le_zero (le_of_lt_succ h))
[GOAL]
case neg.succ
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < shiftl 1 (succ n)
⊢ succ (size m) ≤ succ n
[PROOFSTEP]
apply succ_le_succ (IH _)
[GOAL]
m✝ : ℕ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < shiftl 1 n → size m ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < shiftl 1 (succ n)
⊢ m < shiftl 1 n
[PROOFSTEP]
apply lt_imp_lt_of_le_imp_le (fun h' => bit0_le_bit _ h') h
[GOAL]
m n : ℕ
⊢ m < size n ↔ 2 ^ m ≤ n
[PROOFSTEP]
rw [← not_lt, Decidable.iff_not_comm, not_lt, size_le]
[GOAL]
n : ℕ
⊢ 0 < size n ↔ 0 < n
[PROOFSTEP]
rw [lt_size]
[GOAL]
n : ℕ
⊢ 2 ^ 0 ≤ n ↔ 0 < n
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ size n = 0 ↔ n = 0
[PROOFSTEP]
have := @size_pos n
[GOAL]
n : ℕ
this : 0 < size n ↔ 0 < n
⊢ size n = 0 ↔ n = 0
[PROOFSTEP]
simp [pos_iff_ne_zero] at this
[GOAL]
n : ℕ
this : ¬size n = 0 ↔ ¬n = 0
⊢ size n = 0 ↔ n = 0
[PROOFSTEP]
exact Decidable.not_iff_not.1 this
[GOAL]
n : ℕ
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ List.length (bits n) = size n
[PROOFSTEP]
induction' n using Nat.binaryRec' with b n h ih
[GOAL]
case z
⊢ List.length (bits 0) = size 0
[PROOFSTEP]
simp
[GOAL]
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ List.length (bits (bit b n)) = size (bit b n)
[PROOFSTEP]
rw [size_bit, bits_append_bit _ _ h]
[GOAL]
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ List.length (b :: bits n) = succ (size n)
[PROOFSTEP]
simp [ih]
[GOAL]
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ bit b n ≠ 0
[PROOFSTEP]
simpa [bit_eq_zero_iff]


[GOAL]
n : ℕ
⊢ pred n = Option.getD (ppred n) 0
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ pred zero = Option.getD (ppred zero) 0
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ pred (succ n✝) = Option.getD (ppred (succ n✝)) 0
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ Option.getD (ppred (m - n)) 0 = Option.getD (psub m (n + 1)) 0
[PROOFSTEP]
rw [sub_eq_psub m n, psub]
[GOAL]
m n : ℕ
⊢ Option.getD (ppred (Option.getD (psub m n) 0)) 0 = Option.getD (psub m n >>= ppred) 0
[PROOFSTEP]
cases psub m n
[GOAL]
case none
m n : ℕ
⊢ Option.getD (ppred (Option.getD none 0)) 0 = Option.getD (none >>= ppred) 0
[PROOFSTEP]
rfl
[GOAL]
case some
m n val✝ : ℕ
⊢ Option.getD (ppred (Option.getD (some val✝) 0)) 0 = Option.getD (some val✝ >>= ppred) 0
[PROOFSTEP]
rfl
[GOAL]
m : ℕ
⊢ ppred 0 = some m ↔ succ m = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
m : ℕ
⊢ ppred 0 = some m → succ m = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
m : ℕ
⊢ succ m = 0 → ppred 0 = some m
[PROOFSTEP]
intro h
[GOAL]
case mp
m : ℕ
h : ppred 0 = some m
⊢ succ m = 0
[PROOFSTEP]
contradiction
[GOAL]
case mpr
m : ℕ
h : succ m = 0
⊢ ppred 0 = some m
[PROOFSTEP]
contradiction
[GOAL]
m n : ℕ
⊢ ppred (n + 1) = some m ↔ succ m = n + 1
[PROOFSTEP]
constructor
[GOAL]
case mp
m n : ℕ
⊢ ppred (n + 1) = some m → succ m = n + 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
m n : ℕ
⊢ succ m = n + 1 → ppred (n + 1) = some m
[PROOFSTEP]
intro h
[GOAL]
case mp
m n : ℕ
h : ppred (n + 1) = some m
⊢ succ m = n + 1
[PROOFSTEP]
injection h
[GOAL]
case mpr
m n : ℕ
h : succ m = n + 1
⊢ ppred (n + 1) = some m
[PROOFSTEP]
injection h
[GOAL]
case mp
m n : ℕ
val_eq✝ : Nat.add n 0 = m
⊢ succ m = n + 1
[PROOFSTEP]
subst m
[GOAL]
case mpr
m n : ℕ
n_eq✝ : m = Nat.add n 0
⊢ ppred (n + 1) = some m
[PROOFSTEP]
subst m
[GOAL]
case mp
n : ℕ
⊢ succ (Nat.add n 0) = n + 1
[PROOFSTEP]
rfl
[GOAL]
case mpr
n : ℕ
⊢ ppred (n + 1) = some (Nat.add n 0)
[PROOFSTEP]
rfl
[GOAL]
⊢ ppred 0 = none ↔ 0 = 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ppred (n + 1) = none ↔ n + 1 = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ ppred (n + 1) = none → n + 1 = 0
[PROOFSTEP]
intro
[GOAL]
case mpr
n : ℕ
⊢ n + 1 = 0 → ppred (n + 1) = none
[PROOFSTEP]
intro
[GOAL]
case mp
n : ℕ
a✝ : ppred (n + 1) = none
⊢ n + 1 = 0
[PROOFSTEP]
contradiction
[GOAL]
case mpr
n : ℕ
a✝ : n + 1 = 0
⊢ ppred (n + 1) = none
[PROOFSTEP]
contradiction
[GOAL]
m k : ℕ
⊢ psub m 0 = some k ↔ k + 0 = m
[PROOFSTEP]
simp [eq_comm]
[GOAL]
m n k : ℕ
⊢ psub m (n + 1) = some k ↔ k + (n + 1) = m
[PROOFSTEP]
apply Option.bind_eq_some.trans
[GOAL]
m n k : ℕ
⊢ (∃ a, psub m (Nat.add n 0) = some a ∧ ppred a = some k) ↔ k + (n + 1) = m
[PROOFSTEP]
simp only [psub_eq_some, ppred_eq_some]
[GOAL]
m n k : ℕ
⊢ (∃ a, a + Nat.add n 0 = m ∧ succ k = a) ↔ k + (n + 1) = m
[PROOFSTEP]
simp [add_comm, add_left_comm, Nat.succ_eq_add_one]
[GOAL]
m n : ℕ
⊢ psub m n = none ↔ m < n
[PROOFSTEP]
cases s : psub m n
[GOAL]
case none
m n : ℕ
s : psub m n = none
⊢ none = none ↔ m < n
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ some val✝ = none ↔ m < n
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case none
m n : ℕ
s : psub m n = none
⊢ m < n
[PROOFSTEP]
show m < n
[GOAL]
case none
m n : ℕ
s : psub m n = none
⊢ m < n
[PROOFSTEP]
refine' lt_of_not_ge fun h => _
[GOAL]
case none
m n : ℕ
s : psub m n = none
h : m ≥ n
⊢ False
[PROOFSTEP]
cases' le.dest h with k e
[GOAL]
case none.intro
m n : ℕ
s : psub m n = none
h : m ≥ n
k : ℕ
e : n + k = m
⊢ False
[PROOFSTEP]
injection s.symm.trans (psub_eq_some.2 <| (add_comm _ _).trans e)
[GOAL]
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ m
[PROOFSTEP]
show n ≤ m
[GOAL]
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ m
[PROOFSTEP]
rw [← psub_eq_some.1 s]
[GOAL]
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ val✝ + n
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
m n k : ℕ
⊢ psub m (n + k) = do
    let __do_lift ← psub m n
    psub __do_lift k
[PROOFSTEP]
induction k
[GOAL]
case zero
m n : ℕ
⊢ psub m (n + zero) = do
    let __do_lift ← psub m n
    psub __do_lift zero
case succ
m n n✝ : ℕ
n_ih✝ :
  psub m (n + n✝) = do
    let __do_lift ← psub m n
    psub __do_lift n✝
⊢ psub m (n + succ n✝) = do
    let __do_lift ← psub m n
    psub __do_lift (succ n✝)
[PROOFSTEP]
simp [Option.bind_eq_bind, Option.bind_some]
[GOAL]
case succ
m n n✝ : ℕ
n_ih✝ :
  psub m (n + n✝) = do
    let __do_lift ← psub m n
    psub __do_lift n✝
⊢ psub m (n + succ n✝) = do
    let __do_lift ← psub m n
    psub __do_lift (succ n✝)
[PROOFSTEP]
simp [*, Nat.add_succ]
[GOAL]
m n : ℕ
⊢ psub' m n = psub m n
[PROOFSTEP]
rw [psub']
[GOAL]
m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = psub m n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
m n : ℕ
h : n ≤ m
⊢ some (m - n) = psub m n
case neg m n : ℕ h : ¬n ≤ m ⊢ none = psub m n
[PROOFSTEP]
exact (psub_eq_sub h).symm
[GOAL]
case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = psub m n
[PROOFSTEP]
exact (psub_eq_none.2 (not_le.1 h)).symm