slow rewrite inside conv

Stream: lean4

[Arend Mellendijk]

I'm porting my project into lean 4 and ran into an issue while reordering sums.

In lean 3 the following code runs instantly

import algebra.big_operators.basic
import number_theory.divisors

open finset

open_locale big_operators

set_option profiler true

/-
parsing took 48ms
-/
example (P : ℕ) :
    ∑ d1 d2 l in P.divisors, d1 * d2
  = ∑ l d1 d2 in P.divisors, d1 * d2 :=
begin
  conv{to_rhs, rw sum_comm},
  apply sum_congr rfl,
  intros d1 hd1,
  rw sum_comm,
end

But translated directly into lean 4 the sum_comm inside the conv block takes ages to run.

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.NumberTheory.Divisors

open Finset

open scoped BigOperators
set_option profiler true

/-
tactic execution of Lean.Parser.Tactic.refl took 12.6s
tactic execution of Lean.Parser.Tactic.tacticRfl took 11.3s
-/
example (P : ℕ) :
  ∑ d1 in P.divisors, ∑ d2 in P.divisors, ∑ l in P.divisors, d1 * d2
  = ∑ l in P.divisors, ∑ d1 in P.divisors, ∑ d2 in P.divisors, d1 * d2 :=
  by
  conv =>
    rhs
    rw [sum_comm];
  rw [sum_congr rfl]; intro d1 hd1
  rw [sum_comm]

/- Compiles instantly -/
example (P : ℕ) :
  ∑ d1 in P.divisors, ∑ d2 in P.divisors, ∑ l in P.divisors, d1 * d2
  = ∑ l in P.divisors, ∑ d1 in P.divisors, ∑ d2 in P.divisors, d1 * d2 :=
  by
  apply symm
  rw [sum_comm, sum_congr rfl]; intro d1 hd1
  rw [sum_comm]

I've obviously found a workaround, but I'm wondering what's causing the difference with lean 3. Does anybody have an idea?

[Alex J. Best]

The slow part is calling rfl which conv does by default, so you can see the difference just by trying refl as the first line of the proof, i.e

example (P : ℕ) :
  ∑ d1 in P.divisors, ∑ d2 in P.divisors, ∑ l in P.divisors, d1 * d2
  = ∑ l in P.divisors, ∑ d1 in P.divisors, ∑ d2 in P.divisors, d1 * d2 :=
  by
  rfl

takes a long time to fail