Theorem: div_mul_eq_of_le_of_lt (Fl/Lemmas.lean)

State before:
m k x : ℕ
h : k ≤ m
⊢ 2 ^ m ≤ x → x < 2 ^ m + 2 ^ k → x / 2 ^ k * 2 ^ k = 2 ^ m
Tactic:
apply div_mul_eq_of_dvd_of_le_of_lt
State after:
case h₁
m k x : ℕ
h : k ≤ m
⊢ 2 ^ k ∣ 2 ^ m

State before:
case h₁
m k x : ℕ
h : k ≤ m
⊢ 2 ^ k ∣ 2 ^ m
Tactic:
exact pow_dvd_pow 2 h
State after:
no goals