feat(order/lattice, order/lattice_intervals): coe inf/sup lemmas (#15136

)

This PR adds simp lemmas for coercions of inf/sup in order instances on intervals. We also change the order of some arguments in instances/lemmas, by removing `variables` commands, so that typeclass arguments precede others. 



Co-authored-by: Peter Nelson <apnelson@uwaterloo.ca>

src/order/lattice.lean

@@ -974,6 +974,24 @@ protected def lattice [lattice α] {P : α → Prop}
   lattice {x : α // P x} :=
 { ..subtype.semilattice_inf Pinf, ..subtype.semilattice_sup Psup }
 
+@[simp, norm_cast] lemma coe_sup [semilattice_sup α] {P : α → Prop}
+  (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y)) (x y : subtype P) :
+  (by {haveI := subtype.semilattice_sup Psup, exact (x ⊔ y : subtype P)} : α) = x ⊔ y := rfl
+
+@[simp, norm_cast] lemma coe_inf [semilattice_inf α] {P : α → Prop}
+  (Pinf : ∀⦃x y⦄, P x → P y → P (x ⊓ y)) (x y : subtype P) :
+  (by {haveI := subtype.semilattice_inf Pinf, exact (x ⊓ y : subtype P)} : α) = x ⊓ y := rfl
+
+@[simp] lemma mk_sup_mk [semilattice_sup α] {P : α → Prop} (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y))
+  {x y : α} (hx : P x) (hy : P y) :
+  (by {haveI := subtype.semilattice_sup Psup, exact (⟨x, hx⟩ ⊔ ⟨y, hy⟩ : subtype P)}) =
+    ⟨x ⊔ y, Psup hx hy⟩ := rfl
+
+@[simp] lemma mk_inf_mk [semilattice_inf α] {P : α → Prop} (Pinf : ∀⦃x y⦄, P x → P y → P (x ⊓ y))
+  {x y : α} (hx : P x) (hy : P y) :
+  (by {haveI := subtype.semilattice_inf Pinf, exact (⟨x, hx⟩ ⊓ ⟨y, hy⟩ : subtype P)}) =
+    ⟨x ⊓ y, Pinf hx hy⟩ := rfl
+
 end subtype
 
 section lift

src/order/lattice_intervals.lean

@@ -32,13 +32,12 @@ namespace set
 
 namespace Ico
 
-variables {a b : α}
-
-instance [semilattice_inf α] : semilattice_inf (Ico a b) :=
+instance [semilattice_inf α] {a b : α} : semilattice_inf (Ico a b) :=
 subtype.semilattice_inf (λ x y hx hy, ⟨le_inf hx.1 hy.1, lt_of_le_of_lt inf_le_left hx.2⟩)
 
 /-- `Ico a b` has a bottom element whenever `a < b`. -/
-@[reducible] protected def order_bot [partial_order α] (h : a < b) : order_bot (Ico a b) :=
+@[reducible] protected def order_bot [partial_order α] {a b : α} (h : a < b) :
+  order_bot (Ico a b) :=
 (is_least_Ico h).order_bot
 
 end Ico
@@ -52,83 +51,78 @@ end Iio
 
 namespace Ioc
 
-variables {a b : α}
-
-instance [semilattice_sup α] : semilattice_sup (Ioc a b) :=
+instance [semilattice_sup α] {a b : α} : semilattice_sup (Ioc a b) :=
 subtype.semilattice_sup (λ x y hx hy, ⟨lt_of_lt_of_le hx.1 le_sup_left, sup_le hx.2 hy.2⟩)
 
 /-- `Ioc a b` has a top element whenever `a < b`. -/
-@[reducible] protected def order_top [partial_order α] (h : a < b) : order_top (Ioc a b) :=
+@[reducible] protected def order_top [partial_order α] {a b : α} (h : a < b) :
+  order_top (Ioc a b) :=
 (is_greatest_Ioc h).order_top
 
 end Ioc
 
-namespace Iio
+namespace Ioi
 
 instance [semilattice_sup α] {a : α} : semilattice_sup (Ioi a) :=
 subtype.semilattice_sup (λ x y hx hy, lt_of_lt_of_le hx le_sup_left)
 
-end Iio
+end Ioi
 
 namespace Iic
 
-variables {a : α}
-
-instance [semilattice_inf α] : semilattice_inf (Iic a) :=
+instance [semilattice_inf α] {a : α} : semilattice_inf (Iic a) :=
 subtype.semilattice_inf (λ x y hx hy, le_trans inf_le_left hx)
 
-instance [semilattice_sup α] : semilattice_sup (Iic a) :=
+instance [semilattice_sup α] {a : α} : semilattice_sup (Iic a) :=
 subtype.semilattice_sup (λ x y hx hy, sup_le hx hy)
 
-instance [lattice α] : lattice (Iic a) :=
+instance [lattice α] {a : α} : lattice (Iic a) :=
 { .. Iic.semilattice_inf,
   .. Iic.semilattice_sup }
 
-instance [preorder α] : order_top (Iic a) :=
+instance [preorder α] {a : α} : order_top (Iic a) :=
 { top := ⟨a, le_refl a⟩,
   le_top := λ x, x.prop }
 
 @[simp] lemma coe_top [preorder α] {a : α} : ↑(⊤ : Iic a) = a := rfl
 
-instance [preorder α] [order_bot α] : order_bot (Iic a) :=
+instance [preorder α] [order_bot α] {a : α} : order_bot (Iic a) :=
 { bot := ⟨⊥, bot_le⟩,
   bot_le := λ ⟨_,_⟩, subtype.mk_le_mk.2 bot_le }
 
 @[simp] lemma coe_bot [preorder α] [order_bot α] {a : α} : ↑(⊥ : Iic a) = (⊥ : α) := rfl
 
-instance [preorder α] [order_bot α] : bounded_order (Iic a) :=
+instance [preorder α] [order_bot α] {a : α} : bounded_order (Iic a) :=
 { .. Iic.order_top,
   .. Iic.order_bot }
 
 end Iic
 
 namespace Ici
 
-variables {a : α}
-
-instance [semilattice_inf α] : semilattice_inf (Ici a) :=
+instance [semilattice_inf α] {a : α}: semilattice_inf (Ici a) :=
 subtype.semilattice_inf (λ x y hx hy, le_inf hx hy)
 
-instance [semilattice_sup α] : semilattice_sup (Ici a) :=
+instance [semilattice_sup α] {a : α} : semilattice_sup (Ici a) :=
 subtype.semilattice_sup (λ x y hx hy, le_trans hx le_sup_left)
 
-instance [lattice α] : lattice (Ici a) :=
+instance [lattice α] {a : α} : lattice (Ici a) :=
 { .. Ici.semilattice_inf,
   .. Ici.semilattice_sup }
 
-instance [preorder α] : order_bot (Ici a) :=
+instance [preorder α] {a : α} : order_bot (Ici a) :=
 { bot := ⟨a, le_refl a⟩,
   bot_le := λ x, x.prop }
 
 @[simp] lemma coe_bot [preorder α] {a : α} : ↑(⊥ : Ici a) = a := rfl
 
-instance [preorder α] [order_top α] : order_top (Ici a) :=
+instance [preorder α] [order_top α] {a : α}: order_top (Ici a) :=
 { top := ⟨⊤, le_top⟩,
   le_top := λ ⟨_,_⟩, subtype.mk_le_mk.2 le_top }
 
 @[simp] lemma coe_top [preorder α] [order_top α] {a : α} : ↑(⊤ : Ici a) = (⊤ : α) := rfl
 
-instance [preorder α] [order_top α] : bounded_order (Ici a) :=
+instance [preorder α] [order_top α] {a : α}: bounded_order (Ici a) :=
 { .. Ici.order_top,
   .. Ici.order_bot }