Theorem: Nat.size_div2 (Lib.lean)

State before:
n : ℕ
⊢ size (n / 2) = size n - 1
Tactic:
induction n using Nat.binaryRec' with
| z => rfl
| _ _ _ h =>
  rw [bit_div_2, size_bit]
  apply Eq.symm
  apply Nat.pred_succ
  apply bit_ne_zero_iff.mpr h
State after:
no goals

State before:
case z

⊢ size (0 / 2) = size 0 - 1
Tactic:
rfl
State after:
no goals

State before:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size (bit b✝ n✝ / 2) = size (bit b✝ n✝) - 1
Tactic:
rw [bit_div_2, size_bit]
State after:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size n✝ = succ (size n✝) - 1

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0

State before:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size n✝ = succ (size n✝) - 1

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Tactic:
apply Eq.symm
State after:
case f.h
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ succ (size n✝) - 1 = size n✝

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0

State before:
case f.h
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ succ (size n✝) - 1 = size n✝

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Tactic:
apply Nat.pred_succ
State after:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0

State before:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
Tactic:
apply bit_ne_zero_iff.mpr h
State after:
no goals