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

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

case succ
n✝ : Nat
n_ih✝ : ∀ (n k : Nat), getBit (n % 2 ^ k) n✝ = (decide (n✝ < k) && getBit n n✝)
n k : Nat
⊢ getBit (n % 2 ^ k) (succ n✝) = (decide (succ n✝ < k) && getBit n (succ n✝))

State before:
n k : Nat
⊢ getBit (n % 2 ^ k) zero = (decide (zero < k) && getBit n zero)
Tactic:
case zero =>
  cases k
  case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
  case succ k =>
    conv => lhs; change decide (n%(2^k*2)%2=1); rw [Nat.mod_mul_mod_right]
    conv => rhs; simp [decide_eq_true k.zero_lt_succ]
State after:
no goals

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ k) (succ i) = (decide (succ i < k) && getBit n (succ i))
Tactic:
case succ i h_ind =>
  cases k
  case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
  case succ k =>
    unfold getBit
    have : i.succ < k.succ ↔ i < k :=
      ⟨λ h => Nat.lt_of_succ_lt_succ h, λ h => Nat.succ_lt_succ h⟩
    rw [decide_eq_decide.mpr this]
    conv => lhs; arg 1; change n%(2^k*2)/2; rw [Nat.mul_comm, Nat.mod_mul_div_left]
    exact h_ind (n/2) k
State after:
no goals

State before:
n k : Nat
⊢ getBit (n % 2 ^ k) zero = (decide (zero < k) && getBit n zero)
Tactic:
cases k
State after:
case zero
n : Nat
⊢ getBit (n % 2 ^ zero) zero = (decide (zero < zero) && getBit n zero)

case succ
n n✝ : Nat
⊢ getBit (n % 2 ^ succ n✝) zero = (decide (zero < succ n✝) && getBit n zero)

State before:
n : Nat
⊢ getBit (n % 2 ^ zero) zero = (decide (zero < zero) && getBit n zero)
Tactic:
case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
State after:
no goals

State before:
n k : Nat
⊢ getBit (n % 2 ^ succ k) zero = (decide (zero < succ k) && getBit n zero)
Tactic:
case succ k =>
  conv => lhs; change decide (n%(2^k*2)%2=1); rw [Nat.mod_mul_mod_right]
  conv => rhs; simp [decide_eq_true k.zero_lt_succ]
State after:
no goals

State before:
n : Nat
⊢ getBit (n % 2 ^ zero) zero = (decide (zero < zero) && getBit n zero)
Tactic:
conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
State after:
no goals

State before:
n k : Nat
⊢ getBit (n % 2 ^ succ k) zero = (decide (zero < succ k) && getBit n zero)
Tactic:
conv => lhs; change decide (n%(2^k*2)%2=1); rw [Nat.mod_mul_mod_right]
State after:
n k : Nat
⊢ decide (n % 2 = 1) = (decide (zero < succ k) && getBit n zero)

State before:
n k : Nat
⊢ decide (n % 2 = 1) = (decide (zero < succ k) && getBit n zero)
Tactic:
conv => rhs; simp [decide_eq_true k.zero_lt_succ]
State after:
no goals

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

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

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n : Nat
⊢ getBit (n % 2 ^ zero) (succ i) = (decide (succ i < zero) && getBit n (succ i))
Tactic:
case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
State after:
no goals

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k) (succ i) = (decide (succ i < succ k) && getBit n (succ i))
Tactic:
case succ k =>
  unfold getBit
  have : i.succ < k.succ ↔ i < k :=
    ⟨λ h => Nat.lt_of_succ_lt_succ h, λ h => Nat.succ_lt_succ h⟩
  rw [decide_eq_decide.mpr this]
  conv => lhs; arg 1; change n%(2^k*2)/2; rw [Nat.mul_comm, Nat.mod_mul_div_left]
  exact h_ind (n/2) k
State after:
no goals

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n : Nat
⊢ getBit (n % 2 ^ zero) (succ i) = (decide (succ i < zero) && getBit n (succ i))
Tactic:
conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
State after:
no goals

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k) (succ i) = (decide (succ i < succ k) && getBit n (succ i))
Tactic:
unfold getBit
State after:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)
Tactic:
have : i.succ < k.succ ↔ i < k :=
  ⟨λ h => Nat.lt_of_succ_lt_succ h, λ h => Nat.succ_lt_succ h⟩
State after:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)
Tactic:
rw [decide_eq_decide.mpr this]
State after:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (i < k) && getBit (n / 2) i)

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (i < k) && getBit (n / 2) i)
Tactic:
conv => lhs; arg 1; change n%(2^k*2)/2; rw [Nat.mul_comm, Nat.mod_mul_div_left]
State after:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n / 2 % 2 ^ k) i = (decide (i < k) && getBit (n / 2) i)

State before:
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n / 2 % 2 ^ k) i = (decide (i < k) && getBit (n / 2) i)
Tactic:
exact h_ind (n/2) k
State after:
no goals