awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if b = true then 2 * n + 1 else 2 * n else 0
    else
      if (if b = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if b = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if b = true then 2 * n + 1 else 2 * n) / 2)) =
    if f true b = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have true : (if (if true = true then 2 * m + 1 else 2 * m) = 0 then
    if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
  else
    if (if false = true then 2 * n + 1 else 2 * n) = 0 then
      if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
    else
      if
          f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
              (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
            true then
        bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2) +
          1
      else
        bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
            ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
  if f true false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if false = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
    if f false false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have false : (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: simp
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if false = true then 2 * m + 1 else 2 * m) = 0 then
      if f 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 false = true then if false = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if 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 false = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if 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 false = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if false = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 2)) =
    if f false true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have false : (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: simp
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f false true = true then if false = true then 2 * n + 1 else 2 * n else 0
    else
      if (if false = true then 2 * n + 1 else 2 * n) = 0 then
        if f true false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = true then 2 * m + 1 else 2 * m) % 2 = 1))
                (decide ((if false = true then 2 * n + 1 else 2 * n) % 2 = 1)) =
              true then
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
                ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            1
        else
          bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2) ((if false = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if false = true then 2 * n + 1 else 2 * n) / 2)) =
    if f true false = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have true : (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: simp
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (if (if true = true then 2 * m + 1 else 2 * m) = 0 then
      if f 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 false = true then if true = true then 2 * m + 1 else 2 * m else 0
      else
        if
            f (decide ((if true = 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 true = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
              bitwise f ((if true = 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 true = true then 2 * m + 1 else 2 * m) / 2) ((if true = true then 2 * n + 1 else 2 * n) / 2) +
            bitwise f ((if true = true then 2 * m + 1 else 2 * m) / 2)
              ((if true = true then 2 * n + 1 else 2 * n) / 2)) =
    if f true true = true then 2 * bitwise f m n + 1 else 2 * bitwise f m n
have true : (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: simp
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (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
have pos : m = 0 → f false true = true → f false false = true → 2 * n = 2 * bitwise f m n + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have neg : m = 0 → f false true = true → ¬f false false = true → 2 * n = 2 * bitwise f m n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have pos₁ : m = 0 → ¬f false true = true → f false false = true → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have neg₁ : m = 0 → ¬f false true = true → ¬f false false = true → 0 = 2 * bitwise f m n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have pos₂ : ¬m = 0 → n = 0 → f true false = true → f false false = true → 2 * m = 2 * bitwise f m n + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have neg₂ : ¬m = 0 → n = 0 → f true false = true → ¬f false false = true → 2 * m = 2 * bitwise f m n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have pos₃ : ¬m = 0 → n = 0 → ¬f true false = true → f false false = true → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have neg₃ : ¬m = 0 → n = 0 → ¬f true false = true → ¬f false false = true → 0 = 2 * bitwise f m n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have pos₄ : ¬m = 0 → ¬n = 0 → f false false = true → bitwise f m n + bitwise f m n + 1 = 2 * bitwise f m n + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have neg₄ : ¬m = 0 → ¬n = 0 → ¬f false false = true → bitwise f m n + bitwise f m n = 2 * bitwise f m n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (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
have pos : m = 0 → f false true = true → 2 * n + 1 = 2 * bitwise f m n + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have neg : m = 0 → ¬f false true = true → 0 = 2 * bitwise f m n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
Goal:
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
⊢ (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
have pos : n = 0 → f true false = true → 2 * m + 1 = 2 * bitwise f m n + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have neg : n = 0 → ¬f true false = true → 0 = 2 * bitwise f m n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Bitwise (goal)
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
⊢ (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
have 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
Tactic: split_ifs