Theorem: Nat.bitwise_flip (Extra/Nat/Bitwise.lean)

State before:
f : Bool → Bool → Bool
x y : Nat
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
if x = 0 then
  simp [*, flip]
else if y = 0 then
  simp [*, flip]
else
  simp [*, pos_bitwise_pos, flip, bitwise_flip f (x / 2) (y / 2)]
State after:
no goals

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
simp [*, flip]
State after:
no goals

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
if y = 0 then
simp [*, flip]
else
simp [*, pos_bitwise_pos, flip, bitwise_flip f (x / 2) (y / 2)]
State after:
no goals

State before:
f : Bool → Bool → Bool
x y : Nat
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
simp [*, flip]
State after:
no goals

State before:
f : Bool → Bool → Bool
x y : Nat
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ bitwise f x y = bitwise (flip f) y x
Tactic:
simp [*, pos_bitwise_pos, flip, bitwise_flip f (x / 2) (y / 2)]
State after:
no goals