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
a b c : ℕ
h : a ≠ lxor' b c
⊢ lxor' b c < a ∨ lxor' a c < b ∨ lxor' a b < c
set v := lxor' a (lxor' b c) with hv
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
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
have hab : lxor' a b = lxor' c v := by
  rw [hv]
  conv_rhs =>
    rw [lxor'_comm]
    simp [lxor'_assoc]
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
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
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]
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
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
have hbc : lxor' b c = lxor' a v := by simp [hv, ← lxor'_assoc]
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
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
obtain ⟨i, ⟨hi, hi'⟩⟩ := exists_most_significant_bit (lxor'_ne_zero.2 h)
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
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
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]
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
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
rcases this with (h | h | h)
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
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
on_goal 1 => left ; rw [hbc]
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
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
on_goal 2 => right; left; rw [hac]
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
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
on_goal 3 => right; right; rw [hab]
no goals
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
all_goals
  exact lt_of_testBit i (by
    rw [Nat.testBit_lxor', h, Bool.true_xor,hi]
    rfl
  ) h fun j hj => by
    rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
    trivial
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))
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
rw [hv]
no goals
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))
conv_rhs =>
  rw [lxor'_comm]
  simp [lxor'_assoc]
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))
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
rw [hv]
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)
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))
conv_rhs =>
  right
  rw [← lxor'_comm]
no goals
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)
rw [← lxor'_assoc, ← lxor'_assoc, lxor'_self, zero_lxor', lxor'_comm]
no goals
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
simp [hv, ← lxor'_assoc]
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
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
contrapose! hi
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
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
simp only [Bool.eq_false_eq_not_eq_true, Ne, testBit_lxor'] at hi⊢
no goals
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
rw [hi.1, hi.2.1, hi.2.2, Bool.xor_false, Bool.xor_false]
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
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
left
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.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
rw [hbc]
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
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
left
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.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
rw [hbc]
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
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
right
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
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
left
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.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
rw [hac]
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
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
right
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
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
left
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.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
rw [hac]
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
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
right
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
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
right
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
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
rw [hab]
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
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
right
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
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
right
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
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
rw [hab]
no goals
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
exact lt_of_testBit i (by
  rw [Nat.testBit_lxor', h, Bool.true_xor,hi]
  rfl
) h fun j hj => by
  rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
  trivial
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
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
rw [Nat.testBit_lxor', h, Bool.true_xor,hi]
no goals
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
rfl
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
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
rw [Nat.testBit_lxor', hi' _ hj, Bool.xor_false_right, eq_self_iff_true]
no goals
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
trivial