feat(order/bounded_lattice): min/max commute with coe (#6900)

to with_bot and with_top





Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>

src/order/bounded_lattice.lean

@@ -586,6 +586,14 @@ by rw [← sup_eq_max, lattice_eq_DLO]
 theorem inf_eq_min [linear_order α] (x y : with_bot α) : x ⊓ y = min x y :=
 by rw [← inf_eq_min, lattice_eq_DLO]
 
+@[norm_cast] -- this is not marked simp because the corresponding with_top lemmas are used
+lemma coe_min [linear_order α] (x y : α) : ((min x y : α) : with_bot α) = min x y :=
+by simp [min, ite_cast]
+
+@[norm_cast] -- this is not marked simp because the corresponding with_top lemmas are used
+lemma coe_max [linear_order α] (x y : α) : ((max x y : α) : with_bot α) = max x y :=
+by simp [max, ite_cast]
+
 instance order_top [order_top α] : order_top (with_bot α) :=
 { top := some ⊤,
   le_top := λ o a ha, by cases ha; exact ⟨_, rfl, le_top⟩,
@@ -815,6 +823,14 @@ by rw [← sup_eq_max, lattice_eq_DLO]
 theorem inf_eq_min [linear_order α] (x y : with_top α) : x ⊓ y = min x y :=
 by rw [← inf_eq_min, lattice_eq_DLO]
 
+@[simp, norm_cast]
+lemma coe_min [linear_order α] (x y : α) : ((min x y : α) : with_top α) = min x y :=
+by simp [min, ite_cast]
+
+@[simp, norm_cast]
+lemma coe_max [linear_order α] (x y : α) : ((max x y : α) : with_top α) = max x y :=
+by simp [max, ite_cast]
+
 instance order_bot [order_bot α] : order_bot (with_top α) :=
 { bot := some ⊥,
   bot_le := λ o a ha, by cases ha; exact ⟨_, rfl, bot_le⟩,