Theorem: Nat.pred_size_eq_log (Lib.lean)

State before:
n : ℕ
⊢ size n - 1 = log 2 n
Tactic:
refine binaryRec' (n := n) rfl ?hi
State after:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n - 1 = log 2 n → size (bit b n) - 1 = log 2 (bit b n)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Tactic:
exact tsub_add_cancel_iff_le.mp rfl
State after:
case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 < 2

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

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

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 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✝) - 1 = log 2 (succ n✝)
⊢ 1 < 2

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

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

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

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

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 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✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ succ n✝

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

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

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 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✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 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✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0

State before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0
Tactic:
{ simp }
State after:
no goals

State before:
case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2
Tactic:
cases b <;> simp
State after:
no goals

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