value multiplied by a unit is associated

Stream: Is there code for X?

[Ruben Van de Velde]

Do we not have (something like) these anywhere?

lemma associated_mul_unit {β : Type*} [monoid β] (a u : β) (hu : is_unit u) : associated (a * u) a :=
begin
  obtain ⟨u', hu⟩ := hu,
  refine ⟨(u'⁻¹ : units β), _⟩,
  rw [←hu, mul_assoc, units.mul_inv, mul_one],
end
lemma associated_unit_mul {β : Type*} [comm_monoid β] (a u : β) (hu : is_unit u) : associated (u * a) a :=
begin
  rw mul_comm,
  exact associated_mul_unit _ _ hu
end

[Anne Baanen]

I can't find it. In general, the API around associated is somewhat weak. (Wouldn't associated_mul_unit be more nicely expressed as (associated.mk u rfl).symm?)

[Eric Wieser]

The first lemma golfs to

lemma associated_mul_unit {β : Type*} [monoid β] (a u : β) (hu : is_unit u) : associated (a * u) a :=
begin
  obtain ⟨u, rfl⟩ := hu,
  exact ⟨u⁻¹, units.mul_inv_cancel_right _ _⟩,
end

[Eric Rodriguez]

One thing I've done a lot is change this sort of obtain ... exact ... style in my proofs to let ... in .... Is there any advantages/disadvantages to this?

[Ruben Van de Velde]

I don't think that works with rfl as a pattern

[Eric Rodriguez]

ahh I didn't notice the rfl