case z
n : ℕ
h✝ : ∀ (i : ℕ), testBit n i = false
h : ∀ (i : ℕ), testBit 0 i = false
⊢ 0 = 0

case f
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
⊢ bit b n = 0
n : ℕ
h : ∀ (i : ℕ), testBit n i = false
⊢ n = 0
induction' n using Nat.binaryRec with b n hn
no goals
case z
n : ℕ
h✝ : ∀ (i : ℕ), testBit n i = false
h : ∀ (i : ℕ), testBit 0 i = false
⊢ 0 = 0
rfl
case f
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
this : b = false
⊢ bit b n = 0
case f
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
⊢ bit b n = 0
have : b = false := by simpa using h 0
no goals
case f
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
this : b = false
⊢ bit b n = 0
rw [this, bit_false, bit0_val, hn fun i => by rw [← h (i + 1), testBit_succ], mul_zero]
no goals
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
⊢ b = false
simpa using h 0
no goals
n✝ : ℕ
h✝ : ∀ (i : ℕ), testBit n✝ i = false
b : Bool
n : ℕ
hn : (∀ (i : ℕ), testBit n i = false) → n = 0
h : ∀ (i : ℕ), testBit (bit b n) i = false
this : b = false
i : ℕ
⊢ testBit n i = false
rw [← h (i + 1), testBit_succ]