# Zulip Chat Archive

## Stream: new members

### Topic: Beginner code reviewing / mentor

#### Nicolas Rolland (Aug 15 2023 at 19:34):

Is it appropriate to post code for review here ?

Or is there a better place somewhere for code critique

For instance, I am not sure of the style of the proof of the second example (from the wonderful "math in lean" material)

```
theorem aux : min a b + c ≤ min (a + c) (b + c) := by
apply le_min
apply add_le_add_right (min_le_left _ _)
apply add_le_add_right (min_le_right _ _)
example : min a b + c = min (a + c) (b + c) := by
apply le_antisymm
apply aux
have h : min (a + c) (b + c) ≤ min (a + c + -c) (b + c + -c) + c := by
rw [<- neg_add_cancel_right (min (a + c) (b + c)) ]
apply add_le_add_right (aux _ _ _)
have h' : min (a + c + -c) (b + c + -c) + c = min a b + c := by
rw [add_neg_cancel_right a c , add_neg_cancel_right b c]
linarith
```

#### Richard Copley (Aug 15 2023 at 19:53):

One thing is, you can use strict indentation to emphasize that multiple goals have been introduced and to focus on them one at a time. Another is that `exact`

emphasizes that a goal has been closed. I find this makes it easier to follow the proof structure. (This is coming from another beginner.)

```
theorem aux : min a b + c ≤ min (a + c) (b + c) := by
apply le_min
. exact add_le_add_right (min_le_left _ _)
. exact add_le_add_right (min_le_right _ _)
```

#### Thomas Browning (Aug 15 2023 at 20:04):

You can do it without subtraction:

```
example {T : Type*} [LinearOrderedAddCommMonoid T] {a b c : T} :
min a b + c = min (a + c) (b + c) := by
apply le_antisymm
· apply le_min
· apply add_le_add_right
apply min_le_left
· apply add_le_add_right
apply min_le_right
· rcases min_choice a b with h | h
· rw [h]
apply min_le_left
· rw [h]
apply min_le_right
```

#### Anatole Dedecker (Aug 15 2023 at 20:08):

This is the perfect place to ask for code review. It makes our life a little easier if you post a #mwe (including imports, open namespaces, variables, ...), so it would be nice if you did that in the future :wink:

#### Nicolas Rolland (Aug 15 2023 at 21:58):

Buster said:

One thing is, you can use strict indentation to emphasize that multiple goals have been introduced and to focus on them one at a time. Another is that

`exact`

emphasizes that a goal has been closed. I find this makes it easier to follow the proof structure. (This is coming from another beginner.)`theorem aux : min a b + c ≤ min (a + c) (b + c) := by apply le_min . exact add_le_add_right (min_le_left _ _) . exact add_le_add_right (min_le_right _ _)`

I think you have to fill all the arguments (possibly ywith `_`

) when using exact.

So that would give an extra `_`

at the end in my case

```
import Mathlib.Tactic
import Mathlib.Data.Real.Basic
variable (a b c d : ℝ)
theorem aux : min a b + c ≤ min (a + c) (b + c) := by
apply le_min
. exact add_le_add_right (min_le_left _ _) _
. exact add_le_add_right (min_le_right _ _) _
```

Last updated: Dec 20 2023 at 11:08 UTC