Transforming inequality in Reals to Q (or vice versa)

Stream: Analysis I

[Rado Kirov]

I got one of the proofs down to

M n: ℕ
q : ℕ → ℚ
hq : |q M - q n| ≤ (↑(M + 1) : ℚ)⁻¹
⊢ (↑|q M - q n| : Real) ≤ (↑(M + 1) : Real)⁻¹

(using pp.coersions.types true), but can't seem be able to transform the goal to be in Q and apply hq. This is after applying norm_cast on both.

[Ruben Van de Velde]

I would try to find a lemma that for a b : Rat, a ≤ b iff (a:Real) ≤ (b:Real) and use that on hq. And then hope that simpa finishes

[Rado Kirov]

I think I proved that here https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_5_4.lean#L1305-L1315

But I have two problems

1) very basic - but how to actually use Real.ratCast_ordered_hom: ℚ →+*o Real? Do I just rw [Real.ratCast_ordered_hom.monotone']?
2) more importantly, the cast on the RHS is before the ^-1, so I have to move it out first.

[Kim Morrison]

Do you know about rw?? It is often useful for suggesting lemma names for rewrites from the current goal, particularly when the current goal is relatively small.

[Terence Tao]

Presumably Real.inv_ratCast should help with (2). For (1) we have Real.lt_of_coe but one needs the variant Real.le_of_coe which doesn't currently exist, but it makes sense to add it (and Real.ge_of_coe too, for completeness). Real.ratCast_ordered_hom.monotone' is an implication, not an iff, so an apply (or perhaps a convert Real.ratCast_ordered_hom.monotone' _ _, in case things are not defeq enough) would be needed.

[Rado Kirov]

Do you know about rw?

Yes, I use it a lot together with exact? and apply?. It doesn't seem to show me anything useful in this case.

Screenshot 2025-09-11 at 7.38.03 AM.png

Presumably Real.inv_ratCast should help with (2).

Surprisingly it didn't directly. Took a bit to figure out why? Turns out in the original expression M + 1 is Nat, not Q, so there is no way to directly swap with ^-1.

This lead me to add rw [show (M:Real) = ((M:ℚ):Real) by rfl] (in earlier state, which is easier than M + 1 to state, because then one has to force the right version of +). Turns out after this simple change norm_cast closes the whole proof :partying_face:

[Rado Kirov]

On the meta level, I am running into a bunch of cases like this and this thread - #Is there code for X? > Tactic for stupid inequality . Basically:

• I have my high-powered tactics list - norm_num, linarith, simp, ring, field_simp etc.
• I get to some statement that has no meaningful mathematical content left (vague statement I know, just based on what one would write on paper)
• the high-powered tactics surprisingly fail to close the statement. Note there are only ~10 of them, so I can basically brute-force try them all.
• if nothing works, I have to start thinking, roughly what is the shape of the statement, which tactic I expect to solve it, how does it work, why doesn't it work here, and how can I find the appropriate small rw to get it going.

The last part is by far the hardest, because one has to understand much more precisely how these tactics works (I am thinking about reading the source code of linarith which has been the workhorse of chapter 5).

So far, I have been able to unblock myself on most of chapter 4 and 5 this way, but also wondering if I should be treating incorporating the small pre-step of rw as "bugs / feature requests" for incorporating in the tactic and filling them as issues somewhere, or reporting on zulip. What makes this tricky is everyone has slightly different expectation of how "high-powered" these tactics should be, so a bunch of these cases will be closed as "won't do" (which is fine by me, but don't want to create junk for the maintainers).

[Kim Morrison]

There's an intermediate option as well, in between bashing through everything repeatedly and writing new tactics: every time you encounter a problem that or simp or norm_cast should solve, but doesn't, make sure to add any missing attributes (PRs to Mathlib adding a single norm_cast attribute are very welcome!).

Polishing the annotations in existing libraries is extremely helpful.

[Rado Kirov]

That's a great point! Some tactics are externally extensible through annotations and sometimes the difference is just adding an annotation (much easier than extending the internals of the tactic). I still need to learn more about what makes a theorem good or bad candidate for the annotation, but that's easier than understanding internals.

Other than simp and norm_cast what are the other major tactics that work with annotations?

[Rado Kirov]

OOC, is there ever a downside to adding the annotation, if I can produce a reasonable example of a proof that gets shorter?

[Kim Morrison]

aesop and grind are also annotation driven.

Unfortunately, yes, for all of these there are downsides to bad annotations. For simp we have some reasonably well developed linters that warn about some bad classes. For grind we are still working on this.

Sometimes you just have to try. I'm generally supportive of "try adding the annotation and remove it again if something goes wrong".