awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n m : ℕ
⊢ n &&& m = m &&& n

Tactic:
bitwise_comm Bool.and_comm n m

Premises used: WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, Nat.land, Nat.bitwise_comm, Bool.and_comm
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i : ℕ
⊢ n &&& HPow.hPow (α := ℕ) 2 i = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i

Tactic:
eq_of_testBit_eq fun j => ?_

Premises used: Nat.eq_of_testBit_eq
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i : ℕ
refine : ∀ (j : ℕ), (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j
⊢ n &&& HPow.hPow (α := ℕ) 2 i = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i

Tactic:
refine eq_of_testBit_eq fun j => ?_

Premises used: Nat.eq_of_testBit_eq
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i j : ℕ
inl : (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit i
inr :
  ∀ (hij : i ≠ j), (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i : ℕ
inl :
  ∀ (h : n.testBit i = false),
    (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = (false.toNat * HPow.hPow (α := ℕ) 2 i).testBit i
inl₁ :
  ∀ (h : n.testBit i = true), (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = (true.toNat * HPow.hPow (α := ℕ) 2 i).testBit i
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit i

Tactic:
cases h : n.testBit i

Premises used: Nat.testBit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i j : ℕ
hij : i ≠ j
inr :
  ∀ (h : n.testBit i = false),
    (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = (false.toNat * HPow.hPow (α := ℕ) 2 i).testBit j
inr₁ :
  ∀ (h : n.testBit i = true), (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = (true.toNat * HPow.hPow (α := ℕ) 2 i).testBit j
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = ((n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i).testBit j

Tactic:
cases h : n.testBit i

Premises used: Nat.testBit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i : ℕ
h : n.testBit i = false
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = (false.toNat * HPow.hPow (α := ℕ) 2 i).testBit i

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i : ℕ
h : n.testBit i = true
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit i = (true.toNat * HPow.hPow (α := ℕ) 2 i).testBit i

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = (false.toNat * HPow.hPow (α := ℕ) 2 i).testBit j

Tactic:
simp [testBit_two_pow_of_ne hij]

Premises used: Nat.testBit_two_pow_of_ne
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& HPow.hPow (α := ℕ) 2 i).testBit j = (true.toNat * HPow.hPow (α := ℕ) 2 i).testBit j

Tactic:
simp [testBit_two_pow_of_ne hij]

Premises used: Nat.testBit_two_pow_of_ne
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n i : ℕ
rw : HPow.hPow (α := ℕ) 2 i &&& n = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
rw₁ : n &&& HPow.hPow (α := ℕ) 2 i = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
rw₂ rw₃ : (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i = (n.testBit i).toNat * HPow.hPow (α := ℕ) 2 i
⊢ HPow.hPow (α := ℕ) 2 i &&& n = HPow.hPow (α := ℕ) 2 i * (n.testBit i).toNat

Tactic:
rw [mul_comm, land_comm, and_two_pow]

Premises used: Nat.land_comm, mul_comm, Nat.and_two_pow
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n m k : ℕ
zero : ∀ (m k : ℕ), 0 &&& m &&& k = 0 &&& (m &&& k)
bit bit₁ bit₂ :
  ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n &&& m &&& k = n &&& (m &&& k)) (m k : ℕ),
    Nat.bit b n &&& m &&& k = Nat.bit b n &&& (m &&& k)
bit₃ bit₄ :
  ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n &&& m &&& k = n &&& (m &&& k)) (k : ℕ) (b' : Bool) (m : ℕ)
    (hm : Nat.bit b n &&& m &&& k = Nat.bit b n &&& (m &&& k)),
    Nat.bit b n &&& Nat.bit b' m &&& k = Nat.bit b n &&& (Nat.bit b' m &&& k)
⊢ n &&& m &&& k = n &&& (m &&& k)

Tactic:
bitwise_assoc_tac
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n m k : ℕ
zero : ∀ (m k : ℕ), 0 ||| m ||| k = 0 ||| (m ||| k)
bit bit₁ bit₂ :
  ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n ||| m ||| k = n ||| (m ||| k)) (m k : ℕ),
    Nat.bit b n ||| m ||| k = Nat.bit b n ||| (m ||| k)
bit₃ bit₄ :
  ∀ (b : Bool) (n : ℕ) (hn : ∀ (m k : ℕ), n ||| m ||| k = n ||| (m ||| k)) (k : ℕ) (b' : Bool) (m : ℕ)
    (hm : Nat.bit b n ||| m ||| k = Nat.bit b n ||| (m ||| k)),
    Nat.bit b n ||| Nat.bit b' m ||| k = Nat.bit b n ||| (Nat.bit b' m ||| k)
⊢ n ||| m ||| k = n ||| (m ||| k)

Tactic:
bitwise_assoc_tac
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
h : a ^^^ b ^^^ c ≠ 0
⊢ let v := a ^^^ b ^^^ c;
  v ≠ 0

Tactic:
set v := a ^^^ b ^^^ c with hv
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
h : a ^^^ b ^^^ c ≠ 0
h₁ :
  let v := a ^^^ b ^^^ c;
  v ≠ 0
⊢ let v := a ^^^ b ^^^ c;
  v = a ^^^ b ^^^ c

Tactic:
set v := a ^^^ b ^^^ c with hv
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
rw : a ^^^ b = v ^^^ c
rw₁ rw₂ : a ^^^ b = a ^^^ b
⊢ a ^^^ b = c ^^^ v

Tactic:
rw [Nat.xor_comm c, Nat.xor_xor_cancel_right]

Premises used: Nat.xor_xor_cancel_right, Nat.xor_comm
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
⊢ a ^^^ b = c ^^^ v

Tactic:
have hab : a ^^^ b = c ^^^ v := by
    rw [Nat.xor_comm c, Nat.xor_xor_cancel_right]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
rw : b ^^^ c = a ^^^ (a ^^^ b) ^^^ c
rw₁ rw₂ : b ^^^ c = b ^^^ c
⊢ b ^^^ c = a ^^^ v

Tactic:
rw [← Nat.xor_assoc, Nat.xor_xor_cancel_left]

Premises used: Nat.xor_assoc, Nat.xor_xor_cancel_left
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
⊢ b ^^^ c = a ^^^ v

Tactic:
have hbc : b ^^^ c = a ^^^ v := by
    rw [← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
rw : c ^^^ a = b ^^^ (a ^^^ b ^^^ c)
rw₁ : c ^^^ a = b ^^^ (a ^^^ (b ^^^ c))
rw₂ : c ^^^ a = b ^^^ (b ^^^ c ^^^ a)
rw₃ : c ^^^ a = b ^^^ (b ^^^ c) ^^^ a
rw₄ rw₅ : c ^^^ a = c ^^^ a
⊢ c ^^^ a = b ^^^ v

Tactic:
rw [hv, Nat.xor_assoc, Nat.xor_comm a, ← Nat.xor_assoc, Nat.xor_xor_cancel_left]

Premises used: Nat.xor_assoc, Nat.xor_comm, Nat.xor_xor_cancel_left
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
⊢ c ^^^ a = b ^^^ v

Tactic:
have hca : c ^^^ a = b ^^^ v := by
    rw [hv, Nat.xor_assoc, Nat.xor_comm a, ← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
obtain :
  ∀ (i : ℕ) (hi : v.testBit i = true) (hi' : ∀ (j : ℕ), i < j → v.testBit j = false),
    b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
obtain ⟨i, ⟨hi, hi'⟩⟩ := exists_most_significant_bit h

Premises used: Nat.exists_most_significant_bit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
contrapose! : ∀ (hi : a.testBit i ≠ true ∧ b.testBit i ≠ true ∧ c.testBit i ≠ true), v.testBit i ≠ true
⊢ a.testBit i = true ∨ b.testBit i = true ∨ c.testBit i = true

Tactic:
contrapose! hi
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i ≠ true ∧ b.testBit i ≠ true ∧ c.testBit i ≠ true
simp_rw : ∀ (hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false), v.testBit i = false
⊢ v.testBit i ≠ true

Tactic:
simp_rw [Bool.eq_false_eq_not_eq_true] at hi ⊢

Premises used: Bool.eq_false_eq_not_eq_true
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false
rw : (false ^^ false ^^ false) = false
⊢ v.testBit i = false

Tactic:
rw [testBit_xor, testBit_xor, hi.1, hi.2.1, hi.2.2]

Premises used: Nat.testBit_xor, And.right, And.left
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false
⊢ (false ^^ false ^^ false) = false

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
⊢ a.testBit i = true ∨ b.testBit i = true ∨ c.testBit i = true

Tactic:
have : testBit a i ∨ testBit b i ∨ testBit c i := by
    contrapose! hi
    simp_rw [Bool.eq_false_eq_not_eq_true] at hi ⊢
    rw [testBit_xor, testBit_xor, hi.1, hi.2.1, hi.2.2]
    rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
this : a.testBit i = true ∨ b.testBit i = true ∨ c.testBit i = true
inl : ∀ (h : a.testBit i = true), b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
inr : ∀ (h : b.testBit i = true), b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
inr₁ : ∀ (h : c.testBit i = true), b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
obtain h | h | h := this
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
inl : b ^^^ c < a
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
left
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
inl : a ^^^ v < a
⊢ b ^^^ c < a

Tactic:
rw [hbc]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
inl : a ^^^ v < a
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
on_goal 1 => left; rw [hbc]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
inr : c ^^^ a < b ∨ a ^^^ b < c
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
right
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
inr : c ^^^ a < b
⊢ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
left
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
inr : b ^^^ v < b
⊢ c ^^^ a < b

Tactic:
rw [hca]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
inr : b ^^^ v < b
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
on_goal 2 => right; left; rw [hca]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
inr : c ^^^ a < b ∨ a ^^^ b < c
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
right
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
inr : a ^^^ b < c
⊢ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
right
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
inr : c ^^^ v < c
⊢ a ^^^ b < c

Tactic:
rw [hab]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
inr : c ^^^ v < c
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c

Tactic:
on_goal 3 => right; right; rw [hab]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
⊢ a ^^^ v < a

Tactic:
lt_of_testBit i ?_ h fun j hj => ?_

Premises used: Nat.lt_of_testBit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
inl : (a ^^^ v).testBit i = false
inl₁ : ∀ (j : ℕ) (hj : i < j), (a ^^^ v).testBit j = a.testBit j
⊢ a ^^^ v < a

Tactic:
refine lt_of_testBit i ?_ h fun j hj => ?_

Premises used: Nat.lt_of_testBit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
inl : (true ^^ true) = false
⊢ (a ^^^ v).testBit i = false

Tactic:
rw [testBit_xor, h, hi]

Premises used: Nat.testBit_xor
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
⊢ (true ^^ true) = false

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : a.testBit i = true
j : ℕ
hj : i < j
⊢ (a ^^^ v).testBit j = a.testBit j

Tactic:
simp only [testBit_xor, hi' _ hj, Bool.bne_false]

Premises used: Nat.testBit_xor, Bool.bne_false
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ b ^^^ v < b

Tactic:
lt_of_testBit i ?_ h fun j hj => ?_

Premises used: Nat.lt_of_testBit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
inr : (b ^^^ v).testBit i = false
inr₁ : ∀ (j : ℕ) (hj : i < j), (b ^^^ v).testBit j = b.testBit j
⊢ b ^^^ v < b

Tactic:
refine lt_of_testBit i ?_ h fun j hj => ?_

Premises used: Nat.lt_of_testBit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
inr : (true ^^ true) = false
⊢ (b ^^^ v).testBit i = false

Tactic:
rw [testBit_xor, h, hi]

Premises used: Nat.testBit_xor
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
⊢ (true ^^ true) = false

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : b.testBit i = true
j : ℕ
hj : i < j
⊢ (b ^^^ v).testBit j = b.testBit j

Tactic:
simp only [testBit_xor, hi' _ hj, Bool.bne_false]

Premises used: Nat.testBit_xor, Bool.bne_false
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ c ^^^ v < c

Tactic:
lt_of_testBit i ?_ h fun j hj => ?_

Premises used: Nat.lt_of_testBit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
inr : (c ^^^ v).testBit i = false
inr₁ : ∀ (j : ℕ) (hj : i < j), (c ^^^ v).testBit j = c.testBit j
⊢ c ^^^ v < c

Tactic:
refine lt_of_testBit i ?_ h fun j hj => ?_

Premises used: Nat.lt_of_testBit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
inr : (true ^^ true) = false
⊢ (c ^^^ v).testBit i = false

Tactic:
rw [testBit_xor, h, hi]

Premises used: Nat.testBit_xor
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
⊢ (true ^^ true) = false

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h_1 : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
hbc : b ^^^ c = a ^^^ v
hca : c ^^^ a = b ^^^ v
i : ℕ
hi : v.testBit i = true
hi' : ∀ (j : ℕ), i < j → v.testBit j = false
h : c.testBit i = true
j : ℕ
hj : i < j
⊢ (c ^^^ v).testBit j = c.testBit j

Tactic:
simp only [testBit_xor, hi' _ hj, Bool.bne_false]

Premises used: Nat.testBit_xor, Bool.bne_false
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
h : a < b ^^^ c
inl : ∀ (ha : b ^^^ c < a), a ^^^ c < b ∨ a ^^^ b < c
inr : ∀ (hb : c ^^^ a < b), a ^^^ c < b ∨ a ^^^ b < c
inr₁ : ∀ (hc : a ^^^ b < c), a ^^^ c < b ∨ a ^^^ b < c
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
obtain ha | hb | hc := xor_trichotomy <| Nat.xor_assoc _ _ _ ▸ xor_ne_zero_iff.2 h.ne

Premises used: Nat.xor_trichotomy
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
h : a < b ^^^ c
ha : b ^^^ c < a
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
(h.asymm ha).elim

Premises used: False.elim, LT.lt.asymm
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
h : a < b ^^^ c
hb : c ^^^ a < b
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
Or.inl <| Nat.xor_comm _ _ ▸ hb

Premises used: Eq.rec, Nat.xor_comm, Or.inl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
h : a < b ^^^ c
hc : a ^^^ b < c
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
Or.inr hc

Premises used: Or.inr
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a b c : ℕ
h : a < b ^^^ c
ha : b ^^^ c < a
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
exacts [(h.asymm ha).elim, Or.inl <| Nat.xor_comm _ _ ▸ hb, Or.inr hc]

Premises used: False.elim, LT.lt.asymm, Or.inl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m n : ℕ
pos : ∀ (h : (m + n) % 2 = 0), (m ^^^ n) % 2 = (m + n) % 2
neg : ∀ (h : ¬(m + n) % 2 = 0), (m ^^^ n) % 2 = (m + n) % 2
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
by_cases h : (m + n) % 2 = 0

Premises used: HAdd.hAdd
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m n : ℕ
h : (m + n) % 2 = 0
pos : m % 2 = 1 ↔ n % 2 = 1
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
simp only [h, mod_two_eq_zero_iff_testBit_zero, testBit_zero, xor_mod_two_eq_one, decide_not,
      Bool.decide_iff_dist, Bool.not_eq_false', beq_iff_eq, decide_eq_decide]

Premises used: Bool.not_eq_false', beq_iff_eq, Nat.testBit_zero, decide_eq_decide, decide_not, Nat.mod_two_eq_zero_iff_testBit_zero, Bool.decide_iff_dist, Nat.xor_mod_two_eq_one
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m n : ℕ
h : (m + n) % 2 = 0
⊢ m % 2 = 1 ↔ n % 2 = 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m + n) % 2 = 1

Tactic:
simp only [mod_two_ne_zero] at h

Premises used: Nat.mod_two_ne_zero
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m n : ℕ
h : (m + n) % 2 = 1
neg : ¬(m % 2 = 1 ↔ n % 2 = 1)
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
simp only [h, xor_mod_two_eq_one]

Premises used: Nat.xor_mod_two_eq_one
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m n : ℕ
h : (m + n) % 2 = 1
⊢ ¬(m % 2 = 1 ↔ n % 2 = 1)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m n : ℕ
simp : (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0)
⊢ Even (m ^^^ n) ↔ (Even m ↔ Even n)

Tactic:
simp only [even_iff, xor_mod_two_eq]

Premises used: Nat.xor_mod_two_eq, Nat.even_iff
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
m n : ℕ
⊢ (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
h : Even (α := ℕ) 0
⊢ HXor.hXor (α := ℕ) 0 1 = HAdd.hAdd (α := ℕ) 0 1

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
h : Even (n + 1)
⊢ n + 1 ^^^ 1 = n + 1 + 1

Tactic:
simp +instances [HXor.hXor, instXorOp, xor, bitwise, even_iff.mp h, ← mul_two,
      div_two_mul_two_of_even h]

Premises used: Nat.instXorOp, Nat.div_two_mul_two_of_even, Nat.bitwise, HXor.hXor, Nat.xor, Iff.mp, Nat.even_iff, mul_two
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
n : ℕ
h : Even n
zero : ∀ (h : Even (α := ℕ) 0), HXor.hXor (α := ℕ) 0 1 = HAdd.hAdd (α := ℕ) 0 1
succ : ∀ (n : ℕ) (h : Even (n + 1)), n + 1 ^^^ 1 = n + 1 + 1
⊢ n ^^^ 1 = n + 1

Tactic:
cases n with
  | zero => rfl
  | succ n =>
    simp +instances [HXor.hXor, instXorOp, xor, bitwise, even_iff.mp h, ← mul_two,
      div_two_mul_two_of_even h]

Premises used: Nat.instXorOp, Nat.div_two_mul_two_of_even, Nat.bitwise, HXor.hXor, Nat.xor, Iff.mp, Nat.zero, Nat.even_iff, Nat.succ, mul_two
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
h : Odd (α := ℕ) 0
⊢ HXor.hXor (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1

Tactic:
not_odd_zero h |>.elim

Premises used: False.elim, Nat.not_odd_zero