[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
