## 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

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)) ]
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


#### 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 min_le_left
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


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