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

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

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

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

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

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

State before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
h : x = 0
⊢ False
Tactic:
contradiction
State after:
no goals

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

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

State before:
x y : Nat
f : Bool → Bool → Bool
hx : x ≠ 0
hy : y ≠ 0
hx2 : 2 * x ≠ 0
h : y = 0
⊢ False
Tactic:
contradiction
State after:
no goals