goal `0 = 0` after simp

Stream: mathlib4

[Nailin Guan]

I met a very strange problem in the following case. (Sorry that I didn't get it smaller, something strange happend).

module

public import Mathlib.RingTheory.LocalRing.Module

universe u v

open IsLocalRing

lemma basis_lift {R : Type u} [CommRing R] [Small.{v} R] [IsLocalRing R]
    (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (ι : Type*) (b : Module.Basis ι (R ⧸ maximalIdeal R) (M ⧸ maximalIdeal R • (⊤ : Submodule R M)))
    (f : (ι →₀ Shrink.{v, u} R) →ₗ[R] M) (hf : (maximalIdeal R • (⊤ : Submodule R M)).mkQ ∘ₗ f =
    (LinearEquiv.restrictScalars R b.repr).symm ∘ₗ
    Finsupp.mapRange.linearMap (Submodule.mkQ (maximalIdeal R) ∘ₗ (Shrink.linearEquiv R R))) :
    Function.Surjective f := by
  have : Function.Surjective ((LinearEquiv.restrictScalars R b.repr).symm.toLinearMap ∘ₗ
    Finsupp.mapRange.linearMap ((Submodule.mkQ (maximalIdeal R)).comp
    (Shrink.linearEquiv R R).toLinearMap)) := by
    apply (LinearEquiv.restrictScalars R b.repr).symm.surjective.comp
    apply Finsupp.mapRange_surjective _ ?_ ?_
    · simp
      sorry
    apply (Submodule.mkQ_surjective _).comp (Shrink.linearEquiv R R).surjective
  rw [← hf, ← LinearMap.range_eq_top, LinearMap.range_comp] at this
  exact LinearMap.range_eq_top.mp (IsLocalRing.map_mkQ_eq_top.mp this)

[Nailin Guan]

(On commit "52b9aaf")

[Robin Carlier]

Adding set_option backward.isDefEq.respectTransparency false in removes this error, but should not be considered a solution I think, see the thread #general > backward.isDefEq.respectTransparency .

[Nailin Guan]

moved

[Nailin Guan]

If this appear everywhere in mathlib, then I believe I have the right to use it until a fix come.