Injectivity of the inclusion of an ideal into a ring

Stream: new members

[Jarod Alper]

I am playing around with rings and ideals, and am struggling to even show that the canonical inclusion of an ideal into a commutative ring is injective:

import Mathlib.RingTheory.Ideal.Basic

variable {R : Type*} [CommRing R]
variable {I : Ideal R}

example : Function.Injective (Submodule.subtype I) := by
  sorry

Any suggestions?

[Matthew Ballard]

exact?

[Matthew Ballard]

This tactic used to be called library search (which is perhaps more descriptive). If you use it in place of sorry, you can see if there is something simple to solve the problem

[Matthew Ballard]

Unless you want to bare-knuckle it?

[Jarod Alper]

Matthew Ballard said:

exact?

Thanks! I had actually tried Submodule.injective_subtype in my code (as it was suggested by github copilot and Lean copilot in addition to exact?) but it didn't work in my only slightly more complicated code:

   have ItoR := Submodule.subtype I
   have ItoR_injective : Function.Injective ItoR := by
        exact Submodule.injective_subtype I

in which case I was getting the error

type mismatch
  injective_subtype I
has type
  Function.Injective ⇑(Submodule.subtype I) : Prop
but is expected to have type
  Function.Injective ⇑ItoR : Prop

Any further suggestions?

[Matthew Ballard]

have is data irrelevant. It forgets what the definition is. Does let work?

[Jarod Alper]

Matthew Ballard said:

have is data irrelevant. It forgets what the definition is. Does let work?

Yep, let worked. I've been relying too much on have apparently. Thanks!

[Johan Commelin]

@Damiano Testa recently wrote a have/let linter that will send you a friendly reminder next time (-;
You'll need a recent mathlib to have it work.