Basic Inequality Manipulations in Analysis

Stream: new members

[Jineon Baek]

What is the idiomatic way to proceed with the following?

example (A B C D : ℝ)
    (h : A * B * C < A * B * D) (hA : 0 < A) (hB : 0 < B) : C < D := by
  sorry

In our context, A, B, C, D are large algebraic expressions and we don't want to say their names out a lot. Our approach was to dig mul_le_mul_left from LeanSearch and do

example (A B C D : ℝ)
    (h : A * B * C < A * B * D) (hA : 0 < A) (hB : 0 < B) : C < D := by
  apply (mul_lt_mul_left hB).mp
  apply (mul_lt_mul_left hA).mp
  rw [← mul_assoc, ← mul_assoc]
  exact h

but we feel that there should be some better way to handle such things. @Jaehyeon Seo

[Jineon Baek]

In general, we have tons of such typical 'chain of inequality' arguments in Analysis that we need to formalize, involving manipulating large chunks of expressions and suppressing subexpressions with larger terms etc. We seek for general guidance on how to handle such things.

[Aaron Liu]

simpa [hA, hB] using h solves your example. For manipulating large expressions I can think of a few solutions, but I don't do Analysis and this is not from experience.
1.
Just deal with it. Put the large term in your code, replacing it with _ as much as possible.
2.
Use let to have an abbreviation for your large term. Reference this abbreviation in your code, and use unfold to unfold it in your goal.
3.
Use def or abbrev to define your large term, and prove some stuff about it. Use rw or @[simp] your theorems to unfold it in your goal.

[Kevin Buzzard]

Does positivity or gcongr work?

[Luigi Massacci]

Note that hint also solves the whole thing in one go

[Luigi Massacci]

Suggesting simp_all only [mul_pos_iff_of_pos_left, mul_lt_mul_left]

[Luigi Massacci]

I couldn’t get positivity to work (but the only thing I tried was to rewrite the goal naively in positivity form with docs#sub_pos), gcongr worked as expected but needed a bit of contortion:

import Mathlib

example (A B C D : ℝ) (h : A * B * C < A * B * D) (hA : 0 < A) (hB : 0 < B) : C < D := by
  revert h
  contrapose!
  intro _
  gcongr

[Luigi Massacci]

aesop also closes the goal immediately (with the same suggestion as hint, I don’t know if aesop is itself registered as a hint tactic)

[Ruben Van de Velde]

Shorter:

import Mathlib

example (A B C D : ℝ) (h : A * B * C < A * B * D) (hA : 0 < A) (hB : 0 < B) : C < D := by
  contrapose! h
  gcongr

[Ruben Van de Velde]

It's unsurprising that gcongr doesn't solve it in the original direction, because it tries to split according to the structure of the goal

[Luigi Massacci]

I didn’t know you could do that :rolling_on_the_floor_laughing: In any case @Jineon Baek , this gcongr trick while it is not magic, does generalize a little bit. You can read more in the gcongr documentation, but in general if you have as goal a complicated inequality with some structure and want to prove it by destructing it into smaller pieces, gcongr is your friend. If you have it as an hypothesis and need to break it down to prove a simpler goal, reverse the two

[Luigi Massacci]

and before you try to be clever, don’t forget the bulldozer approach with aesop or hint (and for non-inequality analysis stuff, fun_prop will also be a relevant tank)