help with dsimp

Stream: new members

[King Crawford]

I have this goal:
⊢ (λ (i : ℕ), ∃! (H : i ∈ finset.range n), ∑ (j : ℕ) in finset.range n, f j = f i) c
I want to beta reduce it to
⊢ ∃! (H : c ∈ finset.range n), ∑ (j : ℕ) in finset.range n, f j = f c
dsimp gives me the following which isn't quite what I'm looking for
⊢ ∃! (H : c ∈ finset.range n), (finset.range n).sum f = f c
Is there a way to do this?

[Johan Commelin]

You could show <your desired expression>

[Johan Commelin]

Or maybe dsimp only is slightly less aggressive?

[King Crawford]

dsimp only does the same thing unfortunately, but show worked. I didn't know about show. Thanks!

[Martin Dvořák]

Johan Commelin said:

You could show <your desired expression>

What is the difference between change and show for these purposes?

[Martin Dvořák]

King Crawford said:

I have this goal:
⊢ (λ (i : ℕ), ∃! (H : i ∈ finset.range n), ∑ (j : ℕ) in finset.range n, f j = f i) c
I want to beta reduce it to
⊢ ∃! (H : c ∈ finset.range n), ∑ (j : ℕ) in finset.range n, f j = f c
dsimp gives me the following which isn't quite what I'm looking for
⊢ ∃! (H : c ∈ finset.range n), (finset.range n).sum f = f c
Is there a way to do this?

I have had similar issues. I wish there was a command (or a rw lemma) that specifically performs the beta reduction.

[Johan Commelin]

@Martin Dvořák None. But change is more flexible. You can do change <foobar> at my_hyp,

[Martin Dvořák]

I have been using change on both the goal and hypotheses. I am glad that change exists but it is PITA to use it more than once per day.

[Yaël Dillies]

In fact, you can configure dsimp to perform whichever reduction you like.

[Martin Dvořák]

Can I keep dsimp as it is and create a new command bsimp for beta reductions only?