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

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

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

State before:
k : Nat
⊢ getBit (2 ^ k) zero = decide (k = zero)
Tactic:
case zero =>
  dsimp [getBit]
  cases k
  case zero => decide
  case succ k => conv => lhs; change decide (2^k*2%2 = 1); simp
State after:
no goals

State before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) (succ i) = decide (k = succ i)
Tactic:
case succ i h_ind =>
  dsimp [getBit]
  cases k
  case zero =>
    conv => change getBit 0 i = false
    simp
  case succ k =>
    conv => lhs; arg 1; change 2^k*2/2; simp
    have : k = i ↔ k.succ = i.succ := ⟨λ h => h ▸ rfl, λ h => Nat.succ.inj h⟩
    rw [h_ind, decide_eq_decide.mpr this]
State after:
no goals

State before:
k : Nat
⊢ getBit (2 ^ k) zero = decide (k = zero)
Tactic:
dsimp [getBit]
State after:
k : Nat
⊢ decide (2 ^ k % 2 = 1) = decide (k = 0)

State before:
k : Nat
⊢ decide (2 ^ k % 2 = 1) = decide (k = 0)
Tactic:
cases k
State after:
case zero

⊢ decide (2 ^ zero % 2 = 1) = decide (zero = 0)

case succ
n✝ : Nat
⊢ decide (2 ^ succ n✝ % 2 = 1) = decide (succ n✝ = 0)

State before:
⊢ decide (2 ^ zero % 2 = 1) = decide (zero = 0)
Tactic:
case zero => decide
State after:
no goals

State before:
k : Nat
⊢ decide (2 ^ succ k % 2 = 1) = decide (succ k = 0)
Tactic:
case succ k => conv => lhs; change decide (2^k*2%2 = 1); simp
State after:
no goals

State before:
⊢ decide (2 ^ zero % 2 = 1) = decide (zero = 0)
Tactic:
decide
State after:
no goals

State before:
k : Nat
⊢ decide (2 ^ succ k % 2 = 1) = decide (succ k = 0)
Tactic:
conv => lhs; change decide (2^k*2%2 = 1); simp
State after:
no goals

State before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) (succ i) = decide (k = succ i)
Tactic:
dsimp [getBit]
State after:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k / 2) i = decide (k = succ i)

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

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

State before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit (2 ^ zero / 2) i = decide (zero = succ i)
Tactic:
case zero =>
  conv => change getBit 0 i = false
  simp
State after:
no goals

State before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ succ k / 2) i = decide (succ k = succ i)
Tactic:
case succ k =>
  conv => lhs; arg 1; change 2^k*2/2; simp
  have : k = i ↔ k.succ = i.succ := ⟨λ h => h ▸ rfl, λ h => Nat.succ.inj h⟩
  rw [h_ind, decide_eq_decide.mpr this]
State after:
no goals

State before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit (2 ^ zero / 2) i = decide (zero = succ i)
Tactic:
conv => change getBit 0 i = false
State after:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
⊢ getBit 0 i = false

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

State before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ succ k / 2) i = decide (succ k = succ i)
Tactic:
conv => lhs; arg 1; change 2^k*2/2; simp
State after:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) i = decide (succ k = succ i)

State before:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
⊢ getBit (2 ^ k) i = decide (succ k = succ i)
Tactic:
have : k = i ↔ k.succ = i.succ := ⟨λ h => h ▸ rfl, λ h => Nat.succ.inj h⟩
State after:
i : Nat
h_ind : ∀ (k : Nat), getBit (2 ^ k) i = decide (k = i)
k : Nat
this : k = i ↔ succ k = succ i
⊢ getBit (2 ^ k) i = decide (succ k = succ i)

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