-- Mathlib/Data/Nat/Size.lean
theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
  ⟨fun h => lt_of_lt_of_le (lt_size_self _) (pow_le_pow_of_le_right (by decide) h), by
    rw [← one_shiftLeft]
    induction m using binaryRec generalizing n with
    | z => simp
    | f b m IH =>
      intro h
      by_cases e : bit b m = 0
      · simp [e]
      rw [size_bit e]
      cases n with
      | zero => exact e.elim (Nat.eq_zero_of_le_zero (le_of_lt_succ h))
      | succ n =>
        apply succ_le_succ (IH _)
        apply Nat.lt_of_mul_lt_mul_left (a := 2)
        simp only [shiftLeft_succ] at *
        refine lt_of_le_of_lt ?_ h
        cases b <;> dsimp [bit] <;> omega⟩

Proof state:
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 1 <<< (n + 1)
⊢ m < 1 <<< n

Tactic:
apply Nat.lt_of_mul_lt_mul_left (a := 2)

Result:
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 1 <<< (n + 1)
⊢ 2 * m < 2 * 1 <<< n

Proof state:
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 1 <<< (n + 1)
⊢ 2 * m < 2 * 1 <<< n

Tactic:
simp only [shiftLeft_succ] at *

Result:
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 2 * 1 <<< n
⊢ 2 * m < 2 * 1 <<< n

Proof state:
case neg.zero
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
h : bit b m < 1 <<< 0
⊢ m.size.succ ≤ 0

Tactic:
exact e.elim (Nat.eq_zero_of_le_zero (le_of_lt_succ h))

Result:
no goals

Proof state:
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 2 * 1 <<< n
⊢ 2 * m < 2 * 1 <<< n

Tactic:
refine lt_of_le_of_lt ?_ h

Result:
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 2 * 1 <<< n
⊢ 2 * m ≤ bit b m

Proof state:
case pos
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
h : bit b m < 1 <<< n
e : bit b m = 0
⊢ (bit b m).size ≤ n

Tactic:
simp [e]

Result:
no goals

Proof state:
case z
n : ℕ
⊢ 0 < 1 <<< n → size 0 ≤ n

Tactic:
simp

Result:
no goals

Proof state:
case neg.succ
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 1 <<< (n + 1)
⊢ m.size.succ ≤ n + 1

Tactic:
apply succ_le_succ (IH _)

Result:
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 1 <<< (n + 1)
⊢ m < 1 <<< n

Proof state:
m n : ℕ
⊢ m < 2 ^ n → m.size ≤ n

Tactic:
rw [← one_shiftLeft]

Result:
m n : ℕ
⊢ m < 1 <<< n → m.size ≤ n

Proof state:
m n : ℕ
h : m.size ≤ n
⊢ 2 > 0

Tactic:
decide

Result:
no goals

Proof state:
case neg
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
h : bit b m < 1 <<< n
e : ¬bit b m = 0
⊢ m.size.succ ≤ n

Tactic:
cases n with
| zero => exact e.elim (Nat.eq_zero_of_le_zero (le_of_lt_succ h))
| succ n =>
  apply succ_le_succ (IH _)
  apply Nat.lt_of_mul_lt_mul_left (a := 2)
  simp only [shiftLeft_succ] at *
  refine lt_of_le_of_lt ?_ h
  cases b <;> dsimp [bit] <;> omega

Result:
no goals

Proof state:
case f
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
⊢ bit b m < 1 <<< n → (bit b m).size ≤ n

Tactic:
intro h

Result:
case f
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
h : bit b m < 1 <<< n
⊢ (bit b m).size ≤ n

Proof state:
case f
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
h : bit b m < 1 <<< n
⊢ (bit b m).size ≤ n

Tactic:
by_cases e : bit b m = 0

Result:
case pos
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
h : bit b m < 1 <<< n
e : bit b m = 0
⊢ (bit b m).size ≤ n

case neg
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
h : bit b m < 1 <<< n
e : ¬bit b m = 0
⊢ (bit b m).size ≤ n

Proof state:
case neg
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
h : bit b m < 1 <<< n
e : ¬bit b m = 0
⊢ (bit b m).size ≤ n

Tactic:
rw [size_bit e]

Result:
case neg
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
n : ℕ
h : bit b m < 1 <<< n
e : ¬bit b m = 0
⊢ m.size.succ ≤ n

Proof state:
b : Bool
m : ℕ
IH : ∀ {n : ℕ}, m < 1 <<< n → m.size ≤ n
e : ¬bit b m = 0
n : ℕ
h : bit b m < 2 * 1 <<< n
⊢ 2 * m ≤ bit b m

Tactic:
cases b <;> dsimp [bit] <;> omega

Result:
no goals