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

State before:
n k : Nat
⊢ n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
Tactic:
intro hn i hi
State after:
n k : Nat
hn : n < 2 ^ k
i : Nat
hi : i ≥ k
⊢ getBit n i = false

State before:
n k : Nat
hn : n < 2 ^ k
i : Nat
hi : i ≥ k
⊢ getBit n i = false
Tactic:
induction k generalizing n i
State after:
case zero
n : Nat
hn : n < 2 ^ zero
i : Nat
hi : i ≥ zero
⊢ getBit n i = false

case succ
n✝ : Nat
n_ih✝ : ∀ {n : Nat}, n < 2 ^ n✝ → ∀ (i : Nat), i ≥ n✝ → getBit n i = false
n : Nat
hn : n < 2 ^ succ n✝
i : Nat
hi : i ≥ succ n✝
⊢ getBit n i = false

State before:
n : Nat
hn : n < 2 ^ zero
i : Nat
hi : i ≥ zero
⊢ getBit n i = false
Tactic:
case zero => cases Nat.eq_zero_of_lt_one hn; exact zero_getBit i
State after:
no goals

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
⊢ getBit n i = false
Tactic:
case succ k h_ind =>
  have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hn
  cases hi
  case refl =>
    dsimp [getBit]
    exact h_ind ‹n/2 < 2^k› k Nat.le.refl
  case step i hstep =>
    dsimp [getBit]
    exact h_ind ‹n/2 < 2^k› i (Nat.le_of_succ_le hstep)
State after:
no goals

State before:
n : Nat
hn : n < 2 ^ zero
i : Nat
hi : i ≥ zero
⊢ getBit n i = false
Tactic:
cases Nat.eq_zero_of_lt_one hn
State after:
case refl
i : Nat
hi : i ≥ zero
hn : 0 < 2 ^ zero
⊢ getBit 0 i = false

State before:
case refl
i : Nat
hi : i ≥ zero
hn : 0 < 2 ^ zero
⊢ getBit 0 i = false
Tactic:
exact zero_getBit i
State after:
no goals

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
⊢ getBit n i = false
Tactic:
have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hn
State after:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
this : n / 2 < 2 ^ k
⊢ getBit n i = false

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
this : n / 2 < 2 ^ k
⊢ getBit n i = false
Tactic:
cases hi
State after:
case refl
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit n (succ k) = false

case step
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
m✝ : Nat
a✝ : Nat.le (succ k) m✝
⊢ getBit n (succ m✝) = false

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit n (succ k) = false
Tactic:
case refl =>
  dsimp [getBit]
  exact h_ind ‹n/2 < 2^k› k Nat.le.refl
State after:
no goals

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit n (succ i) = false
Tactic:
case step i hstep =>
  dsimp [getBit]
  exact h_ind ‹n/2 < 2^k› i (Nat.le_of_succ_le hstep)
State after:
no goals

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit n (succ k) = false
Tactic:
dsimp [getBit]
State after:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit (n / 2) k = false

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit (n / 2) k = false
Tactic:
exact h_ind ‹n/2 < 2^k› k Nat.le.refl
State after:
no goals

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit n (succ i) = false
Tactic:
dsimp [getBit]
State after:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit (n / 2) i = false

State before:
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
i : Nat
hstep : Nat.le (succ k) i
⊢ getBit (n / 2) i = false
Tactic:
exact h_ind ‹n/2 < 2^k› i (Nat.le_of_succ_le hstep)
State after:
no goals