How do I prove this problem in lean4

Stream: new members

[Yanpeng Dong]

Show that every submodule of the quotient module M/N can be expressed as (L+N)/N for some submodule L of M.

[Andrew Yang]

docs#Submodule.map_comap_eq_of_surjective is essentially the same statement

[Junjie Bai]

When I tried to use the theorem you provided to solve this problem, I encountered some issues. When I attempted to substitute \( f \) with the quotient map (Submodule.Quotient.mk) in the theorem, Lean prompted me that some instances were missing, such as Funlike. Here is my code:

variable {R M F : Type} [CommRing R] [AddCommGroup M] [Module R M] {N L s: Submodule R M} [Module R (M ⧸ N)]

def f := Submodule.Quotient.mk (M := M) (p := N)

example (P : Submodule R (M ⧸ N)) : ∃ (L : Submodule R M), L.map f (L.comap f) = L := by sorry

How can I solve this issue?

[Andrew Yang]

First of all, you shoudn't write Module R (M ⧸ N). This means, "Suppose there exists an arbitrary R-module structure on M ⧸ N". You should leave this out and let lean find the right R-module structure on its own.
Second, L.map f (L.comap f) doesn't parse. Maybe you meant (L.map f).comap f = L or L.map f = P.

[Junjie Bai]

Thanks for pointing out these! I have change these problems, but (L.map f) will cause an error that "failed to synthesize
FunLike (?m.25475 → ?m.25475 ⧸ ?m.25479) M ?m.25462"
here is my code, how can i solve this?

variable {L : Submodule R M}

#check L.map

example (P : Submodule R (M ⧸ N)) : ∃ (L : Submodule R M), L.map f = P := by sorry

[Edward van de Meent]

the issue is that lean needs to know that f is a semilinear map, not just any map, between M and M ⧸ N. rather than Submodule.Quotient.mk, try using Submodule.mkQ

[Edward van de Meent]

you can tell that using mkQ will work because the type shows that it is indeed a linear map.