Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : f false true = true
h✝ : f false false = true
⊢ 2 * n = 2 * bitwise f m n + 1

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : f false true = true
h✝ : ¬f false false = true
⊢ 2 * n = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : ¬f false true = true
h✝ : f false false = true
⊢ False

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : ¬f false true = true
h✝ : ¬f false false = true
⊢ 0 = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : f true false = true
h✝ : f false false = true
⊢ 2 * m = 2 * bitwise f m n + 1

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : f true false = true
h✝ : ¬f false false = true
⊢ 2 * m = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : ¬f true false = true
h✝ : f false false = true
⊢ False

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : ¬f true false = true
h✝ : ¬f false false = true
⊢ 0 = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : ¬m = 0
h✝¹ : ¬n = 0
h✝ : f false false = true
⊢ bitwise f m n + bitwise f m n + 1 = 2 * bitwise f m n + 1

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : ¬m = 0
h✝¹ : ¬n = 0
h✝ : ¬f false false = true
⊢ bitwise f m n + bitwise f m n = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : m = 0
h✝ : f false true = true
⊢ 2 * n + 1 = 2 * bitwise f m n + 1

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : m = 0
h✝ : ¬f false true = true
⊢ 0 = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬m = 0
h✝ : 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

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬m = 0
h✝ : ¬f false true = true
⊢ bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : n = 0
h✝ : f true false = true
⊢ 2 * m + 1 = 2 * bitwise f m n + 1

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : n = 0
h✝ : ¬f true false = true
⊢ 0 = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬n = 0
h✝ : 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

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬n = 0
h✝ : ¬f true false = true
⊢ bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n = 2 * bitwise f m n

pp: case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝ : 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

pp: case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝ : ¬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:
<;>

Goal state after:
case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : f false true = true
h✝ : f false false = true
⊢ 2 * n = 2 * bitwise f m n + 1

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : f false true = true
h✝ : ¬f false false = true
⊢ 2 * n = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : ¬f false true = true
h✝ : f false false = true
⊢ False

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : m = 0
h✝¹ : ¬f false true = true
h✝ : ¬f false false = true
⊢ 0 = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : f true false = true
h✝ : f false false = true
⊢ 2 * m = 2 * bitwise f m n + 1

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : f true false = true
h✝ : ¬f false false = true
⊢ 2 * m = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : ¬f true false = true
h✝ : f false false = true
⊢ False

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝³ : ¬m = 0
h✝² : n = 0
h✝¹ : ¬f true false = true
h✝ : ¬f false false = true
⊢ 0 = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : ¬m = 0
h✝¹ : ¬n = 0
h✝ : f false false = true
⊢ bitwise f m n + bitwise f m n + 1 = 2 * bitwise f m n + 1

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝² : ¬m = 0
h✝¹ : ¬n = 0
h✝ : ¬f false false = true
⊢ bitwise f m n + bitwise f m n = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : m = 0
h✝ : f false true = true
⊢ 2 * n + 1 = 2 * bitwise f m n + 1

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : m = 0
h✝ : ¬f false true = true
⊢ 0 = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬m = 0
h✝ : 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

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬m = 0
h✝ : ¬f false true = true
⊢ bitwise f m ((2 * n + 1) / 2) + bitwise f m ((2 * n + 1) / 2) = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : n = 0
h✝ : f true false = true
⊢ 2 * m + 1 = 2 * bitwise f m n + 1

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : n = 0
h✝ : ¬f true false = true
⊢ 0 = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬n = 0
h✝ : 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

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝¹ : ¬n = 0
h✝ : ¬f true false = true
⊢ bitwise f ((2 * m + 1) / 2) n + bitwise f ((2 * m + 1) / 2) n = 2 * bitwise f m n

case pos
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝ : 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

case neg
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
h4 : ∀ (x : ℕ), (x + x + 1) / 2 = x
h✝ : ¬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