inv_of_inj

Stream: Is there code for X?

[Damiano Testa]

Dear All,

Lean gave me a hard time proving the result below, but I would imagine that it should already be available in some form or other.

Does anyone know of a simpler proof?

Thanks!

import algebra.invertible

lemma inv_of_inj {R : Type*} [monoid R] {a b : R} [invertible a] [invertible b] :
  ⅟ a = ⅟ b ↔ a = b :=
begin
  refine ⟨λ h, _, λ h, invertible_unique a b h⟩,
  unfreezingI
  { rcases is_unit_of_invertible a with ⟨au, rfl⟩,
    rcases is_unit_of_invertible b with ⟨bu, rfl⟩ },
  rw [inv_of_units, inv_of_units] at h,
  rw [← inv_inv au, ← inv_inv bu],
  exact congr_arg _ (inv_inj.mpr (units.ext h))
end

[Floris van Doorn]

import algebra.invertible

lemma inv_of_inj {R : Type*} [monoid R] {a b : R} [invertible a] [invertible b] :
  ⅟ a = ⅟ b ↔ a = b :=
begin
  refine ⟨λ h, _, λ h, invertible_unique a b h⟩,
  rw [← (inv_of_inv_of : _ = a), ← (inv_of_inv_of : _ = b)],
  exact invertible_unique _ _ h
end

[Damiano Testa]

Thanks for the golfing! Should I PR it?

[Floris van Doorn]

Yes, please do! It should go right after invertible_unique (and can be simp).

[Damiano Testa]

Ok, I'll do that once I'm back at a computer!

[Damiano Testa]

#14011

[Damiano Testa]

It turns out that

⟨λ h, invertible_unique _ _ h, λ h, invertible_unique _ _ h⟩

is also a proof. :upside_down:
Yet another fine example of proof by obfuscation.

(In case anyone is wondering, I tried removing the λ h, ... h but even Lean thinks that this is too obscure.)

[Yaël Dillies]

That's because the a = b argument comes before the [invertible a] [invertible b] arguments in docs#invertible_unique

[Yaël Dillies]

They should probably be swapped around.

[Damiano Testa]

If this is desirable, I can do it in this PR: I already made an argument in a different lemma explicit...

[Damiano Testa]

It seems that invertible_unique is uniquely used in mathlib. And with @!

[Damiano Testa]

Yaël, I went ahead, swapped the arguments and golfed the proof further.