Theorem: div_mul_eq_of_dvd_of_le_of_lt (Fl/Lemmas.lean)

State before:
m k x : ℕ
h₁ : k ∣ m
h₂ : m ≤ x
h₃ : x < m + k
⊢ x / k * k = m
Tactic:
have ⟨d, hd⟩ := h₁
State after:
m k x : ℕ
h₁ : k ∣ m
h₂ : m ≤ x
h₃ : x < m + k
d : ℕ
hd : m = k * d
⊢ x / k * k = m

State before:
m k x : ℕ
h₁ : k ∣ m
h₂ : m ≤ x
h₃ : x < m + k
d : ℕ
hd : m = k * d
⊢ x / k * k = m
Tactic:
rewrite [hd, mul_comm k] at h₂ h₃ ⊢
State after:
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < d * k + k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k

State before:
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < d * k + k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k
Tactic:
rewrite [← Nat.succ_mul] at h₃
State after:
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < Nat.succ d * k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k

State before:
m k x : ℕ
h₁ : k ∣ m
d : ℕ
h₃ : x < Nat.succ d * k
h₂ : d * k ≤ x
hd : m = k * d
⊢ x / k * k = d * k
Tactic:
rw [Nat.div_eq_of_lt_le h₂ h₃]
State after:
no goals