chore(order/*): use to_dual and of_dual in statements instead of implicit coercions between and α and order_dual α (#9593)

Previously the meaning of the statement was hidden away in an invisible surprising typeclass argument.

Before this change, the docs suggested the nonsensical statement that `monotone f` implies `antitone f`!

![image](https://user-images.githubusercontent.com/425260/136348562-d3ecbb85-2a54-4c13-adda-806eb150b00a.png)

Most of the proof changes in this PR are a consequence of changing the interval lemmas, not the monotonicity or convexity ones.

Author: eric-wieser

src/analysis/convex/function.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, François Dupuis
 -/
 import analysis.convex.basic
+import order.order_dual
 import tactic.field_simp
 import tactic.linarith
 import tactic.ring
@@ -70,16 +71,16 @@ convex 𝕜 s ∧
 
 variables {𝕜 s f}
 
-lemma convex_on.dual (hf : convex_on 𝕜 s f) : @concave_on 𝕜 E (order_dual β) _ _ _ _ _ s f := hf
+open order_dual (to_dual of_dual)
 
-lemma concave_on.dual (hf : concave_on 𝕜 s f) : @convex_on 𝕜 E (order_dual β) _ _ _ _ _ s f := hf
+lemma convex_on.dual (hf : convex_on 𝕜 s f) : concave_on 𝕜 s (to_dual ∘ f) := hf
 
-lemma strict_convex_on.dual (hf : strict_convex_on 𝕜 s f) :
-  @strict_concave_on 𝕜 E (order_dual β) _ _ _ _ _ s f :=
+lemma concave_on.dual (hf : concave_on 𝕜 s f) : convex_on 𝕜 s (to_dual ∘ f) := hf
+
+lemma strict_convex_on.dual (hf : strict_convex_on 𝕜 s f) : strict_concave_on 𝕜 s (to_dual ∘ f) :=
 hf
 
-lemma strict_concave_on.dual (hf : strict_concave_on 𝕜 s f) :
-  @strict_convex_on 𝕜 E (order_dual β) _ _ _ _ _ s f :=
+lemma strict_concave_on.dual (hf : strict_concave_on 𝕜 s f) : strict_convex_on 𝕜 s (to_dual ∘ f) :=
 hf
 
 lemma convex_on_id {s : set β} (hs : convex 𝕜 s) : convex_on 𝕜 s id := ⟨hs, by { intros, refl }⟩

src/data/set/intervals/basic.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy
 import algebra.order.group
 import data.set.basic
 import order.rel_iso
+import order.order_dual
 
 /-!
 # Intervals
@@ -31,6 +32,7 @@ universe u
 namespace set
 
 open set
+open order_dual (to_dual of_dual)
 
 section intervals
 variables {α : Type u} [preorder α] {a a₁ a₂ b b₁ b₂ x : α}
@@ -95,17 +97,17 @@ lemma left_mem_Ici : a ∈ Ici a := by simp
 @[simp] lemma right_mem_Ioc : b ∈ Ioc a b ↔ a < b := by simp [le_refl]
 lemma right_mem_Iic : a ∈ Iic a := by simp
 
-@[simp] lemma dual_Ici : @Ici (order_dual α) _ a = @Iic α _ a := rfl
-@[simp] lemma dual_Iic : @Iic (order_dual α) _ a = @Ici α _ a := rfl
-@[simp] lemma dual_Ioi : @Ioi (order_dual α) _ a = @Iio α _ a := rfl
-@[simp] lemma dual_Iio : @Iio (order_dual α) _ a = @Ioi α _ a := rfl
-@[simp] lemma dual_Icc : @Icc (order_dual α) _ a b = @Icc α _ b a :=
+@[simp] lemma dual_Ici : Ici (to_dual a) = of_dual ⁻¹' Iic a := rfl
+@[simp] lemma dual_Iic : Iic (to_dual a) = of_dual ⁻¹' Ici a := rfl
+@[simp] lemma dual_Ioi : Ioi (to_dual a) = of_dual ⁻¹' Iio a := rfl
+@[simp] lemma dual_Iio : Iio (to_dual a) = of_dual ⁻¹' Ioi a := rfl
+@[simp] lemma dual_Icc : Icc (to_dual a) (to_dual b) = of_dual ⁻¹' Icc b a :=
 set.ext $ λ x, and_comm _ _
-@[simp] lemma dual_Ioc : @Ioc (order_dual α) _ a b = @Ico α _ b a :=
+@[simp] lemma dual_Ioc : Ioc (to_dual a) (to_dual b) = of_dual ⁻¹' Ico b a :=
 set.ext $ λ x, and_comm _ _
-@[simp] lemma dual_Ico : @Ico (order_dual α) _ a b = @Ioc α _ b a :=
+@[simp] lemma dual_Ico : Ico (to_dual a) (to_dual b) = of_dual ⁻¹' Ioc b a :=
 set.ext $ λ x, and_comm _ _
-@[simp] lemma dual_Ioo : @Ioo (order_dual α) _ a b = @Ioo α _ b a :=
+@[simp] lemma dual_Ioo : Ioo (to_dual a) (to_dual b) = of_dual ⁻¹' Ioo b a :=
 set.ext $ λ x, and_comm _ _
 
 @[simp] lemma nonempty_Icc : (Icc a b).nonempty ↔ a ≤ b :=
@@ -430,14 +432,14 @@ by rw [← Ico_diff_left, diff_union_self,
   union_eq_self_of_subset_right (singleton_subset_iff.2 $ left_mem_Ico.2 hab)]
 
 lemma Ioo_union_right (hab : a < b) : Ioo a b ∪ {b} = Ioc a b :=
-by simpa only [dual_Ioo, dual_Ico] using @Ioo_union_left (order_dual α) _ b a hab
+by simpa only [dual_Ioo, dual_Ico] using Ioo_union_left hab.dual
 
 lemma Ioc_union_left (hab : a ≤ b) : Ioc a b ∪ {a} = Icc a b :=
 by rw [← Icc_diff_left, diff_union_self,
   union_eq_self_of_subset_right (singleton_subset_iff.2 $ left_mem_Icc.2 hab)]
 
 lemma Ico_union_right (hab : a ≤ b) : Ico a b ∪ {b} = Icc a b :=
-by simpa only [dual_Ioc, dual_Icc] using @Ioc_union_left (order_dual α) _ b a hab
+by simpa only [dual_Ioc, dual_Icc] using Ioc_union_left hab.dual
 
 lemma mem_Ici_Ioi_of_subset_of_subset {s : set α} (ho : Ioi a ⊆ s) (hc : s ⊆ Ici a) :
   s ∈ ({Ici a, Ioi a} : set (set α)) :=
@@ -492,7 +494,7 @@ end
 lemma mem_Ioo_or_eq_right_of_mem_Ioc {x : α} (hmem : x ∈ Ioc a b) :
   x = b ∨ x ∈ Ioo a b :=
 begin
-  have := @mem_Ioo_or_eq_left_of_mem_Ico (order_dual α) _ b a x,
+  have := @mem_Ioo_or_eq_left_of_mem_Ico _ _ (to_dual b) (to_dual a) (to_dual x),
   rw [dual_Ioo, dual_Ico] at this,
   exact this hmem
 end

src/data/set/intervals/disjoint.lean

@@ -17,6 +17,7 @@ universe u
 
 variables {α : Type u}
 
+open order_dual (to_dual)
 
 namespace set
 
@@ -45,7 +46,8 @@ by simp_rw [set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff,
   inf_eq_min, sup_eq_max, not_lt]
 
 @[simp] lemma Ioc_disjoint_Ioc : disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ :=
-by simpa only [dual_Ico] using @Ico_disjoint_Ico (order_dual α) _ a₂ a₁ b₂ b₁
+have h : _ ↔ min (to_dual a₁) (to_dual b₁) ≤ max (to_dual a₂) (to_dual b₂) := Ico_disjoint_Ico,
+by simpa only [dual_Ico] using h
 
 /-- If two half-open intervals are disjoint and the endpoint of one lies in the other,
   then it must be equal to the endpoint of the other. -/

src/data/set/intervals/ord_connected.lean

@@ -65,10 +65,11 @@ instance ord_connected.inter' {s t : set α} [ord_connected s] [ord_connected t]
   ord_connected (s ∩ t) :=
 ord_connected.inter ‹_› ‹_›
 
-lemma ord_connected.dual {s : set α} (hs : ord_connected s) : @ord_connected (order_dual α) _ s :=
+lemma ord_connected.dual {s : set α} (hs : ord_connected s) :
+  ord_connected (order_dual.of_dual ⁻¹' s) :=
 ⟨λ x hx y hy z hz, hs.out hy hx ⟨hz.2, hz.1⟩⟩
 
-lemma ord_connected_dual {s : set α} : @ord_connected (order_dual α) _ s ↔ ord_connected s :=
+lemma ord_connected_dual {s : set α} : ord_connected (order_dual.of_dual ⁻¹' s) ↔ ord_connected s :=
 ⟨λ h, by simpa only [ord_connected_def] using h.dual, λ h, h.dual⟩
 
 lemma ord_connected_sInter {S : set (set α)} (hS : ∀ s ∈ S, ord_connected s) :

src/data/set/intervals/surj_on.lean

@@ -16,7 +16,7 @@ permutations of interval endpoints.
 
 variables {α : Type*} {β : Type*} [linear_order α] [partial_order β] {f : α → β}
 
-open set function
+open set function order_dual (to_dual)
 
 lemma surj_on_Ioo_of_monotone_surjective
   (h_mono : monotone f) (h_surj : function.surjective f) (a b : α) :
@@ -51,10 +51,7 @@ end
 lemma surj_on_Ioc_of_monotone_surjective
   (h_mono : monotone f) (h_surj : function.surjective f) (a b : α) :
   surj_on f (Ioc a b) (Ioc (f a) (f b)) :=
-begin
-  convert @surj_on_Ico_of_monotone_surjective _ _ _ _ _ h_mono.dual h_surj b a;
-  simp
-end
+by simpa using surj_on_Ico_of_monotone_surjective h_mono.dual h_surj (to_dual b) (to_dual a)
 
 -- to see that the hypothesis `a ≤ b` is necessary, consider a constant function
 lemma surj_on_Icc_of_monotone_surjective

src/order/bounded_lattice.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 import data.option.basic
 import logic.nontrivial
 import order.lattice
+import order.order_dual
 import tactic.pi_instances
 
 /-!
@@ -1162,7 +1163,9 @@ lemma inf_eq_bot (h : is_compl x y) : x ⊓ y = ⊥ := h.disjoint.eq_bot
 
 lemma sup_eq_top (h : is_compl x y) : x ⊔ y = ⊤ := top_unique h.top_le_sup
 
-lemma to_order_dual (h : is_compl x y) : @is_compl (order_dual α) _ x y := ⟨h.2, h.1⟩
+open order_dual (to_dual)
+
+lemma to_order_dual (h : is_compl x y) : is_compl (to_dual x) (to_dual y) := ⟨h.2, h.1⟩
 
 end bounded_lattice
 

src/order/bounds.lean

@@ -22,7 +22,7 @@ In this file we define:
 We also prove various lemmas about monotonicity, behaviour under `∪`, `∩`, `insert`, and provide
 formulas for `∅`, `univ`, and intervals.
 -/
-open set
+open set order_dual (to_dual of_dual)
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
@@ -461,13 +461,13 @@ section
 variables [semilattice_inf γ] [densely_ordered γ]
 
 lemma is_lub_Ioo {a b : γ} (hab : a < b) : is_lub (Ioo a b) b :=
-by simpa only [dual_Ioo] using @is_glb_Ioo (order_dual γ) _ _ b a hab
+by simpa only [dual_Ioo] using is_glb_Ioo hab.dual
 
 lemma upper_bounds_Ioo {a b : γ} (hab : a < b) : upper_bounds (Ioo a b) = Ici b :=
 (is_lub_Ioo hab).upper_bounds_eq
 
 lemma is_lub_Ico {a b : γ} (hab : a < b) : is_lub (Ico a b) b :=
-by simpa only [dual_Ioc] using @is_glb_Ioc (order_dual γ) _ _ b a hab
+by simpa only [dual_Ioc] using is_glb_Ioc hab.dual
 
 lemma upper_bounds_Ico {a b : γ} (hab : a < b) : upper_bounds (Ico a b) = Ici b :=
 (is_lub_Ico hab).upper_bounds_eq

src/order/filter/extr.lean

@@ -156,22 +156,24 @@ lemma is_extr_on_const {b : β} : is_extr_on (λ _, b) s a := is_extr_filter_con
 
 /-! ### Order dual -/
 
-lemma is_min_filter_dual_iff : @is_min_filter α (order_dual β) _ f l a ↔ is_max_filter f l a :=
+open order_dual (to_dual)
+
+lemma is_min_filter_dual_iff : is_min_filter (to_dual ∘ f) l a ↔ is_max_filter f l a :=
 iff.rfl
 
-lemma is_max_filter_dual_iff : @is_max_filter α (order_dual β) _ f l a ↔ is_min_filter f l a :=
+lemma is_max_filter_dual_iff : is_max_filter (to_dual ∘ f) l a ↔ is_min_filter f l a :=
 iff.rfl
 
-lemma is_extr_filter_dual_iff : @is_extr_filter α (order_dual β) _ f l a ↔ is_extr_filter f l a :=
+lemma is_extr_filter_dual_iff : is_extr_filter (to_dual ∘ f) l a ↔ is_extr_filter f l a :=
 or_comm _ _
 
 alias is_min_filter_dual_iff ↔ is_min_filter.undual is_max_filter.dual
 alias is_max_filter_dual_iff ↔ is_max_filter.undual is_min_filter.dual
 alias is_extr_filter_dual_iff ↔ is_extr_filter.undual is_extr_filter.dual
 
-lemma is_min_on_dual_iff : @is_min_on α (order_dual β) _ f s a ↔ is_max_on f s a := iff.rfl
-lemma is_max_on_dual_iff : @is_max_on α (order_dual β) _ f s a ↔ is_min_on f s a := iff.rfl
-lemma is_extr_on_dual_iff : @is_extr_on α (order_dual β) _ f s a ↔ is_extr_on f s a := or_comm _ _
+lemma is_min_on_dual_iff : is_min_on (to_dual ∘ f) s a ↔ is_max_on f s a := iff.rfl
+lemma is_max_on_dual_iff : is_max_on (to_dual ∘ f) s a ↔ is_min_on f s a := iff.rfl
+lemma is_extr_on_dual_iff : is_extr_on (to_dual ∘ f) s a ↔ is_extr_on f s a := or_comm _ _
 
 alias is_min_on_dual_iff ↔ is_min_on.undual is_max_on.dual
 alias is_max_on_dual_iff ↔ is_max_on.undual is_min_on.dual

src/order/monotone.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro, Yaël Dillies
 -/
 import order.compare
+import order.order_dual
 
 /-!
 # Monotonicity
@@ -97,106 +98,93 @@ def strict_anti_on (f : α → β) (s : set α) : Prop :=
 
 end monotone_def
 
-/-! #### Monotonicity on the dual order -/
+/-! #### Monotonicity on the dual order
+
+Strictly many of the `*_on.dual` lemmas in this section should use `of_dual ⁻¹' s` instead of `s`,
+but right now this is not possible as `set.preimage` is not defined yet, and importing it creates
+an import cycle.
+-/
 
 section order_dual
 open order_dual
 variables [preorder α] [preorder β] {f : α → β} {s : set α}
 
-protected theorem monotone.dual (hf : monotone f) :
-  @monotone (order_dual α) (order_dual β) _ _ f :=
+protected theorem monotone.dual (hf : monotone f) : monotone (to_dual ∘ f ∘ of_dual) :=
 λ a b h, hf h
 
-protected lemma monotone.dual_left  (hf : monotone f) :
-  @antitone (order_dual α) β _ _ f :=
+protected lemma monotone.dual_left (hf : monotone f) : antitone (f ∘ of_dual) :=
 λ a b h, hf h
 
-protected lemma monotone.dual_right  (hf : monotone f) :
-  @antitone α (order_dual β) _ _ f :=
+protected lemma monotone.dual_right (hf : monotone f) : antitone (to_dual ∘ f) :=
 λ a b h, hf h
 
-protected theorem antitone.dual  (hf : antitone f) :
-  @antitone (order_dual α) (order_dual β) _ _ f :=
+protected theorem antitone.dual (hf : antitone f) : antitone (to_dual ∘ f ∘ of_dual) :=
 λ a b h, hf h
 
-protected lemma antitone.dual_left  (hf : antitone f) :
-  @monotone (order_dual α) β _ _ f :=
+protected lemma antitone.dual_left (hf : antitone f) : monotone (f ∘ of_dual) :=
 λ a b h, hf h
 
-protected lemma antitone.dual_right  (hf : antitone f) :
-  @monotone α (order_dual β) _ _ f :=
+protected lemma antitone.dual_right (hf : antitone f) : monotone (to_dual ∘ f) :=
 λ a b h, hf h
 
-protected theorem monotone_on.dual (hf : monotone_on f s) :
-  @monotone_on (order_dual α) (order_dual β) _ _ f s :=
+protected theorem monotone_on.dual (hf : monotone_on f s) : monotone_on (to_dual ∘ f ∘ of_dual) s :=
 λ a ha b hb, hf hb ha
 
-protected lemma monotone_on.dual_left (hf : monotone_on f s) :
-  @antitone_on (order_dual α) β _ _ f s :=
+protected lemma monotone_on.dual_left (hf : monotone_on f s) : antitone_on (f ∘ of_dual) s :=
 λ a ha b hb, hf hb ha
 
-protected lemma monotone_on.dual_right (hf : monotone_on f s) :
-  @antitone_on α (order_dual β) _ _ f s :=
+protected lemma monotone_on.dual_right (hf : monotone_on f s) : antitone_on (to_dual ∘ f) s :=
 λ a ha b hb, hf ha hb
 
-protected theorem antitone_on.dual (hf : antitone_on f s) :
-  @antitone_on (order_dual α) (order_dual β) _ _ f s :=
+protected theorem antitone_on.dual (hf : antitone_on f s) : antitone_on (to_dual ∘ f ∘ of_dual) s :=
 λ a ha b hb, hf hb ha
 
-protected lemma antitone_on.dual_left (hf : antitone_on f s) :
-  @monotone_on (order_dual α) β _ _ f s :=
+protected lemma antitone_on.dual_left (hf : antitone_on f s) : monotone_on (f ∘ of_dual) s :=
 λ a ha b hb, hf hb ha
 
-protected lemma antitone_on.dual_right (hf : antitone_on f s) :
-  @monotone_on α (order_dual β) _ _ f s :=
+protected lemma antitone_on.dual_right (hf : antitone_on f s) : monotone_on (to_dual ∘ f) s :=
 λ a ha b hb, hf ha hb
 
-protected theorem strict_mono.dual (hf : strict_mono f) :
-  @strict_mono (order_dual α) (order_dual β) _ _ f :=
+protected theorem strict_mono.dual (hf : strict_mono f) : strict_mono (to_dual ∘ f ∘ of_dual) :=
 λ a b h, hf h
 
-protected lemma strict_mono.dual_left  (hf : strict_mono f) :
-  @strict_anti (order_dual α) β _ _ f :=
+protected lemma strict_mono.dual_left (hf : strict_mono f) : strict_anti (f ∘ of_dual) :=
 λ a b h, hf h
 
-protected lemma strict_mono.dual_right  (hf : strict_mono f) :
-  @strict_anti α (order_dual β) _ _ f :=
+protected lemma strict_mono.dual_right (hf : strict_mono f) : strict_anti (to_dual ∘ f) :=
 λ a b h, hf h
 
-protected theorem strict_anti.dual  (hf : strict_anti f) :
-  @strict_anti (order_dual α) (order_dual β) _ _ f :=
+protected theorem strict_anti.dual (hf : strict_anti f) : strict_anti (to_dual ∘ f ∘ of_dual) :=
 λ a b h, hf h
 
-protected lemma strict_anti.dual_left  (hf : strict_anti f) :
-  @strict_mono (order_dual α) β _ _ f :=
+protected lemma strict_anti.dual_left (hf : strict_anti f) : strict_mono (f ∘ of_dual) :=
 λ a b h, hf h
 
-protected lemma strict_anti.dual_right  (hf : strict_anti f) :
-  @strict_mono α (order_dual β) _ _ f :=
+protected lemma strict_anti.dual_right (hf : strict_anti f) : strict_mono (to_dual ∘ f) :=
 λ a b h, hf h
 
 protected theorem strict_mono_on.dual (hf : strict_mono_on f s) :
-  @strict_mono_on (order_dual α) (order_dual β) _ _ f s :=
+  strict_mono_on (to_dual ∘ f ∘ of_dual) s :=
 λ a ha b hb, hf hb ha
 
 protected lemma strict_mono_on.dual_left (hf : strict_mono_on f s) :
-  @strict_anti_on (order_dual α) β _ _ f s :=
+  strict_anti_on (f ∘ of_dual) s :=
 λ a ha b hb, hf hb ha
 
 protected lemma strict_mono_on.dual_right (hf : strict_mono_on f s) :
-  @strict_anti_on α (order_dual β) _ _ f s :=
+  strict_anti_on (to_dual ∘ f) s :=
 λ a ha b hb, hf ha hb
 
 protected theorem strict_anti_on.dual (hf : strict_anti_on f s) :
-  @strict_anti_on (order_dual α) (order_dual β) _ _ f s :=
+  strict_anti_on (to_dual ∘ f ∘ of_dual) s :=
 λ a ha b hb, hf hb ha
 
 protected lemma strict_anti_on.dual_left (hf : strict_anti_on f s) :
-  @strict_mono_on (order_dual α) β _ _ f s :=
+  strict_mono_on (f ∘ of_dual) s :=
 λ a ha b hb, hf hb ha
 
 protected lemma strict_anti_on.dual_right (hf : strict_anti_on f s) :
-  @strict_mono_on α (order_dual β) _ _ f s :=
+  strict_mono_on (to_dual ∘ f) s :=
 λ a ha b hb, hf ha hb
 
 end order_dual
@@ -347,7 +335,7 @@ protected lemma strict_anti.ite' (hf : strict_anti f) (hg : strict_anti g) {p :
   [decidable_pred p] (hp : ∀ ⦃x y⦄, x < y → p y → p x)
   (hfg : ∀ ⦃x y⦄, p x → ¬p y → x < y → g y < f x) :
   strict_anti (λ x, if p x then f x else g x) :=
-@strict_mono.ite' α (order_dual β) _ _ f g hf hg p _ hp hfg
+(strict_mono.ite' hf.dual_right hg.dual_right hp hfg).dual_right
 
 protected lemma strict_anti.ite (hf : strict_anti f) (hg : strict_anti g) {p : α → Prop}
   [decidable_pred p] (hp : ∀ ⦃x y⦄, x < y → p y → p x) (hfg : ∀ x, g x ≤ f x) :

src/order/order_dual.lean

@@ -75,4 +75,13 @@ lemma to_dual_lt [has_lt α] {a : α} {b : order_dual α} :
 protected def rec {C : order_dual α → Sort*} (h₂ : Π (a : α), C (to_dual a)) :
   Π (a : order_dual α), C a := h₂
 
+@[simp] protected lemma «forall» {p : order_dual α → Prop} : (∀ a, p a) ↔ ∀ a, p (to_dual a) :=
+iff.rfl
+
+@[simp] protected lemma «exists» {p : order_dual α → Prop} : (∃ a, p a) ↔ ∃ a, p (to_dual a) :=
+iff.rfl
+
 end order_dual
+
+alias order_dual.to_dual_lt_to_dual ↔ _ has_lt.lt.dual
+alias order_dual.to_dual_le_to_dual ↔ _ has_le.le.dual