awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
a b c : ℕ
h : a ^^^ b ^^^ c ≠ 0
h₁ :
  let v := a ^^^ b ^^^ c;
  v ≠ 0
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have hv : let v := a ^^^ b ^^^ c;
v = a ^^^ b ^^^ c
Tactic: set v := a ^^^ b ^^^ c with hv
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
⊢ a ^^^ b = c ^^^ v
have rw : a ^^^ b = v ^^^ c
Tactic: rw [Nat.xor_comm c, Nat.xor_xor_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
rw : a ^^^ b = v ^^^ c
⊢ a ^^^ b = c ^^^ v
have rw₁ : a ^^^ b = a ^^^ b
Tactic: rw [Nat.xor_comm c, Nat.xor_xor_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have hab : a ^^^ b = c ^^^ v
Tactic: have hab : a ^^^ b = c ^^^ v := by
    rw [Nat.xor_comm c, Nat.xor_xor_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
have rw : b ^^^ c = a ^^^ (a ^^^ b) ^^^ c
Tactic: rw [← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c = a ^^^ v
have rw₁ : b ^^^ c = b ^^^ c
Tactic: rw [← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
a b c : ℕ
v : ℕ := a ^^^ b ^^^ c
h : v ≠ 0
hv : v = a ^^^ b ^^^ c
hab : a ^^^ b = c ^^^ v
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have hbc : b ^^^ c = a ^^^ v
Tactic: have hbc : b ^^^ c = a ^^^ v := by
    rw [← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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)
⊢ c ^^^ a = b ^^^ v
have rw₁ : c ^^^ a = b ^^^ (a ^^^ (b ^^^ c))
Tactic: rw [hv, Nat.xor_assoc, Nat.xor_comm a, ← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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))
⊢ c ^^^ a = b ^^^ v
have rw₂ : c ^^^ a = b ^^^ (b ^^^ c ^^^ a)
Tactic: rw [hv, Nat.xor_assoc, Nat.xor_comm a, ← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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)
⊢ c ^^^ a = b ^^^ v
have rw₃ : c ^^^ a = b ^^^ (b ^^^ c) ^^^ a
Tactic: rw [hv, Nat.xor_assoc, Nat.xor_comm a, ← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ c ^^^ a = b ^^^ v
have rw₄ : c ^^^ a = c ^^^ a
Tactic: rw [hv, Nat.xor_assoc, Nat.xor_comm a, ← Nat.xor_assoc, Nat.xor_xor_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have hca : 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have obtain : ∀ (i : ℕ) (hi : v.testBit i = true) (hi' : ∀ (j : ℕ), i < j → v.testBit j = false),
  b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
Tactic: obtain ⟨i, ⟨hi, hi'⟩⟩ := exists_most_significant_bit h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
have contrapose! : ∀ (hi : a.testBit i ≠ true ∧ b.testBit i ≠ true ∧ c.testBit i ≠ true), v.testBit i ≠ true
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ v.testBit i ≠ true
have simp_rw : ∀ (hi : a.testBit i = false ∧ b.testBit i = false ∧ c.testBit i = false), v.testBit i = false
Tactic: simp_rw [Bool.eq_false_eq_not_eq_true] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ v.testBit i = false
have rw : (false ^^ false ^^ false) = false
Tactic: rw [testBit_xor, testBit_xor, hi.1, hi.2.1, hi.2.2]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have this : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inl : ∀ (h : a.testBit i = true), b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
Tactic: obtain h | h | h := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inr : ∀ (h : b.testBit i = true), b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
Tactic: obtain h | h | h := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inr₁ : ∀ (h : c.testBit i = true), b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
Tactic: obtain h | h | h := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inl : b ^^^ c < a
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a
have inl : a ^^^ v < a
Tactic: rw [hbc]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inl : a ^^^ v < a
Tactic: on_goal 1 => left; rw [hbc]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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 ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inr : c ^^^ a < b ∨ a ^^^ b < c
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ c ^^^ a < b ∨ a ^^^ b < c
have inr : c ^^^ a < b
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ c ^^^ a < b
have inr : b ^^^ v < b
Tactic: rw [hca]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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 ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inr : b ^^^ v < b
Tactic: on_goal 2 => right; left; rw [hca]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inr : c ^^^ a < b ∨ a ^^^ b < c
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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 ^^^ a < b ∨ a ^^^ b < c
have inr : a ^^^ b < c
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ a ^^^ b < c
have inr : c ^^^ v < c
Tactic: rw [hab]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c
have inr : c ^^^ v < c
Tactic: on_goal 3 => right; right; rw [hab]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
have inl : (a ^^^ v).testBit i = false
Tactic: refine lt_of_testBit i ?_ h fun j hj => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ a ^^^ v < a
have inl₁ : ∀ (j : ℕ) (hj : i < j), (a ^^^ v).testBit j = a.testBit j
Tactic: refine lt_of_testBit i ?_ h fun j hj => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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).testBit i = false
have inl : (true ^^ true) = false
Tactic: rw [testBit_xor, h, hi]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
have inr : (b ^^^ v).testBit i = false
Tactic: refine lt_of_testBit i ?_ h fun j hj => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ b ^^^ v < b
have inr₁ : ∀ (j : ℕ) (hj : i < j), (b ^^^ v).testBit j = b.testBit j
Tactic: refine lt_of_testBit i ?_ h fun j hj => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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).testBit i = false
have inr : (true ^^ true) = false
Tactic: rw [testBit_xor, h, hi]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
have inr : (c ^^^ v).testBit i = false
Tactic: refine lt_of_testBit i ?_ h fun j hj => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ c ^^^ v < c
have inr₁ : ∀ (j : ℕ) (hj : i < j), (c ^^^ v).testBit j = c.testBit j
Tactic: refine lt_of_testBit i ?_ h fun j hj => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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).testBit i = false
have inr : (true ^^ true) = false
Tactic: rw [testBit_xor, h, hi]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
a b c : ℕ
h : a < b ^^^ c
⊢ a ^^^ c < b ∨ a ^^^ b < c
have inl : ∀ (ha : b ^^^ c < a), a ^^^ c < b ∨ a ^^^ b < c
Tactic: obtain ha | hb | hc := xor_trichotomy <| Nat.xor_assoc _ _ _ ▸ xor_ne_zero_iff.2 h.ne
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
a b c : ℕ
h : a < b ^^^ c
inl : ∀ (ha : b ^^^ c < a), a ^^^ c < b ∨ a ^^^ b < c
⊢ a ^^^ c < b ∨ a ^^^ b < c
have inr : ∀ (hb : c ^^^ a < b), a ^^^ c < b ∨ a ^^^ b < c
Tactic: obtain ha | hb | hc := xor_trichotomy <| Nat.xor_assoc _ _ _ ▸ xor_ne_zero_iff.2 h.ne
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ a ^^^ c < b ∨ a ^^^ b < c
have inr₁ : ∀ (hc : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
m n : ℕ
⊢ (m ^^^ n) % 2 = (m + n) % 2
have pos : ∀ (h : (m + n) % 2 = 0), (m ^^^ n) % 2 = (m + n) % 2
Tactic: by_cases h : (m + n) % 2 = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
m n : ℕ
pos : ∀ (h : (m + n) % 2 = 0), (m ^^^ n) % 2 = (m + n) % 2
⊢ (m ^^^ n) % 2 = (m + n) % 2
have neg : ∀ (h : ¬(m + n) % 2 = 0), (m ^^^ n) % 2 = (m + n) % 2
Tactic: by_cases h : (m + n) % 2 = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
m n : ℕ
h : (m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2
have pos : m % 2 = 1 ↔ n % 2 = 1
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (hypothesis)
Goal:
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2
have h₁ : (m + n) % 2 = 1
Tactic: simp only [mod_two_ne_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
m n : ℕ
h : (m + n) % 2 = 1
⊢ (m ^^^ n) % 2 = (m + n) % 2
have neg : ¬(m % 2 = 1 ↔ n % 2 = 1)
Tactic: simp only [h, xor_mod_two_eq_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
m n : ℕ
⊢ Even (m ^^^ n) ↔ (Even m ↔ Even n)
have simp : (m + n) % 2 = 0 ↔ (m % 2 = 0 ↔ n % 2 = 0)
Tactic: simp only [even_iff, xor_mod_two_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
h : Even n
⊢ n ^^^ 1 = n + 1
have zero : ∀ (h : Even (α := ℕ) 0), HXor.hXor (α := ℕ) 0 1 = HAdd.hAdd (α := ℕ) 0 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]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
h : Even n
zero : ∀ (h : Even (α := ℕ) 0), HXor.hXor (α := ℕ) 0 1 = HAdd.hAdd (α := ℕ) 0 1
⊢ n ^^^ 1 = n + 1
have succ : ∀ (n : ℕ) (h : Even (n + 1)), n + 1 ^^^ 1 = n + 1 + 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]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
h : Odd (n + 1)
⊢ n + 1 ^^^ 1 = n + 1 - 1
have succ : (if n + 1 = 0 then if (false != true) = true then 1 else 0
  else
    if Eq (α := ℕ) 1 0 then if (true != false) = true then n + 1 else 0
    else
      if (decide ((n + 1) % 2 = 1) != decide True) = true then
        ((if (true != false) = true then (n + 1) / 2 else 0) + if (true != false) = true then (n + 1) / 2 else 0) + 1
      else (if (true != false) = true then (n + 1) / 2 else 0) + if (true != false) = true then (n + 1) / 2 else 0) =
  n + 1 - 1
Tactic: simp +instances only [HXor.hXor, instXorOp, xor, bitwise, reduceDiv, bitwise_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
h : Odd n
⊢ n ^^^ 1 = n - 1
have zero : ∀ (h : Odd (α := ℕ) 0), HXor.hXor (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
Tactic: cases n with
  | zero =>
    exact not_odd_zero h |>.elim
  | succ n =>
    simp +instances only [HXor.hXor, instXorOp, xor, bitwise, reduceDiv, bitwise_zero_right]
    grind
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
h : Odd n
zero : ∀ (h : Odd (α := ℕ) 0), HXor.hXor (α := ℕ) 0 1 = HSub.hSub (α := ℕ) 0 1
⊢ n ^^^ 1 = n - 1
have succ : ∀ (n : ℕ) (h : Odd (n + 1)), n + 1 ^^^ 1 = n + 1 - 1
Tactic: cases n with
  | zero =>
    exact not_odd_zero h |>.elim
  | succ n =>
    simp +instances only [HXor.hXor, instXorOp, xor, bitwise, reduceDiv, bitwise_zero_right]
    grind
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
ih :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
⊢ Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 (n + 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0)
have succ : Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)))
  (match (motive := Fin 4 → ℕ) Fin.ofNat 4 (n + (↑(Fin.ofNat 4 1) : ℕ)) with
  | 0 => n + 1
  | 1 => 1
  | 2 => n + 1 + 1
  | 3 => 0)
Tactic: nth_rw 3 [← show Fin.ofNat 4 1 = (1 : ℕ) from Fin.val_ofNat ..]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
ih :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
⊢ Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1 + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 (n + (↑(Fin.ofNat 4 1) : ℕ)) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0)
have succ : (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0) ^^^
    n + 1 =
  match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) (Fin.ofNat 4 n) (Fin.ofNat 4 1) with
  | 0 => n + 1
  | 1 => 1
  | 2 => n + 1 + 1
  | 3 => 0
Tactic: rw [List.range_succ, List.foldl_append, ih, ← Fin.ofNat_add, List.foldl_cons, List.foldl_nil]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
ih :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
h : Eq (α := Fin 4) (Fin.ofNat 4 n) 0
⊢ (match (motive := Fin 4 → ℕ) 0 with
      | 0 => n
      | 1 => 1
      | 2 => n + 1
      | 3 => 0) ^^^
      n + 1 =
    match (motive := Fin 4 → ℕ) HAdd.hAdd (α := Fin 4) 0 (Fin.ofNat 4 1) with
    | 0 => n + 1
    | 1 => 1
    | 2 => n + 1 + 1
    | 3 => 0
have rw : n % 2 = 0
Tactic: rw [Fin.zero_add, ← xor_one_of_even <| even_iff.mpr ?_, xor_xor_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
n : ℕ
ih :
  Eq (α := ℕ) (List.foldl (fun (x1 x2 : ℕ) ↦ x1 ^^^ x2) 0 (List.range (n + 1)))
    (match (motive := Fin 4 → ℕ) Fin.ofNat 4 n with
    | 0 => n
    | 1 => 1
    | 2 => n + 1
    | 3 => 0)
h : Eq (α := Fin 4) (Fin.ofNat 4 n) 0
⊢ n % 2 = 0
have rw : (↑0 : ℕ) % 2 = 0
Tactic: rw [← @mod_mod_of_dvd _ 4 _ <| by simp, ← Fin.val_ofNat 4, h]