simpNF says simp can prove something it can't

Stream: mathlib4

[Robert Maxton]

Sorry to crosspost, but as it's been a week since the last time I asked:

This PR (one of six 'helper' PRs for the PR constructing (co)limits in Quiv) doesn't pass CI because simpNF claims that simp can prove limitSubobjectProduct_π and its dual. However, when I actually try it locally, simp doesn't work on its own. Is this a false positive, or am I misunderstanding what the linter is telling me here?

[Maja Kądziołka]

Have you seen the full error message here: https://github.com/leanprover-community/mathlib4/actions/runs/14425381374/job/40453462576

[Maja Kądziołka]

also, does a simp with no modifiers make any progress on the left-hand side?

[Robert Maxton]

Maja Kądziołka said:

Have you seen the full error message here: https://github.com/leanprover-community/mathlib4/actions/runs/14425381374/job/40453462576

Yes, but it doesn't make much sense to me; I'm not even sure simp is using any of the Fan.mk_ etc lemmas in this proof.

[Robert Maxton]

Maja Kądziołka said:

also, does a simp with no modifiers make any progress on the left-hand side?

A simp with no modifiers makes no progress without unfolding limitSubobjectProduct.

[Jovan Gerbscheid]

simp can prove limitSubobjectProduct_π as claimed in the error message, but it needs to use limitSubobjectProduct_eq_lift, which is defined after it. That's why it didn't work when you tried to solve it with simp. So I think the simpNF linter is correctly complaining.

[Robert Maxton]

Er.... Well, yes. But the proof of limitSubobjectProduct_eq_lift itself makes use of limitSubobjectProduct_π; removing the simp from limitSubobjectProduct_π makes the former proof not go through.

[Jovan Gerbscheid]

If you can't just pass the lemma directly to simp, you can use @[local simp] so that the simp tag is only used in this file

[Robert Maxton]

Mmm. I suppose I can do that, yeah. Seems a little backward but I guess it marginally reduces the number of simp lemmas

[Bolton Bailey]

I am also experiencing a problem where the simpNF linter is telling me a simp lemma can be proved by simp in this run. But in my case, I can't use the simp call that the linter provides, because one of the lemmas being called is exactly the lemma that comes immediately after, that I am using this lemma to prove. What am I supposed to do about this?

[Aaron Liu]

In that case, one of the lemmas should not be @[simp]

[Bolton Bailey]

It feels to me that both should be simp, In both cases the RHS is much more complicated. Which one shouldn't be simp?

@[simp]
theorem map_univ_comp_coe {β : Type*} (m : Multiset α) (f : α → β) :
    ((Finset.univ : Finset m).val.map (f ∘ (fun x : m ↦ (x : α)))) = m.map f := by
  rw [← Multiset.map_map, Multiset.map_univ_coe]

@[simp]
theorem map_univ {β : Type*} (m : Multiset α) (f : α → β) :
    ((Finset.univ : Finset m).val.map fun (x : m) ↦ f (x : α)) = m.map f := by
  simp_rw [← Function.comp_apply (f := f)]
  exact map_univ_comp_coe m f

[Jovan Gerbscheid]

The lemma that the simpNF linter points out (the first one) should not be simp, since it is redundant.

The fact that Function.comp_apply is actually applied here by simp seems very surprising, but it can be explained by the congr lemma Multiset.map_congr