Beginner code reviewing / mentor

Stream: new members

[Nicolas Rolland]

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]

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]

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]

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]

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