Theorem: Nat.size_le_succ_log (Lib.lean)

State before:
n : ℕ
⊢ size n ≤ log 2 n + 1
Tactic:
refine binaryRec' (n := n) ?hz ?hi
State after:
case hz
n : ℕ
⊢ size 0 ≤ log 2 0 + 1

case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1

State before:
case hz
n : ℕ
⊢ size 0 ≤ log 2 0 + 1

case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1
Tactic:
exact zero_le _
State after:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1

State before:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1
Tactic:
intro b n hb ih
State after:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ log 2 n + 1
⊢ size (bit b n) ≤ log 2 (bit b n) + 1

State before:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ log 2 n + 1
⊢ size (bit b n) ≤ log 2 (bit b n) + 1
Tactic:
cases n
State after:
case hi.zero
n : ℕ
b : Bool
hb : zero = 0 → b = true
ih : size zero ≤ log 2 zero + 1
⊢ size (bit b zero) ≤ log 2 (bit b zero) + 1

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1

State before:
case hi.zero
n : ℕ
b : Bool
hb : zero = 0 → b = true
ih : size zero ≤ log 2 zero + 1
⊢ size (bit b zero) ≤ log 2 (bit b zero) + 1

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1
Tactic:
cases b <;> simp
State after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1

State before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1
Tactic:
rw [size_bit, bit_val, Nat.log_mul_add]
State after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ succ (size (succ n✝)) ≤ log 2 (succ n✝) + 1 + 1

case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0

State before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ succ (size (succ n✝)) ≤ log 2 (succ n✝) + 1 + 1

case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
apply Nat.succ_le_succ ih
State after:
case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0

State before:
case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
apply one_lt_two
State after:
case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0

State before:
case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
apply Nat.succ_le_succ (zero_le _)
State after:
case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0

State before:
case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
cases b <;> simp
State after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0

State before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
cases b <;> simp
State after:
no goals