awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ ∀ (x : ℕ), (x + x + 1) / 2 = x

Tactic:
have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left]
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f Bool.false Bool.false = Bool.false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
false :
  (if m = 0 then if f Bool.false true = true then 2 * n else 0
    else
      if n = 0 then if f true Bool.false = true then 2 * m else 0
      else
        if f Bool.false Bool.false = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    if f Bool.false Bool.false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
⊢ (if (if Bool.false = true then 2 * m + 1 else 2 * m) = 0 then
      if f Bool.false true = true then if Bool.false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if Bool.false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true Bool.false = true then if Bool.false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if Bool.false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if Bool.false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if Bool.false = true then 2 * m + 1 else 2 * m) / 2)
                ((if Bool.false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if Bool.false = true then 2 * m + 1 else 2 * m) / 2)
                ((if Bool.false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if Bool.false = true then 2 * m + 1 else 2 * m) / 2)
              ((if Bool.false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if Bool.false = true then 2 * m + 1 else 2 * m) / 2)
              ((if Bool.false = true then 2 * n + 1 else 2 * n) / 2)) =
    if f Bool.false Bool.false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f Bool.false Bool.false = Bool.false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
false :
  (if m = 0 then if f Bool.false true = true then 2 * n + 1 else 0
    else
      if f Bool.false true = true then bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1
      else bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2)) =
    if f Bool.false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
⊢ (if (if Bool.false = true then 2 * m + 1 else 2 * m) = 0 then
      if f Bool.false true = true then if true = true then 2 * n + 1 else 2 * n else 0
    else
      if (if true = true then 2 * n + 1 else 2 * n) = 0 then
        if f true Bool.false = true then if Bool.false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if Bool.false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if true = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if Bool.false = true then 2 * m + 1 else 2 * m) / 2)
                ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if Bool.false = true then 2 * m + 1 else 2 * m) / 2)
                ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if Bool.false = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if Bool.false = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 2)) =
    if f Bool.false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
true :
  (if n = 0 then if f Bool.true false = Bool.true then 2 * m + 1 else 0
    else
      if f Bool.true false = Bool.true then bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1
      else bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n) =
    if f Bool.true false = Bool.true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
⊢ (if (if Bool.true = Bool.true then 2 * m + 1 else 2 * m) = 0 then
      if f false Bool.true = Bool.true then if false = Bool.true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = Bool.true then 2 * n + 1 else 2 * n) = 0 then
        if f Bool.true false = Bool.true then if Bool.true = Bool.true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = Bool.true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              Bool.true then
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
                ((if false = Bool.true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
                ((if false = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if false = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if false = Bool.true then 2 * n + 1 else 2 * n) / 2)) =
    if f Bool.true false = Bool.true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
true :
  (if f Bool.true Bool.true = Bool.true then
      bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1
    else bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2)) =
    if f Bool.true Bool.true = Bool.true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
⊢ (if (if Bool.true = Bool.true then 2 * m + 1 else 2 * m) = 0 then
      if f false Bool.true = Bool.true then if Bool.true = Bool.true then 2 * n + 1 else 2 * n else 0
    else
      if (if Bool.true = Bool.true then 2 * n + 1 else 2 * n) = 0 then
        if f Bool.true false = Bool.true then if Bool.true = Bool.true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              Bool.true then
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
                ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
                ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if Bool.true = Bool.true then 2 * m + 1 else 2 * m) / 2)
              ((if Bool.true = Bool.true then 2 * n + 1 else 2 * n) / 2)) =
    if f Bool.true Bool.true = Bool.true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
pos : m = 0 → f false true = true → f false false = true → 2 * n = 2 * bitwise f m n + 1
neg : m = 0 → f false true = true → ¬f false false = true → 2 * n = 2 * bitwise f m n
pos₁ : m = 0 → ¬f false true = true → f false false = true → False
neg₁ : m = 0 → ¬f false true = true → ¬f false false = true → 0 = 2 * bitwise f m n
pos₂ : ¬m = 0 → n = 0 → f true false = true → f false false = true → 2 * m = 2 * bitwise f m n + 1
neg₂ : ¬m = 0 → n = 0 → f true false = true → ¬f false false = true → 2 * m = 2 * bitwise f m n
pos₃ : ¬m = 0 → n = 0 → ¬f true false = true → f false false = true → False
neg₃ : ¬m = 0 → n = 0 → ¬f true false = true → ¬f false false = true → 0 = 2 * bitwise f m n
pos₄ : ¬m = 0 → ¬n = 0 → f false false = true → bitwise f m n + bitwise f m n + 1 = 2 * bitwise f m n + 1
neg₄ : ¬m = 0 → ¬n = 0 → ¬f false false = true → bitwise f m n + bitwise f m n = 2 * bitwise f m n
⊢ (if m = 0 then if f false true = true then 2 * n else 0
    else
      if n = 0 then if f true false = true then 2 * m else 0
      else if f false false = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    if f false false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
pos : m = 0 → f false true = true → 2 * n + 1 = 2 * bitwise f m n + 1
neg : m = 0 → ¬f false true = true → 0 = 2 * bitwise f m n
pos₁ :
  ¬m = 0 →
    f false true = true → bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1 = 2 * bitwise f m n + 1
neg₁ : ¬m = 0 → ¬f false true = true → bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) = 2 * bitwise f m n
⊢ (if m = 0 then if f false true = true then 2 * n + 1 else 0
    else
      if f false true = true then bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1
      else bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2)) =
    if f false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
pos : n = 0 → f true false = true → 2 * m + 1 = 2 * bitwise f m n + 1
neg : n = 0 → ¬f true false = true → 0 = 2 * bitwise f m n
pos₁ :
  ¬n = 0 →
    f true false = true → bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1 = 2 * bitwise f m n + 1
neg₁ : ¬n = 0 → ¬f true false = true → bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n = 2 * bitwise f m n
⊢ (if n = 0 then if f true false = true then 2 * m + 1 else 0
    else
      if f true false = true then bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1
      else bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n) =
    if f true false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
pos :
  f true true = true →
    bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1 =
      2 * bitwise f m n + 1
neg :
  ¬f true true = true →
    bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) = 2 * bitwise f m n
⊢ (if f true true = true then
      bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1
    else bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : m = 0
h_2 : f false true = true
h_3 : f false false = true
⊢ 2 * n = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : m = 0
h_2 : f false true = true
h_3 : ¬f false false = true
⊢ 2 * n = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : m = 0
h_2 : ¬f false true = true
h_3 : f false false = true
⊢ False

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : m = 0
h_2 : ¬f false true = true
h_3 : ¬f false false = true
⊢ 0 = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬m = 0
h_2 : n = 0
h_3 : f true false = true
h_4 : f false false = true
⊢ 2 * m = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬m = 0
h_2 : n = 0
h_3 : f true false = true
h_4 : ¬f false false = true
⊢ 2 * m = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬m = 0
h_2 : n = 0
h_3 : ¬f true false = true
h_4 : f false false = true
⊢ False

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬m = 0
h_2 : n = 0
h_3 : ¬f true false = true
h_4 : ¬f false false = true
⊢ 0 = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬m = 0
h_2 : ¬n = 0
h_3 : f false false = true
⊢ bitwise f m n + bitwise f m n + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬m = 0
h_2 : ¬n = 0
h_3 : ¬f false false = true
⊢ bitwise f m n + bitwise f m n = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : m = 0
h_2 : f false true = true
⊢ 2 * n + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : m = 0
h_2 : ¬f false true = true
⊢ 0 = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬m = 0
h_2 : f false true = true
⊢ bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬m = 0
h_2 : ¬f false true = true
⊢ bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : n = 0
h_2 : f true false = true
⊢ 2 * m + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : n = 0
h_2 : ¬f true false = true
⊢ 0 = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬n = 0
h_2 : f true false = true
⊢ bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n + 1 = 2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬n = 0
h_2 : ¬f true false = true
⊢ bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : f true true = true
⊢ bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + 1 =
    2 * bitwise f m n + 1

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h_1 : ¬f true true = true
⊢ bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) + bitwise f ((2 * m + 1) / 2) ((2 * n + 1) / 2) = 2 * bitwise f m n

Tactic:
simp_all +decide [two_mul]

Premises used: two_mul, Decidable.decide
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a : Bool
x : ℕ
⊢ bit a x % 2 = 0 ↔ (!a) = true

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
a : Bool
x : ℕ
⊢ bit a x % 2 = 1 ↔ a = true

Tactic:
simp
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
⊢ ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ), bit a m ||| bit b n = bit (a || b) (m ||| n)

Tactic:
bitwise_bit

Premises used: WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, Nat.lor, Nat.bitwise_bit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
⊢ ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ), bit a m &&& bit b n = bit (a && b) (m &&& n)

Tactic:
bitwise_bit

Premises used: WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, Nat.land, Nat.bitwise_bit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
⊢ ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ), (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
bitwise_bit

Premises used: WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, Nat.ldiff, Nat.bitwise_bit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
⊢ ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ), bit a m ^^^ bit b n = bit (a != b) (m ^^^ n)

Tactic:
bitwise_bit

Premises used: WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, Nat.xor, Nat.bitwise_bit
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
⊢ ∀ (m n k : ℕ), (m ||| n).testBit k = (m.testBit k || n.testBit k)

Tactic:
testBit_bitwise rfl

Premises used: Nat.testBit_bitwise, WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, rfl, Nat.lor
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
⊢ ∀ (m n k : ℕ), (m &&& n).testBit k = (m.testBit k && n.testBit k)

Tactic:
testBit_bitwise rfl

Premises used: Nat.testBit_bitwise, WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, Nat.land, rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
⊢ ∀ (m n k : ℕ), (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)

Tactic:
testBit_bitwise rfl

Premises used: Nat.testBit_bitwise, WellFounded.Nat.fix, Nat.bitwise._unary, WellFounded.Nat.fix.go, Nat.ldiff, rfl
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
unfold :
  if bit a m = 0 then if f false true = true then bit b n else 0
  else
    if bit b n = 0 then if f true false = true then bit a m else 0
    else
      have n' := bit a m / 2;
      have m' := bit b n / 2;
      let b₁ := bit a m % 2 = 1;
      let b₂ := bit b n % 2 = 1;
      have r := bitwise f n' m';
      if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
| bitwise f (bit a m) (bit b n)

Tactic:
unfold bitwise

Premises used: Nat.bitwise
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
conv_lhs :
  (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
conv_lhs => unfold bitwise

Premises used: Nat.bitwise
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
⊢ bit a m ≠ 0

Tactic:
rw [← bit_ne_zero_iff] at ham hbn

Premises used: Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : m = 0 → a = true
hbn : n = 0 → b = true
ham₁ : bit a m ≠ 0
⊢ bit b n ≠ 0

Tactic:
rw [← bit_ne_zero_iff] at ham hbn

Premises used: Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
simp :
  (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)

Tactic:
simp only [ham, hbn, bit_mod_two_eq_one_iff, Bool.decide_coe, ← div2_val, div2_bit,
    ite_false]

Premises used: Nat.div2_bit, ite_false, Nat.bit_mod_two_eq_one_iff, Nat.div2_val, Bool.decide_coe
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
simp : if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n
| bit (f a b) (bitwise f m n)

Tactic:
simp only [bit, two_mul, Bool.cond_eq_ite]

Premises used: Nat.bit, two_mul, Bool.cond_eq_ite
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
conv_rhs :
  (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)
conv_rhs₁ :
  (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n
⊢ (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)

Tactic:
conv_rhs => simp only [bit, two_mul, Bool.cond_eq_ite]

Premises used: Nat.bit, two_mul, Bool.cond_eq_ite
-- Module: Mathlib.Data.Nat.Bitwise
Goal:
f : Bool → Bool → Bool
h :
  ∀ (x y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
        (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
          binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
            (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
        x y
⊢ bitwise f = fun (n : ℕ) ↦
    binaryRec (motive := fun (x : ℕ) ↦ (m : ℕ) → ℕ) (fun (n : ℕ) ↦ bif f false true then n else 0)
      (fun (a : Bool) (m : ℕ) (Ia : (m : ℕ) → ℕ) (n : ℕ) ↦
        binaryRec (motive := fun (x : ℕ) ↦ ℕ) (bif f true false then bit a m else 0)
          (fun (b : Bool) (n x : ℕ) ↦ bit (f a b) (Ia n)) n)
      n

Tactic:
funext x y