int.coe_nat_max

Stream: maths

[Kevin Buzzard]

I don't think int.coe_nat_max : {m n : ℕ} : (↑(max m n) : ℤ) = max m n is in mathlib, and I needed it today. Kenny produced this proof:

theorem int.coe_nat_max {m n : ℕ} : (↑(max m n) : ℤ) = max m n :=
begin
  unfold max,simp [int.coe_nat_le],
  split_ifs;refl,
end

but I was thinking that the result probably lived near the beginning of data.int.basic and I'm not sure that the devs will want split_ifs to be used in such a low-level file. Should it go later on or should we think of a more low-level proof? (or is it there already?)

[Mario Carneiro]

I agree this belongs in data.int.basic, and there is no problem using split_ifs. The mathlib tactics are all very low in the dependency order so that mathlib can use them