# Zulip Chat Archive

## Stream: new members

### Topic: Match lhs and rhs of inequality

#### Kunhao Zheng (Jun 10 2021 at 09:17):

Hello! Currently I am trying to formalizing some inequality exercises involving amgm. Here is the first draft that works.

```
import data.real.basic
import analysis.mean_inequalities
import analysis.special_functions.pow
theorem algebra_amgm2_a2oncpc2onbpb2onaleqa3conb3pb3aonc3pc3bona3
(a b c : ℝ)
(h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
a^2 / c + c^2 / b + b^2 / a ≤ a^3 * c / b^3 + b^3 * a / c^3 + c^3 * b / a^3 :=
begin
have ha₃ := pow_pos h₀.1 3,
have hb₃ := pow_pos h₀.2.1 3,
have hc₃ := pow_pos h₀.2.2 3,
have h₁ := le_of_lt (div_pos (mul_pos hb₃ h₀.1) hc₃),
have h₂ := le_of_lt (div_pos (mul_pos hc₃ h₀.2.1) ha₃),
have h₃ := le_of_lt (div_pos (mul_pos ha₃ h₀.2.2) hb₃),
have h₄ : (0:ℝ) ≤ 1 / 2, norm_num,
have h₅ : 1 / 2 + 1 / 2 = (1:ℝ), ring,
have h₆ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₁ h₂ h₅,
have h₇ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₁ h₃ h₅,
have h₈ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₂ h₃ h₅,
have h₉ := add_le_add (add_le_add h₇ h₈) h₆,
clear h₆ h₇ h₈,
have lhs : (b^3 * a / c^3)^((1:ℝ) / 2) * (a^3 * c / b^3)^((1:ℝ) / 2) +
(c^3 * b / a^3)^((1:ℝ) / 2) * (a^3 * c / b^3)^((1:ℝ) / 2) +
(b^3 * a / c^3)^((1:ℝ) / 2) * (c^3 * b / a^3)^((1:ℝ) / 2) =
a^2 / c + c^2 / b + b^2 / a, {
simp only [←real.mul_rpow, h₁, h₂, h₃],
refine congr (congr_arg has_add.add _) _,
refine congr (congr_arg has_add.add _) _,
{
have pow_can₁: a^2 / c = ((a^2 / c) ^ ((2:ℕ):ℝ)) ^ ((1:ℝ) / 2), {
simp [←real.rpow_mul, le_of_lt (div_pos (pow_pos h₀.1 2) h₀.2.2)],
},
rw pow_can₁,
refine congr_fun (congr_arg pow _) _,
rw [real.rpow_nat_cast],
field_simp [ne_of_gt hb₃, ne_of_gt hc₃, pow_succ' c 2, ne_of_gt h₀.2.2, mul_div_cancel_left],
ring_nf,
},
{
have pow_can₂: c^2 / b = ((c^2 / b) ^ ((2:ℕ):ℝ)) ^ ((1:ℝ) / 2), {
simp [←real.rpow_mul, le_of_lt (div_pos (pow_pos h₀.2.2 2) h₀.2.1)],
},
rw pow_can₂,
refine congr_fun (congr_arg pow _) _,
rw [real.rpow_nat_cast],
field_simp [ne_of_gt ha₃, ne_of_gt hb₃, pow_succ' b 2, ne_of_gt h₀.2.1, mul_div_cancel_left],
ring_nf,
},
{
have pow_can₃: b^2 / a = ((b^2 / a) ^ ((2:ℕ):ℝ)) ^ ((1:ℝ) / 2), {
simp [←real.rpow_mul, le_of_lt (div_pos (pow_pos h₀.2.1 2) h₀.1)],
},
rw pow_can₃,
refine congr_fun (congr_arg pow _) _,
rw [real.rpow_nat_cast],
field_simp [ne_of_gt hc₃, ne_of_gt hb₃, pow_succ' a 2, ne_of_gt h₀.1, mul_div_cancel_left],
ring_nf,
},
},
have rhs : 1 / 2 * (b^3 * a / c^3) + 1 / 2 * (a^3 * c / b^3) +
(1 / 2 * (c^3 * b / a^3) + 1 / 2 * (a^3 * c / b^3)) +
(1 / 2 * (b^3 * a / c^3) + 1 / 2 * (c^3 * b / a^3)) =
a^3 * c / b^3 + b^3 * a / c^3 + c^3 * b / a^3, {
ring_nf,
},
rwa [←lhs, ←rhs],
end
```

The roadmap is to construct an inequality forwardly (h₉) then prove its lhs and rhs can simplify to the goal's. I have to state explicitly the lhs and rhs here because I didn't find any tactic that helps with this kind of situation, something like

```
import data.real.basic
lemma trans_le_trans
(a b c d : ℝ)
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d :=
begin
sorry
end
```

can help me use the `refine`

tactic to generate 2 subgoals of equalities. But I can only find tactic for 1 equality like `eq.trans_le`

. Also, my proof is very forward reasony so I wonder if you have any advice on the proof itself.

#### Sebastien Gouezel (Jun 10 2021 at 09:25):

```
import data.real.basic
lemma trans_le_trans
(a b c d : ℝ)
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d :=
begin
linarith,
end
```

#### Eric Wieser (Jun 10 2021 at 11:07):

Do we have docs#has_le.le.trans_eq?

#### Eric Wieser (Jun 10 2021 at 11:08):

`j.symm.le.trans (h.trans k.le)`

is a short term-mode proof

#### Johan Commelin (Jun 10 2021 at 11:14):

`j.symm.le`

is `j.ge`

#### Johan Commelin (Jun 10 2021 at 11:14):

But I guess we don't get a `trans`

then?

#### Johan Commelin (Jun 10 2021 at 11:16):

Of course `by rwa [j, k] at h`

also works

#### Damiano Testa (Jun 10 2021 at 11:17):

I find that what is below is closer to how I think of it:

```
import data.real.basic
lemma trans_le_trans
(a b c d : ℝ)
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d :=
begin
convert h, -- I know the correct inequality is this one
{ exact j.symm }, -- now fix it!
{ exact k.symm }
end
```

#### Damiano Testa (Jun 10 2021 at 11:19):

For increased opacity, this also works:

```
by convert h; exact eq.symm ‹_›
```

#### Damiano Testa (Jun 10 2021 at 11:20):

Although, while the term mode proofs that have been given earlier are probably closer to mathlib proofs (and also how I would write them), using `convert`

is often more "mathematical".

#### Damiano Testa (Jun 10 2021 at 11:22):

In particular, my impression is that the role of `h`

is *fundamental*, while the extra equalities are *noise*. Beginning a proof with `convert h`

is bringing the attention to what matters. After that, what is left is figuring out that you do indeed have the pieces of the puzzle.

#### Eric Wieser (Jun 10 2021 at 11:36):

You can also use the equation compiler for this type of thing:

```
import data.real.basic
lemma trans_le_trans : ∀
(a b c d : ℝ)
(j : a = c)
(k : b = d)
(h : a ≤ b),
c ≤ d
| _ _ _ _ rfl rfl h := h
```

#### Eric Wieser (Jun 10 2021 at 11:37):

But tactic#linarith is the best "I don't care about this stuff just solve it for me" solution.

#### Kunhao Zheng (Jun 10 2021 at 11:40):

Eric Wieser said:

You can also use the equation compiler for this type of thing:

`import data.real.basic lemma trans_le_trans : ∀ (a b c d : ℝ) (j : a = c) (k : b = d) (h : a ≤ b), c ≤ d | _ _ _ _ rfl rfl h := h`

could you please explain more about this syntax? I don't quite understand what's going on here (especially the `|`

and the `,`

after `(h : a ≤ b)`

)

#### Johan Commelin (Jun 10 2021 at 11:41):

@Kunhao Zheng Note that the is now a `\forall`

on the first line of the lemma

#### Johan Commelin (Jun 10 2021 at 11:41):

So the `,`

is just `\forall bla, blabla`

#### Yakov Pechersky (Jun 10 2021 at 11:46):

Also possible term mode is to use eq.subst, I think (k.subst (j.subst h)) will work. The rw triangle.

#### Yakov Pechersky (Jun 10 2021 at 11:49):

Regarding the proof and reverse reasoning, untested, but after you prove that the cubes are nonnegative, can you try field_simp? That should multiply everything out

#### Kunhao Zheng (Jun 10 2021 at 12:00):

Yakov Pechersky said:

Regarding the proof and reverse reasoning, untested, but after you prove that the cubes are nonnegative, can you try field_simp? That should multiply everything out

Now my proof looks like this:

```
import data.real.basic
import analysis.mean_inequalities
import analysis.special_functions.pow
lemma trans_le_trans
{a b c d : ℝ}
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d := k.subst(j.subst h)
lemma pow_two_pow_half
(a : ℝ)
(h : 0 < a) :
a = (a^2)^((1:ℝ) / 2) :=
begin
simp [←real.rpow_mul, le_of_lt h, ←real.rpow_nat_cast],
end
theorem algebra_amgm2_a2oncpc2onbpb2onaleqa3conb3pb3aonc3pc3bona3
(a b c : ℝ)
(h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
a^2 / c + c^2 / b + b^2 / a ≤ a^3 * c / b^3 + b^3 * a / c^3 + c^3 * b / a^3 :=
begin
have ha₃ := pow_pos h₀.1 3,
have hb₃ := pow_pos h₀.2.1 3,
have hc₃ := pow_pos h₀.2.2 3,
have h₁ := le_of_lt (div_pos (mul_pos hb₃ h₀.1) hc₃),
have h₂ := le_of_lt (div_pos (mul_pos hc₃ h₀.2.1) ha₃),
have h₃ := le_of_lt (div_pos (mul_pos ha₃ h₀.2.2) hb₃),
have h₄ : (0:ℝ) ≤ 1 / 2, norm_num,
have h₅ : 1 / 2 + 1 / 2 = (1:ℝ), ring,
have h₆ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₁ h₂ h₅,
have h₇ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₁ h₃ h₅,
have h₈ := real.geom_mean_le_arith_mean2_weighted h₄ h₄ h₂ h₃ h₅,
have h₉ := add_le_add (add_le_add h₇ h₈) h₆,
clear h₆ h₇ h₈,
refine trans_le_trans h₉ _ _,
{
simp only [←real.mul_rpow, h₁, h₂, h₃],
rw [pow_two_pow_half (a ^ 2 / c) _, pow_two_pow_half (c ^ 2 / b) _, pow_two_pow_half (b ^ 2 / a) _],
refine congr (congr_arg has_add.add _) _,
refine congr (congr_arg has_add.add _) _,
{
refine congr_fun (congr_arg pow _) _,
field_simp [ne_of_gt hb₃, ne_of_gt hc₃, pow_succ' c 2, ne_of_gt h₀.2.2, mul_div_cancel_left],
ring_nf,
},
{
refine congr_fun (congr_arg pow _) _,
field_simp [ne_of_gt ha₃, ne_of_gt hb₃, pow_succ' b 2, ne_of_gt h₀.2.1, mul_div_cancel_left],
ring_nf,
},
{
refine congr_fun (congr_arg pow _) _,
field_simp [ne_of_gt hc₃, ne_of_gt hb₃, pow_succ' a 2, ne_of_gt h₀.1, mul_div_cancel_left],
ring_nf,
},
exact div_pos (pow_pos h₀.2.1 2) h₀.1,
exact div_pos (pow_pos h₀.2.2 2) h₀.2.1,
exact div_pos (pow_pos h₀.1 2) h₀.2.2,
},
ring,
end
```

The line of `field_simp [ne_of_gt hb₃, ne_of_gt hc₃, pow_succ' c 2, ne_of_gt h₀.2.2, mul_div_cancel_left],`

helps me out to convert an equality of `b ^ 3 * a / c ^ 3 * (a ^ 3 * c / b ^ 3) = (a ^ 2 / c) ^ 2`

to `b ^ 3 * a * (a ^ 3 * c) * c ^ 2 = (a ^ 2) ^ 2 * (c ^ 2 * c * b ^ 3)`

. Not sure if this you're referring to?

#### Huỳnh Trần Khanh (Jun 10 2021 at 12:23):

Just wondering: what's with the absurdly long theorem name? Mathlib theorem names tend to encode the formal statement of the theorem and I understand that you want to follow that convention, however I think this is very extreme.

#### Huỳnh Trần Khanh (Jun 10 2021 at 12:24):

As a side note, I tend to call everything a lemma because I'm not a mathematician, LOL. Only mathematicians can prove theorems. I'm just a mere programmer knowing absolutely nothing about proper mathematics.

#### Huỳnh Trần Khanh (Jun 10 2021 at 12:25):

Even though I know how to prove this inequality :clown:

#### Kevin Buzzard (Jun 10 2021 at 12:25):

you won't like Lean 4 then :-)

#### Kunhao Zheng (Jun 10 2021 at 12:33):

Huỳnh Trần Khanh said:

Just wondering: what's with the absurdly long theorem name? Mathlib theorem names tend to encode the formal statement of the theorem and I understand that you want to follow that convention, however I think this is very extreme.

Somehow that's a naming convention we adapt from the metamath system to keep it aligned with statements written in that system (https://github.com/openai/miniF2F), I admit it's a bit tedious and longer but you could know what it tells us by reading the name. I once wanted to come up with another naming convention but I fell back into it:( so if you have any suggestions I will be very happy!

#### Johan Commelin (Jun 10 2021 at 12:39):

@Kunhao Zheng The mathlib name would probably be `sq_div_add_sq_div_add_sq_div_le`

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:22):

@Kunhao Zheng When you have a goal that can be closed simply by substituting variables, try `cc`

. The `cc`

(congruence closure) tactic is specifically designed for this.

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:23):

```
import data.real.basic
lemma trans_le_trans
(a b c d : ℝ)
(h : a ≤ b)
(j : a = c)
(k : b = d) :
c ≤ d := by cc
```

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:25):

The congruence closure tactic is based on the union-find data structure, which is very popular in competitive programming. You are from China, right? I know Chinese people are competitive programming gods!

#### Kunhao Zheng (Jun 10 2021 at 16:17):

Huỳnh Trần Khanh said:

The congruence closure tactic is based on the union-find data structure, which is very popular in competitive programming. You are from China, right? I know Chinese people are competitive programming gods!

Thank you for the hint! You're right. Though I have a CS background but I'm not so good at the competition :grinning_face_with_smiling_eyes:

Last updated: Dec 20 2023 at 11:08 UTC