feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_i…

…ff (#6157)

Add if and only if versions of `Monotone.dual` and `Antitone.dual`.

Needed for #5672



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>

Mathlib/Order/Monotone/Basic.lean

@@ -238,43 +238,31 @@ theorem strictAntiOn_toDual_comp_iff : StrictAntiOn (toDual ∘ f : α → βᵒ
   Iff.rfl
 #align strict_anti_on_to_dual_comp_iff strictAntiOn_toDual_comp_iff
 
-protected theorem Monotone.dual (hf : Monotone f) : Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) :=
-  swap hf
-#align monotone.dual Monotone.dual
+theorem monotone_dual_iff : Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Monotone f := by
+  rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]
 
-protected theorem Antitone.dual (hf : Antitone f) : Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) :=
-  swap hf
-#align antitone.dual Antitone.dual
+theorem antitone_dual_iff : Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Antitone f := by
+  rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]
 
-protected theorem MonotoneOn.dual (hf : MonotoneOn f s) :
-    MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s :=
-  swap₂ hf
-#align monotone_on.dual MonotoneOn.dual
+theorem monotone_on_dual_iff : MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s := by
+  rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]
 
-protected theorem AntitoneOn.dual (hf : AntitoneOn f s) :
-    AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s :=
-  swap₂ hf
-#align antitone_on.dual AntitoneOn.dual
+theorem antitone_on_dual_iff : AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s := by
+  rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]
 
-protected theorem StrictMono.dual (hf : StrictMono f) :
-    StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) :=
-  swap hf
-#align strict_mono.dual StrictMono.dual
+theorem strict_mono_dual_iff : StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f := by
+  rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]
 
-protected theorem StrictAnti.dual (hf : StrictAnti f) :
-    StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) :=
-  swap hf
-#align strict_anti.dual StrictAnti.dual
+theorem strict_anti_dual_iff : StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f := by
+  rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]
 
-protected theorem StrictMonoOn.dual (hf : StrictMonoOn f s) :
-    StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s :=
-  swap₂ hf
-#align strict_mono_on.dual StrictMonoOn.dual
+theorem strict_mono_on_dual_iff :
+    StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictMonoOn f s := by
+  rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]
 
-protected theorem StrictAntiOn.dual (hf : StrictAntiOn f s) :
-    StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s :=
-  swap₂ hf
-#align strict_anti_on.dual StrictAntiOn.dual
+theorem strict_anti_on_dual_iff :
+    StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictAntiOn f s := by
+  rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]
 
 alias antitone_comp_ofDual_iff ↔ _ Monotone.dual_left
 #align monotone.dual_left Monotone.dual_left
@@ -324,6 +312,30 @@ alias strictAntiOn_toDual_comp_iff ↔ _ StrictMonoOn.dual_right
 alias strictMonoOn_toDual_comp_iff ↔ _ StrictAntiOn.dual_right
 #align strict_anti_on.dual_right StrictAntiOn.dual_right
 
+alias monotone_dual_iff ↔ _ Monotone.dual
+#align monotone.dual Monotone.dual
+
+alias antitone_dual_iff ↔ _ Antitone.dual
+#align antitone.dual Antitone.dual
+
+alias monotone_on_dual_iff ↔ _ MonotoneOn.dual
+#align monotone_on.dual MonotoneOn.dual
+
+alias antitone_on_dual_iff ↔ _ AntitoneOn.dual
+#align antitone_on.dual AntitoneOn.dual
+
+alias strict_mono_dual_iff ↔ _ StrictMono.dual
+#align strict_mono.dual StrictMono.dual
+
+alias strict_anti_dual_iff ↔ _ StrictAnti.dual
+#align strict_anti.dual StrictAnti.dual
+
+alias strict_mono_on_dual_iff ↔ _ StrictMonoOn.dual
+#align strict_mono_on.dual StrictMonoOn.dual
+
+alias strict_anti_on_dual_iff ↔ _ StrictAntiOn.dual
+#align strict_anti_on.dual StrictAntiOn.dual
+
 end OrderDual
 
 /-! ### Monotonicity in function spaces -/