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

State before:
n k i : Nat
⊢ getBit (n >>> k) i = getBit n (i + k)
Tactic:
induction k generalizing n i
State after:
case zero
n i : Nat
⊢ getBit (n >>> zero) i = getBit n (i + zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (n i : Nat), getBit (n >>> n✝) i = getBit n (i + n✝)
n i : Nat
⊢ getBit (n >>> succ n✝) i = getBit n (i + succ n✝)

State before:
n i : Nat
⊢ getBit (n >>> zero) i = getBit n (i + zero)
Tactic:
case zero => rfl
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n i : Nat), getBit (n >>> k) i = getBit n (i + k)
n i : Nat
⊢ getBit (n >>> succ k) i = getBit n (i + succ k)
Tactic:
case succ k h_ind =>
  conv =>
    lhs; rw [Nat.succ_eq_add_one, Nat.add_comm, ←Nat.shiftRight_shiftRight]
    rw [h_ind]
State after:
no goals

State before:
n i : Nat
⊢ getBit (n >>> zero) i = getBit n (i + zero)
Tactic:
rfl
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n i : Nat), getBit (n >>> k) i = getBit n (i + k)
n i : Nat
⊢ getBit (n >>> succ k) i = getBit n (i + succ k)
Tactic:
conv =>
  lhs; rw [Nat.succ_eq_add_one, Nat.add_comm, ←Nat.shiftRight_shiftRight]
  rw [h_ind]
State after:
no goals