rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]
α : Type u_1
inst✝³ : CanonicallyLinearOrderedAddCommMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a - (a - b) = min a b
no goals