refactor(order/preorder_hom): golf and simp lemmas (#7429)

The main change here is to adjust `simps` to generate coercion lemmas rather than `.to_fun` for `preorder_hom`, which allows us to auto-generate some simp lemmas. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebraic_topology/simplex_category.lean

@@ -162,7 +162,7 @@ begin
     order_embedding.coe_of_strict_mono,
     function.comp_app,
     simplex_category.hom.to_preorder_hom_mk,
-    preorder_hom.comp_to_fun],
+    preorder_hom.comp_coe],
   rcases i with ⟨i, _⟩,
   rcases j with ⟨j, _⟩,
   rcases k with ⟨k, _⟩,
@@ -178,7 +178,7 @@ begin
     order_embedding.coe_of_strict_mono,
     function.comp_app,
     simplex_category.hom.to_preorder_hom_mk,
-    preorder_hom.comp_to_fun],
+    preorder_hom.comp_coe],
   rcases i with ⟨i, _⟩,
   rcases j with ⟨j, _⟩,
   split_ifs; { simp at *; linarith },
@@ -322,10 +322,13 @@ section skeleton
 
 /-- The functor that exhibits `simplex_category` as skeleton
 of `NonemptyFinLinOrd` -/
+@[simps obj map]
 def skeletal_functor : simplex_category ⥤ NonemptyFinLinOrd :=
 { obj := λ a, NonemptyFinLinOrd.of $ ulift (fin (a.len + 1)),
   map := λ a b f,
-    ⟨λ i, ulift.up (f.to_preorder_hom i.down), λ i j h, f.to_preorder_hom.monotone h⟩ }
+    ⟨λ i, ulift.up (f.to_preorder_hom i.down), λ i j h, f.to_preorder_hom.monotone h⟩,
+  map_id' := λ a, by { ext, simp, },
+  map_comp' := λ a b c f g, by { ext, simp, }, }
 
 lemma skeletal : skeletal simplex_category :=
 λ X Y ⟨I⟩,
@@ -341,12 +344,12 @@ namespace skeletal_functor
 
 instance : full skeletal_functor :=
 { preimage := λ a b f, simplex_category.hom.mk ⟨λ i, (f (ulift.up i)).down, λ i j h, f.monotone h⟩,
-  witness' := by { intros m n f, dsimp at *, ext1 ⟨i⟩, ext1, refl } }
+  witness' := by { intros m n f, dsimp at *, ext1 ⟨i⟩, ext1, ext1, cases x, simp, } }
 
 instance : faithful skeletal_functor :=
 { map_injective' := λ m n f g h,
   begin
-    ext1, ext1 i, apply ulift.up.inj,
+    ext1, ext1, ext1 i, apply ulift.up.inj,
     change (skeletal_functor.map f) ⟨i⟩ = (skeletal_functor.map g) ⟨i⟩,
     rw h,
   end }
@@ -365,9 +368,9 @@ instance : ess_surj skeletal_functor :=
     { rintro ⟨i⟩ ⟨j⟩ h, show f i ≤ f j, exact hf.monotone h, },
     { intros i j h, show f.symm i ≤ f.symm j, rw ← hf.le_iff_le,
       show f (f.symm i) ≤ f (f.symm j), simpa only [order_iso.apply_symm_apply], },
-    { ext1 ⟨i⟩, ext1, exact f.symm_apply_apply i },
-    { ext1 i, exact f.apply_symm_apply i },
-  end⟩⟩,}
+    { ext1, ext1 ⟨i⟩, ext1, exact f.symm_apply_apply i },
+    { ext1, ext1 i, exact f.apply_symm_apply i },
+  end⟩⟩, }
 
 noncomputable instance is_equivalence : is_equivalence skeletal_functor :=
 equivalence.equivalence_of_fully_faithfully_ess_surj skeletal_functor

src/order/category/Preorder.lean

@@ -20,7 +20,7 @@ instance : bundled_hom @preorder_hom :=
 { to_fun := @preorder_hom.to_fun,
   id := @preorder_hom.id,
   comp := @preorder_hom.comp,
-  hom_ext := @preorder_hom.coe_inj }
+  hom_ext := @preorder_hom.ext }
 
 attribute [derive [has_coe_to_sort, large_category, concrete_category]] Preorder
 

src/order/omega_complete_partial_order.lean

@@ -145,7 +145,7 @@ instance : has_le (chain α) :=
 { le := λ x y, ∀ i, ∃ j, x i ≤ y j  }
 
 /-- `map` function for `chain` -/
-@[simps] def map : chain β :=
+@[simps {fully_applied := ff}] def map : chain β :=
 f.comp c
 
 variables {f}
@@ -453,7 +453,7 @@ begin
   intro c,
   apply eq_of_forall_ge_iff, intro z,
   simp only [inf_le_iff, hf c, hg c, ωSup_le_iff, ←forall_or_distrib_left, ←forall_or_distrib_right,
-             chain.map_to_fun, function.comp_app, preorder_hom.has_inf_inf_to_fun],
+             function.comp_app, chain.map_coe, preorder_hom.has_inf_inf_coe],
   split,
   { introv h, apply h },
   { intros h i j,
@@ -467,7 +467,7 @@ lemma Sup_continuous (s : set $ α →ₘ β) (hs : ∀ f ∈ s, continuous f) :
 begin
   intro c, apply eq_of_forall_ge_iff, intro z,
   simp only [ωSup_le_iff, and_imp, preorder_hom.complete_lattice_Sup, set.mem_image,
-             chain.map_to_fun, function.comp_app, Sup_le_iff, preorder_hom.has_Sup_Sup_to_fun,
+             chain.map_coe, function.comp_app, Sup_le_iff, preorder_hom.has_Sup_Sup_coe,
              exists_imp_distrib],
   split; introv h hx hb; subst b,
   { apply le_trans _ (h _ _ hx rfl),
@@ -521,16 +521,16 @@ lemma top_continuous :
   continuous (⊤ : α →ₘ β) :=
 begin
   intro c, apply eq_of_forall_ge_iff, intro z,
-  simp only [ωSup_le_iff, forall_const, chain.map_to_fun, function.comp_app,
-             preorder_hom.has_top_top_to_fun],
+  simp only [ωSup_le_iff, forall_const, chain.map_coe, function.comp_app,
+             preorder_hom.has_top_top_coe],
 end
 
 lemma bot_continuous :
   continuous (⊥ : α →ₘ β) :=
 begin
   intro c, apply eq_of_forall_ge_iff, intro z,
-  simp only [ωSup_le_iff, forall_const, chain.map_to_fun, function.comp_app,
-             preorder_hom.has_bot_bot_to_fun],
+  simp only [ωSup_le_iff, forall_const, chain.map_coe, function.comp_app,
+             preorder_hom.has_bot_bot_coe],
 end
 
 end complete_lattice
@@ -564,7 +564,7 @@ protected def ωSup (c : chain (α →ₘ β)) : α →ₘ β :=
 { to_fun := λ a, ωSup (c.map (monotone_apply a)),
   monotone' := λ x y h, ωSup_le_ωSup_of_le (chain.map_le_map _ $ λ a, a.monotone h) }
 
-@[simps ωSup_to_fun]
+@[simps ωSup_coe]
 instance omega_complete_partial_order : omega_complete_partial_order (α →ₘ β) :=
 omega_complete_partial_order.lift preorder_hom.to_fun_hom preorder_hom.ωSup
   (λ x y h, h) (λ c, rfl)
@@ -617,23 +617,23 @@ lemma ωSup_bind {β γ : Type v} (c : chain α) (f : α →ₘ roption β) (g :
   ωSup (c.map (f.bind g)) = ωSup (c.map f) >>= ωSup (c.map g) :=
 begin
   apply eq_of_forall_ge_iff, intro x,
-  simp only [ωSup_le_iff, roption.bind_le, chain.mem_map_iff, and_imp, preorder_hom.bind_to_fun,
+  simp only [ωSup_le_iff, roption.bind_le, chain.mem_map_iff, and_imp, preorder_hom.bind_coe,
     exists_imp_distrib],
   split; intro h''',
   { intros b hb, apply ωSup_le _ _ _,
     rintros i y hy, simp only [roption.mem_ωSup] at hb,
     rcases hb with ⟨j,hb⟩, replace hb := hb.symm,
-    simp only [roption.eq_some_iff, chain.map_to_fun, function.comp_app, pi.monotone_apply_to_fun]
+    simp only [roption.eq_some_iff, chain.map_coe, function.comp_app, pi.monotone_apply_coe]
       at hy hb,
     replace hb : b ∈ f (c (max i j))   := f.monotone (c.monotone (le_max_right i j)) _ hb,
     replace hy : y ∈ g (c (max i j)) b := g.monotone (c.monotone (le_max_left i j)) _ _ hy,
     apply h''' (max i j),
-    simp only [exists_prop, roption.bind_eq_bind, roption.mem_bind_iff, chain.map_to_fun,
-               function.comp_app, preorder_hom.bind_to_fun],
+    simp only [exists_prop, roption.bind_eq_bind, roption.mem_bind_iff, chain.map_coe,
+               function.comp_app, preorder_hom.bind_coe],
     exact ⟨_,hb,hy⟩, },
   { intros i, intros y hy,
-    simp only [exists_prop, roption.bind_eq_bind, roption.mem_bind_iff, chain.map_to_fun,
-               function.comp_app, preorder_hom.bind_to_fun] at hy,
+    simp only [exists_prop, roption.bind_eq_bind, roption.mem_bind_iff, chain.map_coe,
+               function.comp_app, preorder_hom.bind_coe] at hy,
     rcases hy with ⟨b,hb₀,hb₁⟩,
     apply h''' b _,
     { apply le_ωSup (c.map g) _ _ _ hb₁ },
@@ -716,9 +716,9 @@ def const (f : β) : α →𝒄 β :=
 of_mono (preorder_hom.const _ f)
     begin
       intro c, apply le_antisymm,
-      { simp only [function.const, preorder_hom.const_to_fun],
+      { simp only [function.const, preorder_hom.const_coe],
         apply le_ωSup_of_le 0, refl },
-      { apply ωSup_le, simp only [preorder_hom.const_to_fun, chain.map_to_fun, function.comp_app],
+      { apply ωSup_le, simp only [preorder_hom.const_coe, chain.map_coe, function.comp_app],
         intros, refl },
     end
 
@@ -777,8 +777,8 @@ continuous_hom.of_mono (ωSup $ c.map to_mono)
 begin
   intro c',
   apply eq_of_forall_ge_iff, intro z,
-  simp only [ωSup_le_iff, (c _).continuous, chain.map_to_fun, preorder_hom.monotone_apply_to_fun,
-    to_mono_to_fun, coe_apply, preorder_hom.omega_complete_partial_order_ωSup_to_fun,
+  simp only [ωSup_le_iff, (c _).continuous, chain.map_coe, preorder_hom.monotone_apply_coe,
+    to_mono_coe, coe_apply, preorder_hom.omega_complete_partial_order_ωSup_coe,
     forall_forall_merge, forall_forall_merge', function.comp_app],
 end
 
@@ -793,11 +793,11 @@ lemma ωSup_ωSup (c₀ : chain (α →𝒄 β)) (c₁ : chain α) :
   ωSup c₀ (ωSup c₁) = ωSup (continuous_hom.prod.apply.comp $ c₀.zip c₁) :=
 begin
   apply eq_of_forall_ge_iff, intro z,
-  simp only [ωSup_le_iff, (c₀ _).continuous, chain.map_to_fun, to_mono_to_fun, coe_apply,
-    preorder_hom.omega_complete_partial_order_ωSup_to_fun, ωSup_def, forall_forall_merge,
-    chain.zip_to_fun, preorder_hom.prod.map_to_fun, preorder_hom.prod.diag_to_fun, prod.map_mk,
-    preorder_hom.monotone_apply_to_fun, function.comp_app, prod.apply_to_fun,
-    preorder_hom.comp_to_fun, ωSup_to_fun],
+  simp only [ωSup_le_iff, (c₀ _).continuous, chain.map_coe, to_mono_coe, coe_apply,
+    preorder_hom.omega_complete_partial_order_ωSup_coe, ωSup_def, forall_forall_merge,
+    chain.zip_coe, preorder_hom.prod.map_coe, preorder_hom.prod.diag_coe, prod.map_mk,
+    preorder_hom.monotone_apply_coe, function.comp_app, prod.apply_coe,
+    preorder_hom.comp_coe, ωSup_to_fun],
 end
 
 /-- A family of continuous functions yields a continuous family of functions. -/
@@ -820,16 +820,16 @@ end
 @[simps {rhs_md := reducible}]
 noncomputable def map {β γ : Type v} (f : β → γ) (g : α →𝒄 roption β) : α →𝒄 roption γ :=
 of_fun (λ x, f <$> g x) (bind g (const (pure ∘ f))) $
-by ext; simp only [map_eq_bind_pure_comp, bind_to_fun, preorder_hom.bind_to_fun, const_apply,
-  preorder_hom.const_to_fun, coe_apply]
+by ext; simp only [map_eq_bind_pure_comp, bind_to_fun, preorder_hom.bind_coe, const_apply,
+  preorder_hom.const_coe, coe_apply]
 
 /-- `roption.seq` as a continuous function. -/
 @[simps {rhs_md := reducible}]
 noncomputable def seq {β γ : Type v} (f : α →𝒄 roption (β → γ)) (g : α →𝒄 roption β) :
   α →𝒄 roption γ :=
 of_fun (λ x, f x <*> g x) (bind f $ (flip $ _root_.flip map g))
   (by ext; simp only [seq_eq_bind_map, flip, roption.bind_eq_bind, map_to_fun, roption.mem_bind_iff,
-                      bind_to_fun, preorder_hom.bind_to_fun, coe_apply, flip_to_fun]; refl)
+                      bind_to_fun, preorder_hom.bind_coe, coe_apply, flip_to_fun]; refl)
 
 end continuous_hom
 

src/order/preorder_hom.lean

@@ -29,30 +29,28 @@ instance : has_coe_to_fun (preorder_hom α β) :=
 { F := λ f, α → β,
   coe := preorder_hom.to_fun }
 
+initialize_simps_projections preorder_hom (to_fun → coe)
+
 @[mono]
 lemma monotone (f : α →ₘ β) : monotone f :=
 preorder_hom.monotone' f
 
-@[simp]
-lemma coe_fun_mk {f : α → β} (hf : _root_.monotone f) (x : α) : mk f hf x = f x := rfl
-
-@[ext] lemma ext (f g : preorder_hom α β) (h : ∀ a, f a = g a) : f = g :=
-by { cases f, cases g, congr, funext, exact h _ }
+@[simp] lemma to_fun_eq_coe {f : α →ₘ β} : f.to_fun = f := rfl
+@[simp] lemma coe_fun_mk {f : α → β} (hf : _root_.monotone f) : (mk f hf : α → β) = f := rfl
 
-lemma coe_inj (f g : preorder_hom α β) (h : (f : α → β) = g) : f = g :=
-by { ext, rw h }
+@[ext] -- See library note [partially-applied ext lemmas]
+lemma ext (f g : preorder_hom α β) (h : (f : α → β) = g) : f = g :=
+by { cases f, cases g, congr, exact h }
 
 /-- The identity function as bundled monotone function. -/
-@[simps]
+@[simps {fully_applied := ff}]
 def id : preorder_hom α α :=
 ⟨id, monotone_id⟩
 
 instance : inhabited (preorder_hom α α) := ⟨id⟩
 
-@[simp] lemma coe_id : (@id α _ : α → α) = id := rfl
-
 /-- The composition of two bundled monotone functions. -/
-@[simps]
+@[simps {fully_applied := ff}]
 def comp (g : preorder_hom β γ) (f : preorder_hom α β) : preorder_hom α γ :=
 ⟨g ∘ f, g.monotone.comp f.monotone⟩
 
@@ -63,6 +61,7 @@ by { ext, refl }
 by { ext, refl }
 
 /-- `subtype.val` as a bundled monotone function.  -/
+@[simps {fully_applied := ff}]
 def subtype.val (p : α → Prop) : subtype p →ₘ α :=
 ⟨subtype.val, λ x y h, h⟩
 
@@ -89,7 +88,7 @@ instance {β : Type*} [semilattice_inf β] : has_inf (α →ₘ β) :=
 { inf := λ f g, ⟨λ a, f a ⊓ g a, λ x y h, inf_le_inf (f.monotone h) (g.monotone h)⟩ }
 
 instance {β : Type*} [semilattice_inf β] : semilattice_inf (α →ₘ β) :=
-{ inf := has_inf.inf,
+{ inf := (⊓),
   inf_le_left := λ a b x, inf_le_left,
   inf_le_right := λ a b x, inf_le_right,
   le_inf := λ a b c h₀ h₁ x, le_inf (h₀ x) (h₁ x),
@@ -104,7 +103,7 @@ instance {β : Type*} [order_bot β] : has_bot (α →ₘ β) :=
 { bot := ⟨λ a, ⊥, λ a b h, le_refl _⟩ }
 
 instance {β : Type*} [order_bot β] : order_bot (α →ₘ β) :=
-{ bot := has_bot.bot,
+{ bot := ⊥,
   bot_le := λ a x, bot_le,
   .. (_ : partial_order (α →ₘ β)) }
 
@@ -113,7 +112,7 @@ instance {β : Type*} [order_top β] : has_top (α →ₘ β) :=
 { top := ⟨λ a, ⊤, λ a b h, le_refl _⟩ }
 
 instance {β : Type*} [order_top β] : order_top (α →ₘ β) :=
-{ top := has_top.top,
+{ top := ⊤,
   le_top := λ a x, le_top,
   .. (_ : partial_order (α →ₘ β)) }
 
@@ -176,14 +175,11 @@ end preorder_hom
 namespace order_embedding
 
 /-- Convert an `order_embedding` to a `preorder_hom`. -/
+@[simps {fully_applied := ff}]
 def to_preorder_hom {X Y : Type*} [preorder X] [preorder Y] (f : X ↪o Y) : X →ₘ Y :=
 { to_fun := f,
   monotone' := f.monotone }
 
-@[simp]
-lemma to_preorder_hom_coe {X Y : Type*} [preorder X] [preorder Y] (f : X ↪o Y) :
-  (f.to_preorder_hom : X → Y) = (f : X → Y) := rfl
-
 end order_embedding
 section rel_hom
 
@@ -195,12 +191,11 @@ variables (f : ((<) : α → α → Prop) →r ((<) : β → β → Prop))
 
 /-- A bundled expression of the fact that a map between partial orders that is strictly monotonic
 is weakly monotonic. -/
+@[simps {fully_applied := ff}]
 def to_preorder_hom : α →ₘ β :=
 { to_fun    := f,
   monotone' := strict_mono.monotone (λ x y, f.map_rel), }
 
-@[simp] lemma to_preorder_hom_coe_fn : ⇑f.to_preorder_hom = f := rfl
-
 end rel_hom
 
 lemma rel_embedding.to_preorder_hom_injective (f : ((<) : α → α → Prop) ↪r ((<) : β → β → Prop)) :

src/topology/omega_complete_partial_order.lean

@@ -106,7 +106,7 @@ begin
   apply eq_of_forall_ge_iff, intro z,
   rw ωSup_le_iff,
   simp only [ωSup_le_iff, not_below, set.mem_set_of_eq, le_Prop_eq, preorder_hom.coe_fun_mk,
-             chain.map_to_fun, function.comp_app, exists_imp_distrib, not_forall],
+             chain.map_coe, function.comp_app, exists_imp_distrib, not_forall],
 end
 
 end not_below
@@ -141,7 +141,7 @@ begin
   simp only [not_below, preorder_hom.coe_fun_mk, eq_iff_iff, set.mem_set_of_eq] at hf_h,
   rw [← not_iff_not],
   simp only [ωSup_le_iff, hf_h, ωSup, supr, Sup, complete_lattice.Sup, complete_semilattice_Sup.Sup,
-    exists_prop, set.mem_range, preorder_hom.coe_fun_mk, chain.map_to_fun, function.comp_app,
+    exists_prop, set.mem_range, preorder_hom.coe_fun_mk, chain.map_coe, function.comp_app,
     eq_iff_iff, not_forall],
   tauto,
 end