Theorem: size_div_mul (Fl/Lemmas.lean)

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

State before:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size (x / 2 ^ m * 2 ^ m) = Nat.size x
Tactic:
rewrite [size_mul_pow div_pow_pos m]
State after:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size (x / 2 ^ m) + m = Nat.size x

State before:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size (x / 2 ^ m) + m = Nat.size x
Tactic:
rewrite [size_div_pow h]
State after:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size x - m + m = Nat.size x

State before:
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.size x - m + m = Nat.size x
Tactic:
apply tsub_add_cancel_of_le
State after:
case h
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ m ≤ Nat.size x

State before:
case h
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ m ≤ Nat.size x
Tactic:
apply Nat.le_of_pred_lt
State after:
case h.a
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.pred m < Nat.size x

State before:
case h.a
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ Nat.pred m < Nat.size x
Tactic:
rewrite [Nat.lt_size]
State after:
case h.a
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ 2 ^ Nat.pred m ≤ x

State before:
case h.a
x m : ℕ
h : 2 ^ m ≤ x
div_pow_pos : 0 < x / 2 ^ m
⊢ 2 ^ Nat.pred m ≤ x
Tactic:
calc 2 ^ Nat.pred m
  _ ≤ 2 ^ m := Nat.pow_le_pow_of_le_right two_pos (Nat.pred_le m)
  _ ≤ x     := h
State after:
no goals