mathlib

116435d6 - feat(tactic/alias): fix alias docstrings for implications from iffs (#13944)

feat(tactic/alias): fix alias docstrings for implications from iffs (#13944) Now they say for instance: ```lean le_inv_mul_of_mul_le : ∀ {α : Type u} [_inst_1 : group α] [_inst_2 : has_le α] [_inst_3 : covariant_class α α has_mul.mul has_le.le] {a b c : α}, a * b ≤ c → b ≤ a⁻¹ * c **Alias** of the reverse direction of `le_inv_mul_iff_mul_le`. ``` https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60alias.60.20issue.20in.20algebra.2Eorder.2Egroup/near/281158569