convert ... using ... with ...

Stream: mathlib4

[Michael Stoll]

The following surprsies me:

import Mathlib.Tactic

open BigOperators

def Nat.primesBelow (n : ℕ) : Finset ℕ := (Finset.range n).filter (fun p ↦ p.Prime)

example (f : ℕ → ℂ) (n : ℕ) :
    ∑ p in n.primesBelow, f p = ∑ m in Finset.range n, Set.indicator {p : ℕ | p.Prime} f m := by
  convert Set.sum_indicator_subset f Finset.mem_of_mem_filter using 2 -- `with m hm` does not work
  sorry

After convert, the tactic state is

f: ℕ → ℂ
n x✝: ℕ
a✝: x✝ ∈ Finset.range n
⊢ Set.indicator {p | Nat.Prime p} f x✝ = Set.indicator (↑(Finset.filter (fun p ↦ Nat.Prime p) (Finset.range n))) f x✝

Trying to name the hidden variables by appending with m hm does not work: there is no error message, but the tactic state is the same as before. This looks like a bug to me.
(Of course, I can (and do) rename them via rename_i, but it should be possible to give them names through the call to convert.)

[Kyle Miller]

Yes, there's some sort of bug in with that I've noticed and haven't tracked down yet. Here's a workaround:

convert Set.sum_indicator_subset f Finset.mem_of_mem_filter using 2 with _ _ m hm

[Michael Stoll]

The problem with this is that it will break once the bug is fixed...

[Kyle Miller]

I'm sorry for the bug (I wrote this feature), but there are at least a couple workarounds and you can decide which you want to use.

At least if you use _'s you can delete them once the bug is fixed. The bug seems to be that the with clause variables get unnecessarily consumed.

[Scott Morrison]

The advantage of something breaking once a bug is fixed is that we are not stuck with the workaround forever!