From 108fa6f305a5280f1ea67012a4c4094759c9b587 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 6 Apr 2021 01:49:47 +0000 Subject: [PATCH] feat(order/bounded_lattice): min/max commute with coe (#6900) to with_bot and with_top Co-authored-by: Floris van Doorn --- src/order/bounded_lattice.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/order/bounded_lattice.lean b/src/order/bounded_lattice.lean index bd03ff475b09d..190a9fabed457 100644 --- a/src/order/bounded_lattice.lean +++ b/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⟩,