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

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

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

case succ
n✝ : Nat
n_ih✝ : ∀ (n k : Nat), n✝ < k → getBit (n <<< k) n✝ = false
n k : Nat
h : succ n✝ < k
⊢ getBit (n <<< k) (succ n✝) = false

State before:
n k : Nat
h : zero < k
⊢ getBit (n <<< k) zero = false
Tactic:
case zero =>
  have : k.pred.succ = k := Nat.succ_pred_eq_of_pos h
  rw [←this, Nat.shiftLeft_succ]
  conv => lhs; change decide ((2*n <<< k.pred) % 2 = 1); simp
State after:
no goals

State before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
⊢ getBit (n <<< k) (succ i) = false
Tactic:
case succ i h_ind =>
  have : k.pred.succ = k := Nat.succ_pred_eq_of_pos (trans i.zero_lt_succ h)
  rw [←this, Nat.shiftLeft_succ]
  conv =>
    lhs; change getBit ((2 * n <<< k.pred) / 2) i
    rw [Nat.mul_div_cancel_left _ (Nat.zero_lt_succ 1)]
  apply h_ind
  exact Nat.lt_of_succ_lt_succ (trans h this.symm)
State after:
no goals

State before:
n k : Nat
h : zero < k
⊢ getBit (n <<< k) zero = false
Tactic:
have : k.pred.succ = k := Nat.succ_pred_eq_of_pos h
State after:
n k : Nat
h : zero < k
this : succ (pred k) = k
⊢ getBit (n <<< k) zero = false

State before:
n k : Nat
h : zero < k
this : succ (pred k) = k
⊢ getBit (n <<< k) zero = false
Tactic:
rw [←this, Nat.shiftLeft_succ]
State after:
n k : Nat
h : zero < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) zero = false

State before:
n k : Nat
h : zero < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) zero = false
Tactic:
conv => lhs; change decide ((2*n <<< k.pred) % 2 = 1); simp
State after:
no goals

State before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
⊢ getBit (n <<< k) (succ i) = false
Tactic:
have : k.pred.succ = k := Nat.succ_pred_eq_of_pos (trans i.zero_lt_succ h)
State after:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< k) (succ i) = false

State before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< k) (succ i) = false
Tactic:
rw [←this, Nat.shiftLeft_succ]
State after:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) (succ i) = false

State before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (2 * n <<< pred k) (succ i) = false
Tactic:
conv =>
  lhs; change getBit ((2 * n <<< k.pred) / 2) i
  rw [Nat.mul_div_cancel_left _ (Nat.zero_lt_succ 1)]
State after:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< pred k) i = false

State before:
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< pred k) i = false
Tactic:
apply h_ind
State after:
case h
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ i < pred k

State before:
case h
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ i < pred k
Tactic:
exact Nat.lt_of_succ_lt_succ (trans h this.symm)
State after:
no goals