Theorem: Int.nat_mul_div_assoc (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
⊢ b % c = 0 → a * b / c = a * (b / c)
Tactic:
intro hmod
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ a * b / c = a * (b / c)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ a * b / c = a * (b / c)
Tactic:
rw [Nat.mul_div_assoc]
State after:
case H
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ c ∣ b

State before:
case H
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ c ∣ b
Tactic:
rwa [← Nat.modEq_zero_iff_dvd]
State after:
no goals