# Zulip Chat Archive

## Stream: new members

### Topic: Style feedback

#### Martin C. Martin (Feb 02 2023 at 18:42):

Section 2.5 in "Mathematics in Lean" has us prove:

`(h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c `

Here's my proof, but it feels a little verbose and awkward. Is there a simpler / more readable / more canonical proof?

```
variables {R : Type*} [ordered_ring R]
variables a b c : R
example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
begin
nth_rewrite 0 ← add_zero (a * c),
have h1 : b * c = a * c + (b - a) * c,
by noncomm_ring,
rw h1,
apply add_le_add_left,
apply mul_nonneg,
{ simp, exact h },
exact h'
end
```

#### Kevin Buzzard (Feb 02 2023 at 20:09):

What are the types of a,b,c?

#### Martin C. Martin (Feb 02 2023 at 20:36):

(Edit: Actually, an `ordered_ring`

.) Sorry, updated. They're in a `metric_space`

.

#### Martin C. Martin (Feb 02 2023 at 20:44):

I just noticed that Mathematics in Lean comes with solutions! Here's their solution to the problem:

```
theorem aux1 : a ≤ b → 0 ≤ b - a :=
begin
intro h,
rw [←sub_self a, sub_eq_add_neg, sub_eq_add_neg, add_comm, add_comm b],
apply add_le_add_left h
end
theorem aux2 : 0 ≤ b - a → a ≤ b :=
begin
intro h,
rw [←add_zero a, ←sub_add_cancel b a, add_comm (b - a)],
apply add_le_add_left h
end
example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
begin
have h1 : 0 ≤ (b - a) * c,
{ exact mul_nonneg (aux1 _ _ h) h' },
rw sub_mul at h1,
exact aux2 _ _ h1
end
```

#### Jireh Loreaux (Feb 02 2023 at 20:49):

Not a `metric_space`

(at least not by itself), there's no `dist`

here. It's an `ordered_ring R`

with `a b c : R`

#### Jireh Loreaux (Feb 02 2023 at 20:51):

Note that the solutions named the first two `example`

s (and changed to `theorem`

) so that they could be used in the proof of the third one.

#### Martin C. Martin (Feb 02 2023 at 20:51):

Ugh! Sorry, I got it mixed up with the next question. :) Yes, this is an ordered_ring, I updated my example.

#### Jireh Loreaux (Feb 02 2023 at 21:02):

Here are a few ways I would consider doing it (of course, the last one is cheating in some sense). Note that `sub_nonneg`

is an `↔`

combining `aux1`

and `aux2`

. the `positivity`

tactic is pretty cool in case you haven't learned about it yet.

```
import tactic.positivity
variables {R : Type*} [ordered_ring R]
variables a b c : R
example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
begin
rw ←sub_nonneg at h ⊢,
rw ←sub_mul,
exact mul_nonneg h h',
end
example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
begin
rw ←sub_nonneg at h ⊢,
rw ←sub_mul,
positivity,
end
example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
mul_le_mul_of_nonneg_right h h'
```

#### Martin C. Martin (Feb 03 2023 at 18:19):

Thanks, those are much better! And I hadn't heard of the positivity tactic, thanks for the tip.

#### Martin C. Martin (Feb 03 2023 at 18:32):

When working forward (i.e. adding new things to the context from what we already know, as opposed to working backward from the goal), is there a way to add a hypothesis without stating it's type? For example, in

```
variables {X : Type*} [metric_space X]
variables x y z : X
example (x y : X) : 0 ≤ dist x y :=
begin
have h1 : dist x x ≤ (dist x y) + (dist y x),
{ exact dist_triangle x y x},
sorry
end
```

that's kind of a lot of typing to just say h1 is `dist_triangle x y x`

.

#### Kyle Miller (Feb 03 2023 at 18:34):

You probably can do `have h1 := dist_triangle x y x`

here

#### Ruben Van de Velde (Feb 03 2023 at 18:37):

```
variables {X : Type*} [metric_space X]
variables x y z : X
example (x y : X) : 0 ≤ dist x y :=
begin
have h1 := dist_triangle x y x,
sorry
end
```

#### Martin C. Martin (Feb 03 2023 at 18:43):

Dude! So the ": type" is optional, I thought I tried leaving that out and it didn't work, but it's working now. :) It seems also `have h1 :=`

is the same as `have h1, from`

?

#### Martin C. Martin (Feb 03 2023 at 18:49):

.

#### Jireh Loreaux (Feb 03 2023 at 19:30):

It's optional if Lean can infer the type from the term you provided. Sometimes this doesn't work if the term you provided has metavariables.

#### Jireh Loreaux (Feb 03 2023 at 19:31):

Although on second thought, I think it still "works" it's just that `h1`

is pretty useless because it has metavariables in its type.

#### Kevin Buzzard (Feb 03 2023 at 19:35):

Although it's not great style, `h1`

is not useless if it has metavariables in its type -- you can sometimes just continue and they'll be unified later on (and the random non-Prop goals will magically disappear).

#### Jireh Loreaux (Feb 03 2023 at 19:56):

This is sometimes true, but in practice I frequently find that unification fails in those situations.

#### Jireh Loreaux (Feb 03 2023 at 19:57):

Maybe this is because the metavariables I have include some TC goals that depend on how they unify? I'm not sure, I don't have an example at hand.

Last updated: Dec 20 2023 at 11:08 UTC