Theorem: size_div_pow (Fl/Lemmas.lean)

State before:
x m : ℕ
h : 2 ^ m ≤ x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
Tactic:
have pos : 0 < x := Nat.lt_of_lt_of_le two_pow_pos h
State after:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m

State before:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
Tactic:
have lt_size : m < Nat.size x := by rwa [Nat.lt_size]
State after:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m

State before:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ Nat.size (x / 2 ^ m) = Nat.size x - m
Tactic:
apply size_of_le_of_lt
State after:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m

case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)

State before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m

case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Tactic:
. have le_size_pred : m ≤ Nat.size x - 1 := Nat.le_pred_of_lt lt_size
  rewrite [tsub_right_comm]
  rewrite [← Nat.pow_div le_size_pred two_pos]
  apply Nat.div_le_div_right
  exact le_size_of_pos pos
State after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)

State before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Tactic:
. have pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x := pow_dvd_pow 2 lt_size.le
  rewrite [Nat.div_lt_iff_lt_mul two_pow_pos]
  rewrite [← Nat.pow_div lt_size.le two_pos]
  rewrite [Nat.div_mul_cancel pow_dvd]
  exact Nat.lt_size_self x
State after:
no goals

State before:
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
⊢ m < Nat.size x
Tactic:
rwa [Nat.lt_size]
State after:
no goals

State before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m
Tactic:
have le_size_pred : m ≤ Nat.size x - 1 := Nat.le_pred_of_lt lt_size
State after:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m

State before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - m - 1) ≤ x / 2 ^ m
Tactic:
rewrite [tsub_right_comm]
State after:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1 - m) ≤ x / 2 ^ m

State before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1 - m) ≤ x / 2 ^ m
Tactic:
rewrite [← Nat.pow_div le_size_pred two_pos]
State after:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1) / 2 ^ m ≤ x / 2 ^ m

State before:
case hl
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1) / 2 ^ m ≤ x / 2 ^ m
Tactic:
apply Nat.div_le_div_right
State after:
case hl.h
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1) ≤ x

State before:
case hl.h
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
le_size_pred : m ≤ Nat.size x - 1
⊢ 2 ^ (Nat.size x - 1) ≤ x
Tactic:
exact le_size_of_pos pos
State after:
no goals

State before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Tactic:
have pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x := pow_dvd_pow 2 lt_size.le
State after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)

State before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x / 2 ^ m < 2 ^ (Nat.size x - m)
Tactic:
rewrite [Nat.div_lt_iff_lt_mul two_pow_pos]
State after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ (Nat.size x - m) * 2 ^ m

State before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ (Nat.size x - m) * 2 ^ m
Tactic:
rewrite [← Nat.pow_div lt_size.le two_pos]
State after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ Nat.size x / 2 ^ m * 2 ^ m

State before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ Nat.size x / 2 ^ m * 2 ^ m
Tactic:
rewrite [Nat.div_mul_cancel pow_dvd]
State after:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ Nat.size x

State before:
case hr
x m : ℕ
h : 2 ^ m ≤ x
pos : 0 < x
lt_size : m < Nat.size x
pow_dvd : 2 ^ m ∣ 2 ^ Nat.size x
⊢ x < 2 ^ Nat.size x
Tactic:
exact Nat.lt_size_self x
State after:
no goals