pith. machine review for the scientific record. sign in
lemma proved tactic proof

allOnes_testBit_lt

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  87private lemma allOnes_testBit_lt : ∀ {t k : Nat}, k < t → (allOnes t).testBit k = true
  88  | 0, _, hk => (Nat.not_lt_zero _ hk).elim
  89  | (t + 1), 0, _ => by
  90      -- `allOnes (t+1) = bit true (allOnes t)`
  91      have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t

proof body

Tactic-mode proof.

  92      simpa [hrepr] using (Nat.testBit_bit_zero true (allOnes t))
  93  | (t + 1), (k + 1), hk => by
  94      have hk' : k < t := Nat.lt_of_succ_lt_succ hk
  95      have hrepr : allOnes (t + 1) = Nat.bit true (allOnes t) := allOnes_succ_eq_bit t
  96      -- shift the bit index down one using `testBit_bit_succ`
  97      have hshift :
  98          (allOnes (t + 1)).testBit (k + 1) = (allOnes t).testBit k := by
  99        simpa [hrepr] using (Nat.testBit_bit_succ (b := true) (n := allOnes t) (m := k))
 100      -- now finish by IH
 101      simpa [hshift] using (allOnes_testBit_lt (t := t) (k := k) hk')
 102

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.