Theorem: Nat.bitwise_nilpotent (Algdata/Data/Nat/Bits.lean)

State before:
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n : Nat
⊢ bitwise f n n = 0
Tactic:
apply Nat.bitext
State after:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f n n) i = getBit 0 i

State before:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n : Nat
⊢ ∀ (i : Nat), getBit (bitwise f n n) i = getBit 0 i
Tactic:
intro i
State after:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n i : Nat
⊢ getBit (bitwise f n n) i = getBit 0 i

State before:
case a
f : Bool → Bool → Bool
h : ∀ (b : Bool), f b b = false
n i : Nat
⊢ getBit (bitwise f n n) i = getBit 0 i
Tactic:
simp [Nat.bitwise_getBit f (h false), h]
State after:
no goals