Theorem: tsub_one_mul (LeanCamCombi/Mathlib/Algebra/Order/Ring/Canonical.lean)

State before:
α : Type u_1
inst✝⁴ : CanonicallyOrderedCommSemiring α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a - 1) * b = a * b - b
Tactic:
rw [tsub_mul, one_mul]
State after:
no goals