what is le_min doing here?

Stream: general

[Leni Greco]

i don't understand how le_min works at that place

example : min a b = min b a := by
apply le_antisymm
· show min a b ≤ min b a
apply le_min --what happens here
· apply min_le_right
apply min_le_left
· show min b a ≤ min a b
apply le_min
· apply min_le_right
apply min_le_left

at that place we go from the goal
min a b ≤ min b a
to the goal
min a b ≤ b

[Andrew Yang]

#backticks and #mwe

[Andrew Yang]

le_min has type x ≤ a → x ≤ b → x ≤ min a b. So applying it to a goal ?_ ≤ min b a creates two goals: ?_ ≤ b and ?_ ≤ a. (?_ is min a b in your case)

[Leni Greco]

thanks