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

State before:
k i : Nat
⊢ getBit (2 ^ k - 1) i = decide (i < k)
Tactic:
induction k generalizing i
State after:
case zero
i : Nat
⊢ getBit (2 ^ zero - 1) i = decide (i < zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (i : Nat), getBit (2 ^ n✝ - 1) i = decide (i < n✝)
i : Nat
⊢ getBit (2 ^ succ n✝ - 1) i = decide (i < succ n✝)

State before:
i : Nat
⊢ getBit (2 ^ zero - 1) i = decide (i < zero)
Tactic:
case zero =>
  conv => lhs; rw [Nat.pow_zero]; change getBit 0 i; rw [Nat.zero_getBit]
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) i = decide (i < succ k)
Tactic:
case succ k h_ind =>
  cases i
  case zero =>
    dsimp [Nat.getBit]; apply decide_eq_decide.mpr
    have := calc
      (2^k.succ - 1) % 2
        = (2^k*2 - 1) % 2 := by rw [Nat.pow_succ]
      _ = (2-1)%2 :=
        Nat.mul_sub_mod_right (Nat.pos_pow_of_pos (n:=2) _ (by decide)) (.step .refl)
      _ = 1 := rfl
    rw [this]
    constructor <;> intros; exact k.zero_lt_succ; rfl
  case succ i =>
    have := calc
      (2^k.succ - 1).getBit i.succ
        = ((2^k*2 - 1)/2).getBit i := by rw [Nat.pow_succ, Nat.getBit]
      _ = (2^k - 1).getBit i :=
        by rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]; rfl
    rw [this, h_ind]; apply decide_eq_decide.mpr
    exact ⟨Nat.succ_lt_succ, Nat.lt_of_succ_lt_succ⟩
State after:
no goals

State before:
i : Nat
⊢ getBit (2 ^ zero - 1) i = decide (i < zero)
Tactic:
conv => lhs; rw [Nat.pow_zero]; change getBit 0 i; rw [Nat.zero_getBit]
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) i = decide (i < succ k)
Tactic:
cases i
State after:
case zero
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ getBit (2 ^ succ k - 1) zero = decide (zero < succ k)

case succ
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
n✝ : Nat
⊢ getBit (2 ^ succ k - 1) (succ n✝) = decide (succ n✝ < succ k)

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ getBit (2 ^ succ k - 1) zero = decide (zero < succ k)
Tactic:
case zero =>
  dsimp [Nat.getBit]; apply decide_eq_decide.mpr
  have := calc
    (2^k.succ - 1) % 2
      = (2^k*2 - 1) % 2 := by rw [Nat.pow_succ]
    _ = (2-1)%2 :=
      Nat.mul_sub_mod_right (Nat.pos_pow_of_pos (n:=2) _ (by decide)) (.step .refl)
    _ = 1 := rfl
  rw [this]
  constructor <;> intros; exact k.zero_lt_succ; rfl
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) (succ i) = decide (succ i < succ k)
Tactic:
case succ i =>
  have := calc
    (2^k.succ - 1).getBit i.succ
      = ((2^k*2 - 1)/2).getBit i := by rw [Nat.pow_succ, Nat.getBit]
    _ = (2^k - 1).getBit i :=
      by rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]; rfl
  rw [this, h_ind]; apply decide_eq_decide.mpr
  exact ⟨Nat.succ_lt_succ, Nat.lt_of_succ_lt_succ⟩
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ getBit (2 ^ succ k - 1) zero = decide (zero < succ k)
Tactic:
dsimp [Nat.getBit]
State after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ decide ((2 ^ succ k - 1) % 2 = 1) = decide (0 < succ k)

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ decide ((2 ^ succ k - 1) % 2 = 1) = decide (0 < succ k)
Tactic:
apply decide_eq_decide.mpr
State after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k
Tactic:
have := calc
  (2^k.succ - 1) % 2
    = (2^k*2 - 1) % 2 := by rw [Nat.pow_succ]
  _ = (2-1)%2 :=
    Nat.mul_sub_mod_right (Nat.pos_pow_of_pos (n:=2) _ (by decide)) (.step .refl)
  _ = 1 := rfl
State after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k
Tactic:
rw [this]
State after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ 1 = 1 ↔ 0 < succ k

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ 1 = 1 ↔ 0 < succ k
Tactic:
constructor <;> intros
State after:
case mp
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 1 = 1
⊢ 0 < succ k

case mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 0 < succ k
⊢ 1 = 1

State before:
case mp
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 1 = 1
⊢ 0 < succ k

case mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 0 < succ k
⊢ 1 = 1
Tactic:
exact k.zero_lt_succ
State after:
case mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 0 < succ k
⊢ 1 = 1

State before:
case mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
a✝ : 0 < succ k
⊢ 1 = 1
Tactic:
rfl
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ (2 ^ succ k - 1) % 2 = (2 ^ k * 2 - 1) % 2
Tactic:
rw [Nat.pow_succ]
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ 0 < 2
Tactic:
decide
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) (succ i) = decide (succ i < succ k)
Tactic:
have := calc
  (2^k.succ - 1).getBit i.succ
    = ((2^k*2 - 1)/2).getBit i := by rw [Nat.pow_succ, Nat.getBit]
  _ = (2^k - 1).getBit i :=
    by rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]; rfl
State after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ getBit (2 ^ succ k - 1) (succ i) = decide (succ i < succ k)

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ getBit (2 ^ succ k - 1) (succ i) = decide (succ i < succ k)
Tactic:
rw [this, h_ind]
State after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ decide (i < k) = decide (succ i < succ k)

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ decide (i < k) = decide (succ i < succ k)
Tactic:
apply decide_eq_decide.mpr
State after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ i < k ↔ succ i < succ k

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ i < k ↔ succ i < succ k
Tactic:
exact ⟨Nat.succ_lt_succ, Nat.lt_of_succ_lt_succ⟩
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ succ k - 1) (succ i) = getBit ((2 ^ k * 2 - 1) / 2) i
Tactic:
rw [Nat.pow_succ, Nat.getBit]
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit ((2 ^ k * 2 - 1) / 2) i = getBit (2 ^ k - 1) i
Tactic:
rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]
State after:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ k - succ (0 / 2)) i = getBit (2 ^ k - 1) i

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ k - succ (0 / 2)) i = getBit (2 ^ k - 1) i
Tactic:
rfl
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ 2 > 0
Tactic:
decide
State after:
no goals

State before:
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ 0 < 2
Tactic:
decide
State after:
no goals