[Merged by Bors] - chore(order/*): Less order_dual abuse

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -496,13 +496,12 @@ noncomputable def sequence_of_cubes : ℕ → { i : ι // valley cs ((cs i).shif
 | 0     := let v := valley_unit_cube h      in ⟨mi h v, valley_mi⟩
 | (k+1) := let v := (sequence_of_cubes k).2 in ⟨mi h v, valley_mi⟩
 
-def decreasing_sequence (k : ℕ) : order_dual ℝ :=
-(cs (sequence_of_cubes h k).1).w
+def decreasing_sequence (k : ℕ) : ℝ := (cs (sequence_of_cubes h k).1).w
 
-lemma strict_mono_sequence_of_cubes : strict_mono $ decreasing_sequence h :=
-strict_mono_nat_of_lt_succ $
+lemma strict_anti_sequence_of_cubes : strict_anti $ decreasing_sequence h :=
+strict_anti_nat_of_succ_lt $ λ k,
 begin
-  intro k, let v := (sequence_of_cubes h k).2, dsimp only [decreasing_sequence, sequence_of_cubes],
+  let v := (sequence_of_cubes h k).2, dsimp only [decreasing_sequence, sequence_of_cubes],
   apply w_lt_w h v (mi_mem_bcubes : mi h v ∈ _),
 end
 
@@ -512,7 +511,7 @@ theorem not_correct : ¬correct cs :=
 begin
   intro h, apply (lt_omega_of_fintype ι).not_le,
   rw [omega, lift_id], fapply mk_le_of_injective, exact λ n, (sequence_of_cubes h n).1,
-  intros n m hnm, apply strict_mono.injective (strict_mono_sequence_of_cubes h),
+  intros n m hnm, apply (strict_anti_sequence_of_cubes h).injective,
   dsimp only [decreasing_sequence], rw hnm
 end
 

src/algebra/order/field.lean

@@ -706,11 +706,11 @@ eq.symm $ monotone.map_max (λ x y, div_le_div_of_le hc)
 
 lemma min_div_div_right_of_nonpos {c : α} (hc : c ≤ 0) (a b : α) :
   min (a / c) (b / c) = (max a b) / c :=
-eq.symm $ @monotone.map_max α αᵒᵈ _ _ _ _ _ (λ x y, div_le_div_of_nonpos_of_le hc)
+eq.symm $ antitone.map_max $ λ x y, div_le_div_of_nonpos_of_le hc
 
 lemma max_div_div_right_of_nonpos {c : α} (hc : c ≤ 0) (a b : α) :
   max (a / c) (b / c) = (min a b) / c :=
-eq.symm $ @monotone.map_min α αᵒᵈ _ _ _ _ _ (λ x y, div_le_div_of_nonpos_of_le hc)
+eq.symm $ antitone.map_min $ λ x y, div_le_div_of_nonpos_of_le hc
 
 lemma abs_div (a b : α) : |a / b| = |a| / |b| := (abs_hom : α →*₀ α).map_div a b
 
@@ -733,10 +733,10 @@ lemma one_div_pow_lt_one_div_pow_of_lt (a1 : 1 < a) {m n : ℕ} (mn : m < n) :
 by refine (one_div_lt_one_div _ _).mpr (pow_lt_pow a1 mn);
   exact pow_pos (trans zero_lt_one a1) _
 
-lemma one_div_pow_mono (a1 : 1 ≤ a) : monotone (λ n : ℕ, order_dual.to_dual 1 / a ^ n) :=
+lemma one_div_pow_anti (a1 : 1 ≤ a) : antitone (λ n : ℕ, 1 / a ^ n) :=
 λ m n, one_div_pow_le_one_div_pow_of_le a1
 
-lemma one_div_pow_strict_mono (a1 : 1 < a) : strict_mono (λ n : ℕ, order_dual.to_dual 1 / a ^ n) :=
+lemma one_div_pow_strict_anti (a1 : 1 < a) : strict_anti (λ n : ℕ, 1 / a ^ n) :=
 λ m n, one_div_pow_lt_one_div_pow_of_lt a1
 
 /-! ### Results about `is_lub` and `is_glb` -/

src/analysis/convex/quasiconvex.lean

@@ -31,7 +31,7 @@ not hard but quite a pain to go about as there are many cases to consider.
 * https://en.wikipedia.org/wiki/Quasiconvex_function
 -/
 
-open function set
+open function order_dual set
 
 variables {𝕜 E F β : Type*}
 
@@ -62,17 +62,9 @@ quasiconvex_on 𝕜 s f ∧ quasiconcave_on 𝕜 s f
 
 variables {𝕜 s f}
 
-lemma quasiconvex_on.dual (hf : quasiconvex_on 𝕜 s f) :
-  @quasiconcave_on 𝕜 E (order_dual β) _ _ _ _ s f :=
-hf
-
-lemma quasiconcave_on.dual (hf : quasiconcave_on 𝕜 s f) :
-  @quasiconvex_on 𝕜 E (order_dual β) _ _ _ _ s f :=
-hf
-
-lemma quasilinear_on.dual (hf : quasilinear_on 𝕜 s f) :
-  @quasilinear_on 𝕜 E (order_dual β) _ _ _ _ s f :=
-⟨hf.2, hf.1⟩
+lemma quasiconvex_on.dual : quasiconvex_on 𝕜 s f → quasiconcave_on 𝕜 s (to_dual ∘ f) := id
+lemma quasiconcave_on.dual : quasiconcave_on 𝕜 s f → quasiconvex_on 𝕜 s (to_dual ∘ f) := id
+lemma quasilinear_on.dual : quasilinear_on 𝕜 s f → quasilinear_on 𝕜 s (to_dual ∘ f) := and.swap
 
 lemma convex.quasiconvex_on_of_convex_le (hs : convex 𝕜 s) (h : ∀ r, convex 𝕜 {x | f x ≤ r}) :
   quasiconvex_on 𝕜 s f :=

src/data/finset/lattice.lean

@@ -607,6 +607,8 @@ lemma inf'_le (h : b ∈ s) : s.inf' ⟨b, h⟩ f ≤ f b := @le_sup' αᵒᵈ _
 
 @[simp] lemma inf'_const (a : α) : s.inf' H (λ b, a) = a := @sup'_const αᵒᵈ _ _ _ _ _
 
+@[simp] lemma le_inf'_iff : a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b := @sup'_le_iff αᵒᵈ _ _ _ H f _
+
 lemma inf'_bUnion [decidable_eq β] {s : finset γ} (Hs : s.nonempty) {t : γ → finset β}
   (Ht : ∀ b, (t b).nonempty) :
   (s.bUnion t).inf' (Hs.bUnion (λ b _, Ht b)) f = s.inf' Hs (λ b, (t b).inf' (Ht b) f) :=

src/number_theory/liouville/liouville_constant.lean

@@ -106,7 +106,7 @@ calc (∑' i, 1 / m ^ (i + (n + 1))!)
       (λ b, one_div_pow_le_one_div_pow_of_le m1.le (b.add_factorial_succ_le_factorial_add_succ n))
       -- 3. the term with index `i = 2` of the first series is strictly smaller than
       -- the corresponding term of the second series
-      (one_div_pow_strict_mono m1 (n.add_factorial_succ_lt_factorial_add_succ rfl.le))
+      (one_div_pow_strict_anti m1 (n.add_factorial_succ_lt_factorial_add_succ rfl.le))
       -- 4. the second series is summable, since its terms grow quickly
       (summable_one_div_pow_of_le m1 (λ j, nat.le.intro rfl))
 ... = ∑' i, (1 / m) ^ i * (1 / m ^ (n + 1)!) :

src/order/compare.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import order.basic
+import order.order_dual
 
 /-!
 # Comparison
@@ -126,22 +126,23 @@ by cases o₁; cases o₂; exact dec_trivial
 
 end ordering
 
-lemma order_dual.dual_compares [has_lt α] {a b : α} {o : ordering} :
-  @ordering.compares αᵒᵈ _ o a b ↔ @ordering.compares α _ o b a :=
+open ordering order_dual
+
+@[simp] lemma to_dual_compares_to_dual [has_lt α] {a b : α} {o : ordering} :
+  compares o (to_dual a) (to_dual b) ↔ compares o b a :=
+by { cases o, exacts [iff.rfl, eq_comm, iff.rfl] }
+
+@[simp] lemma of_dual_compares_of_dual [has_lt α] {a b : αᵒᵈ} {o : ordering} :
+  compares o (of_dual a) (of_dual b) ↔ compares o b a :=
 by { cases o, exacts [iff.rfl, eq_comm, iff.rfl] }
 
 lemma cmp_compares [linear_order α] (a b : α) : (cmp a b).compares a b :=
-begin
-  unfold cmp cmp_using,
-  by_cases a < b; simp [h],
-  by_cases h₂ : b < a; simp [h₂, gt],
-  exact (decidable.lt_or_eq_of_le (le_of_not_gt h₂)).resolve_left h
-end
+by obtain h | h | h := lt_trichotomy a b; simp [cmp, cmp_using, h, h.not_lt]
 
 lemma cmp_swap [preorder α] [@decidable_rel α (<)] (a b : α) : (cmp a b).swap = cmp b a :=
 begin
   unfold cmp cmp_using,
-  by_cases a < b; by_cases h₂ : b < a; simp [h, h₂, gt, ordering.swap],
+  by_cases a < b; by_cases h₂ : b < a; simp [h, h₂, ordering.swap],
   exact lt_asymm h h₂
 end
 

src/order/galois_connection.lean

@@ -41,7 +41,8 @@ This means the infimum of subgroups will be defined to be the intersection of se
 with a proof that intersection of subgroups is a subgroup, rather than the closure of the
 intersection.
 -/
-open function order set
+
+open function order_dual set
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {κ : ι → Sort*} {a a₁ a₂ : α}
@@ -543,22 +544,22 @@ structure galois_coinsertion {α β : Type*} [preorder α] [preorder β] (l : α
 
 /-- Make a `galois_insertion u l` in the `order_dual`, from a `galois_coinsertion l u` -/
 def galois_coinsertion.dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
-  galois_coinsertion l u → @galois_insertion (order_dual β) (order_dual α) _ _ u l :=
+  galois_coinsertion l u → galois_insertion (to_dual ∘ u ∘ of_dual) (to_dual ∘ l ∘ of_dual) :=
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Make a `galois_coinsertion u l` in the `order_dual`, from a `galois_insertion l u` -/
 def galois_insertion.dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
-  galois_insertion l u → @galois_coinsertion (order_dual β) (order_dual α) _ _ u l :=
+  galois_insertion l u → galois_coinsertion (to_dual ∘ u ∘ of_dual) (to_dual ∘ l ∘ of_dual) :=
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Make a `galois_coinsertion l u` from a `galois_insertion l u` in the `order_dual` -/
 def galois_coinsertion.of_dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
-  @galois_insertion (order_dual β) (order_dual α) _ _ u l → galois_coinsertion l u :=
+  galois_insertion (to_dual ∘ u ∘ of_dual) (to_dual ∘ l ∘ of_dual) → galois_coinsertion l u :=
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Make a `galois_insertion l u` from a `galois_coinsertion l u` in the `order_dual` -/
 def galois_insertion.of_dual {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α} :
-  @galois_coinsertion (order_dual β) (order_dual α) _ _ u l → galois_insertion l u :=
+  galois_coinsertion (to_dual ∘ u ∘ of_dual) (to_dual ∘ l ∘ of_dual) → galois_insertion l u :=
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Makes a Galois coinsertion from an order-preserving bijection. -/

src/order/monotone.lean

@@ -557,7 +557,7 @@ protected theorem strict_mono_on.compares (hf : strict_mono_on f s) {a b : α} (
 protected theorem strict_anti_on.compares (hf : strict_anti_on f s) {a b : α} (ha : a ∈ s)
   (hb : b ∈ s) {o : ordering} :
   o.compares (f a) (f b) ↔ o.compares b a :=
-order_dual.dual_compares.trans $ hf.dual_right.compares hb ha
+to_dual_compares_to_dual.trans $ hf.dual_right.compares hb ha
 
 protected theorem strict_mono.compares (hf : strict_mono f) {a b : α} {o : ordering} :
   o.compares (f a) (f b) ↔ o.compares a b :=

src/order/ord_continuous.lean

@@ -23,7 +23,7 @@ universes u v w x
 
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
 
-open set function
+open function order_dual set
 
 /-!
 ### Definitions
@@ -51,8 +51,8 @@ protected lemma id : left_ord_continuous (id : α → α) := λ s x h, by simpa
 
 variable {α}
 
-protected lemma order_dual (hf : left_ord_continuous f) :
-  @right_ord_continuous (order_dual α) (order_dual β) _ _ f := hf
+protected lemma order_dual : left_ord_continuous f → right_ord_continuous (to_dual ∘ f ∘ of_dual) :=
+id
 
 lemma map_is_greatest (hf : left_ord_continuous f) {s : set α} {x : α} (h : is_greatest s x):
   is_greatest (f '' s) (f x) :=
@@ -148,8 +148,8 @@ protected lemma id : right_ord_continuous (id : α → α) := λ s x h, by simpa
 
 variable {α}
 
-protected lemma order_dual (hf : right_ord_continuous f) :
-  @left_ord_continuous (order_dual α) (order_dual β) _ _ f := hf
+protected lemma order_dual : right_ord_continuous f → left_ord_continuous (to_dual ∘ f ∘ of_dual) :=
+id
 
 lemma map_is_least (hf : right_ord_continuous f) {s : set α} {x : α} (h : is_least s x):
   is_least (f '' s) (f x) :=