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

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

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

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