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

State before:
n k i : Nat
⊢ i ≥ k → getBit (n <<< k) i = getBit n (i - k)
Tactic:
intro h
State after:
n k i : Nat
h : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)

State before:
n k i : Nat
h : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)
Tactic:
induction k generalizing n i
State after:
case zero
n i : Nat
h : i ≥ zero
⊢ getBit (n <<< zero) i = getBit n (i - zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (n : Nat) {i : Nat}, i ≥ n✝ → getBit (n <<< n✝) i = getBit n (i - n✝)
n i : Nat
h : i ≥ succ n✝
⊢ getBit (n <<< succ n✝) i = getBit n (i - succ n✝)

State before:
n i : Nat
h : i ≥ zero
⊢ getBit (n <<< zero) i = getBit n (i - zero)
Tactic:
case zero => rfl
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
Tactic:
case succ k h_ind =>
  have : i-k = (i-k.succ).succ := by
    rw [Nat.sub_succ i k]
    apply (Nat.succ_pred_eq_of_pos ?_).symm
    exact Nat.zero_lt_sub_of_lt h
  conv =>
    lhs; change (n <<< (k+1)).getBit i
    rw [Nat.add_comm, ←Nat.shiftLeft_shiftLeft]
    rw [h_ind (n <<< 1) (Nat.le_of_succ_le h), this]
    change ((2*n)/2).getBit (i-k.succ)
    simp
State after:
no goals

State before:
n i : Nat
h : i ≥ zero
⊢ getBit (n <<< zero) i = getBit n (i - zero)
Tactic:
rfl
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
Tactic:
have : i-k = (i-k.succ).succ := by
  rw [Nat.sub_succ i k]
  apply (Nat.succ_pred_eq_of_pos ?_).symm
  exact Nat.zero_lt_sub_of_lt h
State after:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
this : i - k = succ (i - succ k)
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)

State before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
this : i - k = succ (i - succ k)
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
Tactic:
conv =>
  lhs; change (n <<< (k+1)).getBit i
  rw [Nat.add_comm, ←Nat.shiftLeft_shiftLeft]
  rw [h_ind (n <<< 1) (Nat.le_of_succ_le h), this]
  change ((2*n)/2).getBit (i-k.succ)
  simp
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ i - k = succ (i - succ k)
Tactic:
rw [Nat.sub_succ i k]
State after:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ i - k = succ (pred (i - k))

State before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ i - k = succ (pred (i - k))
Tactic:
apply (Nat.succ_pred_eq_of_pos ?_).symm
State after:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ 0 < i - k

State before:
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ 0 < i - k
Tactic:
exact Nat.zero_lt_sub_of_lt h
State after:
no goals