tactic for rearrange terms?

Stream: Is there code for X?

[Casavaca]

I want to proof something like a b c d e p q s : R, a * b * c * d * e < p * q * e * d * s. Suppose I want to apply

theorem mul_lt_mul_of_pos_left [...] (bc : b < c) (a0 : 0 < a) :
a * b < a * c

and transform the goal into a * b * c * d < p * q * d * s and 0 < e.

Then apply again on d to turn the goal into a * b * c < p * q * s and 0 < d

Is there a tactic to free me from always reorder the terms manually?

Thanks.

[Yaël Dillies]

Try gcongr _ * _ * _ * ?_ * ?_

[Kevin Buzzard]

What is R? Can you write a #mwe if Yael's suggestion doesn't answer your question?

[Kyle Miller]

There's also convert_to to create equalities that you could prove with ring. The using clause tells convert_to the depth at which it should stop trying to pull things apart.

example (a b c d e p q s : ℝ) :
    a * b * c * d * e < p * q * e * d * s := by
  convert_to e * (a * b * c * d) < e * (p * q * d * s) using 1
  · ring
  · ring
  apply mul_lt_mul_of_pos_left
  /-
  case bc
  a b c d e p q s : ℝ
  ⊢ a * b * c * d < p * q * d * s

  case a0
  a b c d e p q s : ℝ
  ⊢ 0 < e
  -/

[Damiano Testa]

move_mul [e] should also move e to the far right (and using ←e moves it to the far left).

[Damiano Testa]

E.g.

import Mathlib

example (a b c d e p q s : ℝ) :
    a * b * c * d * e < p * q * e * d * s := by
  move_mul [e]   -- ⊢ a * b * c * d * e < p * q * d * s * e
  apply mul_lt_mul_of_pos_right
  /-
  case bc
  a b c d e p q s : ℝ
  ⊢ a * b * c * d < p * q * d * s

  case a0
  a b c d e p q s : ℝ
  ⊢ 0 < e
  -/

[Casavaca]

Thank you all. I meant "ℝ" when I typed R. move_mul is very useful because I don't have to manually locate the term by "gcongr _ * _ * _ * ?_ * ?_" or manually rewrite all the terms by "convert_to e * (a * b * c * d) < e * (p * q * d * s)".

[Casavaca]

I got another question:

How do I do this? Basically I want to make Lean merge the constants.

example {a b c d : ℝ} (h : (2 : ℝ) * a * ((2 : ℝ) * b) * ((2 : ℝ) * c) = d) : True := by
  -- h : 2 * a * (2 * b) * (2 * c) = d
  magic_norm_num at h
  -- h : (8 : ℝ) * (a * b * c) = d

[Damiano Testa]

Oh, I did not implement move_mul at? I think that I did in lean3.

Otherwise, maybe move_mul [a, b, c] at h; rw [show (2 : ℝ) * 2 * 2 = 8 by norm_num] at h would work?

(Even if it did, I agree that it is not ideal.)

[Damiano Testa]

There was a recent thread about a tactic for "collecting terms", but I'm on mobile now.

[Casavaca]

You're right. "collecting terms" wanted to achieve similar goal.
You did implement move_mul. In this case, it can be weird because if goal is "2 * a * 2 * a * 2 * a", you can't apply move_mul, it would say that 2 is already left_most, and a is already right most

[Damiano Testa]

Repetitions should be allowed and respected: move_mul [a, a, a] should do what you want.

[Damiano Testa]

(And it is a bug if it does not work: there is some care taken in "uniquifing" the input, to preserve multiplicities.)

[Damiano Testa]

I.e. move_mul [a, a] should not be the same as move_mul [a]; move_mul [a].

[Casavaca]

Thanks. move_mul [2, 2] worked, but we don't have move_mul ... at ... yet. It would be nice if we can have something like move_combine_constant.

[Damiano Testa]

Ok, I had at in Lean 3, but did not port it. The "combine constants" part I think that has never part of any tactic, though maybe it is part of the specs for ring. However, also ring does not support the at ... syntax.

[Damiano Testa]

import Mathlib

example {a b c d : ℝ} : (2 : ℝ) * a * ((2 : ℝ) * b) * ((2 : ℝ) * c) = d := by
  ring
  -- ⊢ a * b * c * 8 = d