fail to synth an easy instance

Stream: mathlib4

[Nailin Guan]

I met a strange problem after the update to 4.29-rc1 (previously it was 4.28-rc1?)

module

public import Mathlib.Algebra.Category.ModuleCat.EpiMono

variable {R M N : Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]

instance (f : M →ₗ[R] N) :  Module R f.ker := inferInstance

lemma foo (f : M →ₗ[R] N) : CategoryTheory.Mono (ModuleCat.ofHom f.ker.subtype) := by
  sorry

This has error "Module R ↥f.ker", but inferInstance works.

[Nailin Guan]

(On commit "52b9aaf")

[Nailin Guan]

Similar problem in the following, but it failed completely

variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M)

instance : HasQuotient (↥N) (Submodule R ↥N) := sorry -- inferInstance

[Robin Arnez]

Another problem related to #general > backward.isDefEq.respectTransparency :-)

import Mathlib

variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M] (N : Submodule R M)

set_option backward.isDefEq.respectTransparency false

instance : HasQuotient (↥N) (Submodule R ↥N) := inferInstance

works if you need a workaround.

[Nailin Guan]

OK, many unrelated things seems to because of the same reason, thanks.