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

State before:
n k i : Nat
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
cases Nat.lt_or_ge i k
State after:
case inl
n k i : Nat
h✝ : i < k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))

case inr
n k i : Nat
h✝ : i ≥ k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))

State before:
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
case inl hlt =>
  rw [decide_eq_false (Nat.not_le_of_gt hlt), Bool.false_and]
  exact shiftLeft_getBit_lt n k hlt
State after:
no goals

State before:
n k i : Nat
hge : i ≥ k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
case inr hge =>
  rw [decide_eq_true hge, Bool.true_and]
  exact shiftLeft_getBit_ge n k hge
State after:
no goals

State before:
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
rw [decide_eq_false (Nat.not_le_of_gt hlt), Bool.false_and]
State after:
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = false

State before:
n k i : Nat
hlt : i < k
⊢ getBit (n <<< k) i = false
Tactic:
exact shiftLeft_getBit_lt n k hlt
State after:
no goals

State before:
n k i : Nat
hge : i ≥ k
⊢ getBit (n <<< k) i = (decide (i ≥ k) && getBit n (i - k))
Tactic:
rw [decide_eq_true hge, Bool.true_and]
State after:
n k i : Nat
hge : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)

State before:
n k i : Nat
hge : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)
Tactic:
exact shiftLeft_getBit_ge n k hge
State after:
no goals