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

State before:
f : Bool → Bool → Bool
x y : Nat
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
if x = 0 then
  have : 2 * x = 0 := by simp [*]
  simp [*]; cases (f false true) <;> simp [*]
else
  have hx : 2 * x ≠ 0 := by intro h; simp [Nat.mul_eq_zero] at h; contradiction
  simp [pos_bitwise_pos _ hx]
State after:
no goals

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
have : 2 * x = 0 := by simp [*]
State after:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
this : 2 * x = 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
this : 2 * x = 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
simp [*]
State after:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
this : 2 * x = 0
⊢ (bif f false true then 2 * y + 1 else 0) = (2 * bif f false true then y else 0) + bif f false true then 1 else 0

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
this : 2 * x = 0
⊢ (bif f false true then 2 * y + 1 else 0) = (2 * bif f false true then y else 0) + bif f false true then 1 else 0
Tactic:
cases (f false true) <;> simp [*]
State after:
no goals

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : x = 0
⊢ 2 * x = 0
Tactic:
simp [*]
State after:
no goals

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
have hx : 2 * x ≠ 0 := by intro h; simp [Nat.mul_eq_zero] at h; contradiction
State after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
hx : 2 * x ≠ 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
hx : 2 * x ≠ 0
⊢ bitwise f (2 * x) (2 * y + 1) = 2 * bitwise f x y + bif f false true then 1 else 0
Tactic:
simp [pos_bitwise_pos _ hx]
State after:
no goals

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
⊢ 2 * x ≠ 0
Tactic:
intro h
State after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
h : 2 * x = 0
⊢ False

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
h : 2 * x = 0
⊢ False
Tactic:
simp [Nat.mul_eq_zero] at h
State after:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
h : x = 0
⊢ False

State before:
f : Bool → Bool → Bool
x y : Nat
h✝ : ¬x = 0
h : x = 0
⊢ False
Tactic:
contradiction
State after:
no goals