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

State before:
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ bitwise f m n <<< k = bitwise f (m <<< k) (n <<< k)
Tactic:
apply bitext
State after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k : Nat
⊢ ∀ (i : Nat), getBit (bitwise f m n <<< k) i = getBit (bitwise f (m <<< k) (n <<< k)) i

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

State before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ getBit (bitwise f m n <<< k) i = getBit (bitwise f (m <<< k) (n <<< k)) i
Tactic:
simp only [shiftLeft_getBit, bitwise_getBit f f_stable]
State after:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ (decide (i ≥ k) && f (getBit m (i - k)) (getBit n (i - k))) =
    f (decide (i ≥ k) && getBit m (i - k)) (decide (i ≥ k) && getBit n (i - k))

State before:
case a
f : Bool → Bool → Bool
f_stable : f false false = false
m n k i : Nat
⊢ (decide (i ≥ k) && f (getBit m (i - k)) (getBit n (i - k))) =
    f (decide (i ≥ k) && getBit m (i - k)) (decide (i ≥ k) && getBit n (i - k))
Tactic:
cases decide (i ≥ k) <;> simp [f_stable]
State after:
no goals