n : ℕ
⊢ n < shiftl 1 (size n)
n : ℕ
⊢ n < 2 ^ size n
rw [← one_shiftl]
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ n < shiftl 1 (size n)
n : ℕ
⊢ n < shiftl 1 (size n)
have : ∀ {n}, n = 0 → n < shiftl 1 (size n) := by simp
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ 0 < shiftl 1 (size 0)

n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ ∀ (b : Bool) (n : ℕ), n < shiftl 1 (size n) → bit b n < shiftl 1 (size (bit b n))
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ n < shiftl 1 (size n)
apply binaryRec _ _ n
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
⊢ bit b n < shiftl 1 (size (bit b n))
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ ∀ (b : Bool) (n : ℕ), n < shiftl 1 (size n) → bit b n < shiftl 1 (size (bit b n))
intro b n IH
case pos
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : bit b n = 0
⊢ bit b n < shiftl 1 (size (bit b n))

case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : ¬bit b n = 0
⊢ bit b n < shiftl 1 (size (bit b n))
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
⊢ bit b n < shiftl 1 (size (bit b n))
by_cases h : bit b n = 0
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : ¬bit b n = 0
⊢ bit b n < bit0 (shiftl 1 (size n))
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : ¬bit b n = 0
⊢ bit b n < shiftl 1 (size (bit b n))
rw [size_bit h, shiftl_succ]
no goals
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : ¬bit b n = 0
⊢ bit b n < bit0 (shiftl 1 (size n))
exact bit_lt_bit0 _ IH
no goals
n : ℕ
⊢ ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
simp
no goals
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
⊢ 0 < shiftl 1 (size 0)
apply this rfl
no goals
case pos
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < shiftl 1 (size n)
b : Bool
n : ℕ
IH : n < shiftl 1 (size n)
h : bit b n = 0
⊢ bit b n < shiftl 1 (size (bit b n))
apply this h