Variable expansion in filter_upwards

Stream: mathlib4

[Sebastien Gouezel]

In complicated proofs, I try to hide some complexity behind local definitions given with let. Unfortunately, a few tactics expand automatically the let, leaving a very heavy goal state. This has been discussed about simp recently, but another example is filter_upwards. In

import Mathlib.Probability.IdentDistrib

lemma foo : ∀ᶠ n in (Filter.atTop : Filter ℕ), True := by
  let φ : ℕ → ℕ := fun n ↦ 3 * n + 17
  have : ∀ᶠ n in Filter.atTop, φ n = 0 := sorry
  filter_upwards [this] with n hn
  trivial

after the filter_upwards line I would expect hn to be φ n = 0, but the φ has been expanded and it is instead 3 * n + 17 = 0. This is not a problem in this example, but it can be quite unpleasant in real-life examples. Is this something that would be easily fixable, or do I just have to live with it?

[Heather Macbeth]

I've been using a lot of clear_value φ to deal with this kind of thing. (Not with filter_upwards -- in fact I can't remember which tactics I've needed it for, but I agree with your impression that it is several of them.)

[Heather Macbeth]

It's not a good solution.

[Patrick Massot]

I tried a blind fix at https://github.com/leanprover-community/mathlib4/commit/06900385e7bfb123eeb6cfc56145c82f218dc743 on branch pm_filter_zeta. Let's see how CI likes it.

[Patrick Massot]

Fixed at #7213

[Heather Macbeth]

I think field_simp might be one of the other tactics with this problem -- anyone want to experiment with removing zeta-reduction there?

[Patrick Massot]

Do you have a test case?

[Patrick Massot]

I created a branch https://github.com/leanprover-community/mathlib4/tree/field_simp_zeta with a very naive fix attempt.

[Heather Macbeth]

I have a feeling that some of @Matthew Ballard's porting notes about field_simp in Geometry.Manifold.Instances.Sphere could be resolved by fixing this.

[Heather Macbeth]

I guess the test would be to change back the proofs from the port-adjusted versions to the original mathlib3 proofs.