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





leanprover-community/mathlib,leanprover-community/mathlib