Expression with `tmul` in it hangs for unclear reasons

Stream: mathlib4

[Brendan Seamas Murphy]

Here's a MWE for my problem

import Mathlib

namespace TensorProduct

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

open LinearMap

noncomputable def lTensor_ring_mod_ideal_equiv_mod_ideal_smul (I : Ideal R) :
    ((R⧸I) ⊗[R] M) ≃ₗ[R] M⧸(I • (⊤ : Submodule R M)) :=
  (rTensor.equiv _ (exact_subtype_mkQ I) I.mkQ_surjective).symm.trans <|
    Submodule.Quotient.equiv _ _ (TensorProduct.lid R M) sorry

lemma lTensor_ring_mod_ideal_equiv_mod_ideal_smul_apply
    (I : Ideal R) (r : R) (x : M) :
    lTensor_ring_mod_ideal_equiv_mod_ideal_smul I
      (Ideal.Quotient.mk I r ⊗ₜ[R] _) = Submodule.mkQ (I • ⊤) (r • x) :=
  sorry

end TensorProduct

and a slightly less minimal example with the stubbed out proof in lTensor_ring_mod_ideal_equiv_mod_ideal_smul filled in: https://gist.github.com/Shamrock-Frost/69d63790ab3b3137c14847161bb91b27. If I fill in the underscore in Ideal.Quotient.mk I r ⊗ₜ[R] _ and write Ideal.Quotient.mk I r ⊗ₜ[R] x then lean hangs. Why is this, and how can I fix it? It does not happen if I fill in the _ with sorry.

[Brendan Seamas Murphy]

(also if this equivalence is in mathlib and I missed it please let me know!)

[Matthew Ballard]

This seems fixed with lean4#4092

[Matthew Ballard]

Filling x instantly pops up declaration uses sorry

[Brendan Seamas Murphy]

huh! great timing on my part to run into this bug I guess

[Matthew Ballard]

Thank Leo who traced it into the binop% elaborator.

[Matthew Ballard]

Now you just need to convince Kim to put it into rc2... :)

[Brendan Seamas Murphy]

I think for now I'm going to stick with the ol reliable set_option maxHeartbeats 800000 in and hope the fix gets merged before I PR this code in

[Kim Morrison]

Matthew Ballard said:

Now you just need to convince Kim to put it into rc2... :)

I've marked it for backporting!

[Brendan Seamas Murphy]

welp, after updating mathlib it times out and requires set_option maxHeartbeats 1200000. What's the timeline for when the mathlib CI will be on this lean4 version? Not trying to rush anything, this can wait to get merged, I'm just unfamiliar

[Matthew Ballard]

Usual cadence is when the month turns over

[Matthew Ballard]

You could

1. run off a custom toolchain (eg mattrobball/lean4:test2-24-05-07)
2. build on top of nightly
3. or wait

until then. I probably would not do 2.

[Matthew Ballard]

This is lightning quick in v4.8.0-rc2