argument order of `peel h with ...`

Stream: mathlib4

[Patrick Massot]

About the main proof above: @Jireh Loreaux I am always confused by the ordering in the with clause of peel. Is there a rational explanation or is the implementation making it random?

[Jireh Loreaux]

I don't think I understand the question. Can you provide a mwe with the goal state before and after and what you find "random" about it?

[Patrick Massot]

The above example is a #mwe, although it could be minimized more.

[Patrick Massot]

It has this: ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ Metric.closedBall 0 i → ‖f x‖ ≤ c and the goal is ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ Metric.closedBall 0 i → ∀ y ∈ Ι 0 x.im, ‖f (↑x.re + ↑y * I)‖ ≤ c.

[Patrick Massot]

The correct argument order in peel is hi i i_pos which feels completely random.

[Patrick Massot]

where i is i, i_pos : 0 < i and hi : ∀ ⦃x : ℂ⦄, x ∈ Metric.closedBall 0 i → ‖f x‖ ≤ c.

[Patrick Massot]

The order I would expect is i i_pos hi.

[Johan Commelin]

How can i come after hi if hi depends on i?

[Jireh Loreaux]

Thanks, I see what you mean now.

[Patrick Massot]

Johan, this is only a sequence of names at the time you call the tactic.

[Johan Commelin]

Ooh, right, I see it now

[Jireh Loreaux]

So, the rule is that the hypothesis comes first and all the variables introduced come after. I think it might be easily switched, but I'd need to review the implementation. I think I originally wrote it this way for simplicity of the recursion when applying peel a number of times equal to the number of variables introduced.

[Jireh Loreaux]

It's easy, I'll PR shortly.

[Jireh Loreaux]

@Patrick Massot #9413

[Patrick Massot]

Thanks. I don't really know how to make sure other users agree with me.

[Patrick Massot]

How many uses of peel did you find in Mathlib?

[Jireh Loreaux]

only one, and I think it was mine!

[Notification Bot]

17 messages were moved here from #Is there code for X? > pulling continuity past integrals by Jireh Loreaux.

[Kevin Buzzard]

I use it in my undergraduate course to prove things like if a(n) tends to L then -a(n) tends to -L.

[Jireh Loreaux]

@Kevin Buzzard how do you feel about this swap in the argument order for the with clause?

[Mario Carneiro]

I had to read up on the tactic definition because I missed when this tactic was introduced, but after having done so I agree with Patrick, the h should come last

[Kevin Buzzard]

Feel free to fiddle with it

[Patrick Massot]

This is good enough for me but Kyle left a request on GitHub.