prove Multiset.map produces no duplicates under local inject

Stream: new members

[Nick_adfor]

What's the standard approach in Mathlib to prove Nodup in this scenario? Specifically, how do I properly leverage the injectivity hypothesis that's only on the finite subset Fin n when working with multisets?

lemma range_n_nodup_of_fin_injective (n : ℕ) (f : ℕ → ℝ) (h : Function.Injective (fun (i : Fin n) => f i)) :
    (Multiset.map f (Multiset.range n)).Nodup := by sorry

[Aaron Liu]

docs#Multiset.Nodup.map_on

[Nick_adfor]

I've finished but found an interesting thing:

import Mathlib

open Real

lemma range_n_nodup_of_fin_injective (n : ℕ) (f : ℕ → ℝ) (h : Function.Injective (fun (i : Fin n) => f i)) :
    (Multiset.map f (Multiset.range n)).Nodup := by
  have h_range_nodup : (Multiset.range n).Nodup := by
    simp [Multiset.nodup_range]
  refine h_range_nodup.map_on fun x hx y hy hfxy => ?_
  rw [Multiset.mem_range] at hx hy
  let x' : Fin n := ⟨x, hx⟩
  let y' : Fin n := ⟨y, hy⟩
  exact?

[Nick_adfor]

This exact? show me:

found a proof, but the corresponding tactic failed:
  (expose_names; exact Fin.mk.inj_iff.mp (h hfxy))

It may be possible to correct this proof by adding type annotations, explicitly specifying implicit arguments, or eliminating unnecessary function abstractions.

in the earlier version, it would show:

Try this: exact Fin.mk.inj_iff.mp (h hfxy)

but cannot run with error

don't know how to synthesize implicit argument 'a'
  @Iff.mp (⟨x, ?m.22979⟩ = ⟨y, ?m.22980⟩) (x = y) Fin.mk.inj_iff (h hfxy)

[Nick_adfor]

I'm wondering how exact? works. Before that I always think exact? will conclude the proof but today my faith destroys.

[Aaron Liu]

You can probably repair this proof

[Aaron Liu]

probably what happened is that exact? found a working proof but the pretty printer was not able to preserve all of that information

[Aaron Liu]

yeah if you do

  exact @Iff.mp (x' = y') (x = y) Fin.mk.inj_iff (h hfxy)

then it works

[Nick_adfor]

Aaron Liu said:

yeah if you do

  exact @Iff.mp (x' = y') (x = y) Fin.mk.inj_iff (h hfxy)

then it works

@Iff.mp (x' = y') (x = y) : ((x' = y') ↔ (x = y)) → (x' = y') → (x = y)

The exact? tactic can vaguely recognize this part, but cannot write it out accurately. On the contrary, it hides them.

[Kevin Buzzard]

Yes I have seen exact? do this expose_names thing before and it's usually due to some issue with variables. I use the same workaround that Aaron is suggesting (in fact sometimes just deleting the expose_names fixes it, but sometimes you have to engage your brain by looking at what exact? found).