Theorem: Nat.log2'_le_log2' (Algdata/Data/Nat/Bits.lean)

State before:
m n : Nat
⊢ m ≤ n → log2' m ≤ log2' n
Tactic:
induction m using recBase2 generalizing n
State after:
case zero
n : Nat
⊢ 0 ≤ n → log2' 0 ≤ log2' n

case one
n : Nat
⊢ 1 ≤ n → log2' 1 ≤ log2' n

case div2
n✝ : Nat
a✝ : ∀ {n : Nat}, n✝ / 2 + 1 ≤ n → log2' (n✝ / 2 + 1) ≤ log2' n
n : Nat
⊢ n✝ + 2 ≤ n → log2' (n✝ + 2) ≤ log2' n

State before:
n : Nat
⊢ 0 ≤ n → log2' 0 ≤ log2' n
Tactic:
case zero => intros; exact Nat.zero_le _
State after:
no goals

State before:
n : Nat
⊢ 1 ≤ n → log2' 1 ≤ log2' n
Tactic:
case one => intros; exact Nat.zero_le _
State after:
no goals

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
⊢ m + 2 ≤ n → log2' (m + 2) ≤ log2' n
Tactic:
case div2 m h_ind =>
  intro h
  let k := n-2
  have : n = k+2 := Eq.symm $ Nat.sub_add_cancel $ calc
    2 ≤ m+2 := Nat.le_add_left 2 m
    _ ≤ n := h
  rw [this]; unfold log2'; simp [recBase2_div2]
  conv => change (m/2+1).log2' + 1 ≤ (k/2+1).log2' + 1
  suffices m/2+1 ≤ k/2+1
    from Nat.succ_le_succ (h_ind this)
  suffices m ≤ k
    from Nat.succ_le_succ (div_le_div this)
  show m ≤ k;
    exact Nat.le_of_add_le_add_right (‹n=k+2› ▸ h)
State after:
no goals

State before:
n : Nat
⊢ 0 ≤ n → log2' 0 ≤ log2' n
Tactic:
intros
State after:
n : Nat
a✝ : 0 ≤ n
⊢ log2' 0 ≤ log2' n

State before:
n : Nat
a✝ : 0 ≤ n
⊢ log2' 0 ≤ log2' n
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
n : Nat
⊢ 1 ≤ n → log2' 1 ≤ log2' n
Tactic:
intros
State after:
n : Nat
a✝ : 1 ≤ n
⊢ log2' 1 ≤ log2' n

State before:
n : Nat
a✝ : 1 ≤ n
⊢ log2' 1 ≤ log2' n
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
⊢ m + 2 ≤ n → log2' (m + 2) ≤ log2' n
Tactic:
intro h
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
⊢ log2' (m + 2) ≤ log2' n

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
⊢ log2' (m + 2) ≤ log2' n
Tactic:
let k := n-2
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
⊢ log2' (m + 2) ≤ log2' n

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
⊢ log2' (m + 2) ≤ log2' n
Tactic:
have : n = k+2 := Eq.symm $ Nat.sub_add_cancel $ calc
  2 ≤ m+2 := Nat.le_add_left 2 m
  _ ≤ n := h
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m + 2) ≤ log2' n

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m + 2) ≤ log2' n
Tactic:
rw [this]
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m + 2) ≤ log2' (k + 2)

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m + 2) ≤ log2' (k + 2)
Tactic:
unfold log2'
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (m + 2) ≤ recBase2 0 0 (fun x x_1 => x_1 + 1) (k + 2)

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (m + 2) ≤ recBase2 0 0 (fun x x_1 => x_1 + 1) (k + 2)
Tactic:
simp [recBase2_div2]
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (m / 2 + 1) + 1 ≤ recBase2 0 0 (fun x x_1 => x_1 + 1) ((n - 2) / 2 + 1) + 1

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (m / 2 + 1) + 1 ≤ recBase2 0 0 (fun x x_1 => x_1 + 1) ((n - 2) / 2 + 1) + 1
Tactic:
conv => change (m/2+1).log2' + 1 ≤ (k/2+1).log2' + 1
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m / 2 + 1) + 1 ≤ log2' (k / 2 + 1) + 1

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m / 2 + 1) + 1 ≤ log2' (k / 2 + 1) + 1
Tactic:
suffices m/2+1 ≤ k/2+1
  from Nat.succ_le_succ (h_ind this)
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ m / 2 + 1 ≤ k / 2 + 1

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ m / 2 + 1 ≤ k / 2 + 1
Tactic:
suffices m ≤ k
  from Nat.succ_le_succ (div_le_div this)
State after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ m ≤ k

State before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ m ≤ k
Tactic:
exact Nat.le_of_add_le_add_right (‹n=k+2› ▸ h)
State after:
no goals