Using `conv` with binders on finsum

Stream: mathlib4

[Eric Wieser]

Is there a mechanism for hooking custom congruence lemmas into conv? How can I tell it to use docs#finsum_congr_Prop in the following?

import Mathlib

open scoped BigOperators

example : ∑ᶠ (i : ℕ) (h : i < 3), i = 3 := by
  conv =>
    enter [1, 1, i]
    -- goal: | ∑ᶠ (_ : i < 3), i
    skip
    -- how do I get my goal to be `| i < 3` via `finsum_congr_Prop`?
  sorry

[Eric Wieser]

rw [finsum_congr_Prop _ fun x => rfl] is close, but it leaves me with a metavariable that I want conv to absorb

[Kyle Miller]

It's clunky, but you can do

example : ∑ᶠ (i : ℕ) (h : i < 3), i = 3 := by
  conv =>
    enter [1, 1, i]
    apply finsum_congr_Prop
    tactic => intro; rfl
    skip
    -- | i < 3

or

example : ∑ᶠ (i : ℕ) (h : i < 3), i = 3 := by
  conv =>
    enter [1, 1, i]
    apply finsum_congr_Prop _ (fun _ => rfl)
    -- | i < 3

[Kyle Miller]

(To a first approximation, congr just does apply with a congruence lemma.)

[Kyle Miller]

There's no mechanism for custom congruence lemmas yet though. I think only the congr! tactic (and tactics using congr!) is the only use of them outside of simp.

[Eric Wieser]

That second example doesn't work for me, there's a stray ⊢ ℕ → Prop that comes first

[Kyle Miller]

Weird, something changed in the last week of mathlib (or Lean? I don't know, I was on nightly-testing I think)

[Kyle Miller]

This does the right thing:

    apply finsum_congr_Prop
    tactic => intro; rfl

[Kyle Miller]

Anyway, I'd like to see conv have some tactics for applying a @[congr] lemma, maybe that could be congr itself, so enter would gain that power.