Theorem: mul_tsub_one (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 * (b - 1) = a * b - a
Tactic:
rw [mul_tsub, mul_one]
State after:
no goals