Theorem: div_mul_div_cancel_of_dvd (Fl/Lemmas.lean)

State before:
n m k : ℕ
h₂ : k ∣ m
⊢ n / k * k / m = n / m
Tactic:
have ⟨d, hd⟩ := h₂
State after:
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / m = n / m

State before:
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / m = n / m
Tactic:
rewrite [hd]
State after:
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / (k * d) = n / (k * d)

State before:
n m k : ℕ
h₂ : k ∣ m
d : ℕ
hd : m = k * d
⊢ n / k * k / (k * d) = n / (k * d)
Tactic:
match k with
| 0 => rw [Nat.mul_zero, Nat.zero_mul, Nat.zero_div, Nat.div_zero]
| x + 1 =>
  rewrite [← Nat.div_div_eq_div_mul]
  rewrite [Nat.mul_div_cancel _ (Nat.add_pos_right _ zero_lt_one)]
  exact Nat.div_div_eq_div_mul _ _ _
State after:
no goals

State before:
n m k d : ℕ
h₂ : 0 ∣ m
hd : m = 0 * d
⊢ n / 0 * 0 / (0 * d) = n / (0 * d)
Tactic:
rw [Nat.mul_zero, Nat.zero_mul, Nat.zero_div, Nat.div_zero]
State after:
no goals

State before:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) * (x + 1) / ((x + 1) * d) = n / ((x + 1) * d)
Tactic:
rewrite [← Nat.div_div_eq_div_mul]
State after:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) * (x + 1) / (x + 1) / d = n / ((x + 1) * d)

State before:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) * (x + 1) / (x + 1) / d = n / ((x + 1) * d)
Tactic:
rewrite [Nat.mul_div_cancel _ (Nat.add_pos_right _ zero_lt_one)]
State after:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) / d = n / ((x + 1) * d)

State before:
n m k d x : ℕ
h₂ : x + 1 ∣ m
hd : m = (x + 1) * d
⊢ n / (x + 1) / d = n / ((x + 1) * d)
Tactic:
exact Nat.div_div_eq_div_mul _ _ _
State after:
no goals