feat(topology/algebra/const_mul_action): order_dual instances (#17125)

A few missing instances for `order_dual`. Namely:
* `has_vadd αᵒᵈ β`, `has_smul αᵒᵈ β`, `has_pow αᵒᵈ β` and the corresponding `lex` ones
* `has_continuous_const_vadd α βᵒᵈ`, `has_continuous_const_smul α βᵒᵈ`
* `has_continuous_const_vadd αᵒᵈ β`, `has_continuous_const_smul αᵒᵈ β`

Also fix accidents in `algebra.group.order_synonym`.

src/algebra/group/order_synonym.lean

@@ -24,8 +24,11 @@ variables {α β : Type*}
 @[to_additive] instance [h : has_inv α] : has_inv αᵒᵈ := h
 @[to_additive] instance [h : has_div α] : has_div αᵒᵈ := h
 @[to_additive] instance [h : has_smul α β] : has_smul α βᵒᵈ := h
+@[to_additive] instance order_dual.has_smul' [h : has_smul α β] : has_smul αᵒᵈ β := h
 @[to_additive order_dual.has_smul]
 instance order_dual.has_pow [h : has_pow α β] : has_pow αᵒᵈ β := h
+@[to_additive order_dual.has_smul']
+instance order_dual.has_pow' [h : has_pow α β] : has_pow α βᵒᵈ := h
 @[to_additive] instance [h : semigroup α] : semigroup αᵒᵈ := h
 @[to_additive] instance [h : comm_semigroup α] : comm_semigroup αᵒᵈ := h
 @[to_additive] instance [h : left_cancel_semigroup α] : left_cancel_semigroup αᵒᵈ := h
@@ -58,16 +61,22 @@ lemma of_dual_mul [has_mul α] (a b : αᵒᵈ) : of_dual (a * b) = of_dual a *
 lemma to_dual_div [has_div α] (a b : α) : to_dual (a / b) = to_dual a / to_dual b := rfl
 @[simp, to_additive]
 lemma of_dual_div [has_div α] (a b : αᵒᵈ) : of_dual (a / b) = of_dual a / of_dual b := rfl
-lemma to_dual_vadd [has_vadd α β] (a : α) (b : β) : to_dual (a +ᵥ b) = a +ᵥ to_dual b := rfl
-lemma of_dual_vadd [has_vadd α β] (a : α) (b : βᵒᵈ) : of_dual (a +ᵥ b) = a +ᵥ of_dual b := rfl
 @[simp, to_additive]
 lemma to_dual_smul [has_smul α β] (a : α) (b : β) : to_dual (a • b) = a • to_dual b := rfl
 @[simp, to_additive]
 lemma of_dual_smul [has_smul α β] (a : α) (b : βᵒᵈ) : of_dual (a • b) = a • of_dual b := rfl
-@[simp, to_additive to_dual_smul]
+@[simp, to_additive]
+lemma to_dual_smul' [has_smul α β] (a : α) (b : β) : to_dual a • b = a • b := rfl
+@[simp, to_additive]
+lemma of_dual_smul' [has_smul α β] (a : αᵒᵈ) (b : β) : of_dual a • b = a • b := rfl
+@[simp, to_additive to_dual_smul, to_additive_reorder 1 4]
 lemma to_dual_pow [has_pow α β] (a : α) (b : β) : to_dual (a ^ b) = to_dual a ^ b := rfl
-@[simp, to_additive of_dual_smul]
+@[simp, to_additive of_dual_smul, to_additive_reorder 1 4]
 lemma of_dual_pow [has_pow α β] (a : αᵒᵈ) (b : β) : of_dual (a ^ b) = of_dual a ^ b := rfl
+@[simp, to_additive to_dual_smul', to_additive_reorder 1 4]
+lemma pow_to_dual [has_pow α β] (a : α) (b : β) : a ^ to_dual b = a ^ b := rfl
+@[simp, to_additive of_dual_smul', to_additive_reorder 1 4]
+lemma pow_of_dual [has_pow α β] (a : α) (b : βᵒᵈ) : a ^ of_dual b = a ^ b := rfl
 
 /-! ### Lexicographical order -/
 
@@ -76,7 +85,9 @@ lemma of_dual_pow [has_pow α β] (a : αᵒᵈ) (b : β) : of_dual (a ^ b) = of
 @[to_additive] instance [h : has_inv α] : has_inv (lex α) := h
 @[to_additive] instance [h : has_div α] : has_div (lex α) := h
 @[to_additive] instance [h : has_smul α β] : has_smul α (lex β) := h
+@[to_additive] instance lex.has_smul' [h : has_smul α β] : has_smul (lex α) β := h
 @[to_additive lex.has_smul] instance lex.has_pow [h : has_pow α β] : has_pow (lex α) β := h
+@[to_additive lex.has_smul'] instance lex.has_pow' [h : has_pow α β] : has_pow α (lex β) := h
 @[to_additive] instance [h : semigroup α] : semigroup (lex α) := h
 @[to_additive] instance [h : comm_semigroup α] : comm_semigroup (lex α) := h
 @[to_additive] instance [h : left_cancel_semigroup α] : left_cancel_semigroup (lex α) := h
@@ -102,20 +113,26 @@ instance [h : division_comm_monoid α] : division_comm_monoid (lex α) := h
 @[simp, to_additive]
 lemma to_lex_mul [has_mul α] (a b : α) : to_lex (a * b) = to_lex a * to_lex b := rfl
 @[simp, to_additive]
-lemma of_lex_mul [has_mul α] (a b : αᵒᵈ) : of_lex (a * b) = of_lex a * of_lex b := rfl
+lemma of_lex_mul [has_mul α] (a b : lex α) : of_lex (a * b) = of_lex a * of_lex b := rfl
 @[simp, to_additive] lemma to_lex_inv [has_inv α] (a : α) : to_lex a⁻¹ = (to_lex a)⁻¹ := rfl
-@[simp, to_additive] lemma of_lex_inv [has_inv α] (a : αᵒᵈ) : of_lex a⁻¹ = (of_lex a)⁻¹ := rfl
+@[simp, to_additive] lemma of_lex_inv [has_inv α] (a : lex α) : of_lex a⁻¹ = (of_lex a)⁻¹ := rfl
 @[simp, to_additive]
 lemma to_lex_div [has_div α] (a b : α) : to_lex (a / b) = to_lex a / to_lex b := rfl
 @[simp, to_additive]
-lemma of_lex_div [has_div α] (a b : αᵒᵈ) : of_lex (a / b) = of_lex a / of_lex b := rfl
-lemma to_lex_vadd [has_vadd α β] (a : α) (b : β) : to_lex (a +ᵥ b) = a +ᵥ to_lex b := rfl
-lemma of_lex_vadd [has_vadd α β] (a : α) (b : βᵒᵈ) : of_lex (a +ᵥ b) = a +ᵥ of_lex b := rfl
+lemma of_lex_div [has_div α] (a b : lex α) : of_lex (a / b) = of_lex a / of_lex b := rfl
 @[simp, to_additive]
 lemma to_lex_smul [has_smul α β] (a : α) (b : β) : to_lex (a • b) = a • to_lex b := rfl
 @[simp, to_additive]
-lemma of_lex_smul [has_smul α β] (a : α) (b : βᵒᵈ) : of_lex (a • b) = a • of_lex b := rfl
+lemma of_lex_smul [has_smul α β] (a : α) (b : lex β) : of_lex (a • b) = a • of_lex b := rfl
+@[simp, to_additive]
+lemma to_lex_smul' [has_smul α β] (a : α) (b : β) : to_lex a • b = a • b := rfl
+@[simp, to_additive]
+lemma of_lex_smul' [has_smul α β] (a : lex α) (b : β) : of_lex a • b = a • b := rfl
 @[simp, to_additive to_lex_smul, to_additive_reorder 1 4]
 lemma to_lex_pow [has_pow α β] (a : α) (b : β) : to_lex (a ^ b) = to_lex a ^ b := rfl
 @[simp, to_additive of_lex_smul, to_additive_reorder 1 4]
-lemma of_lex_pow [has_pow α β] (a : αᵒᵈ) (b : β) : of_lex (a ^ b) = of_lex a ^ b := rfl
+lemma of_lex_pow [has_pow α β] (a : lex α) (b : β) : of_lex (a ^ b) = of_lex a ^ b := rfl
+@[simp, to_additive to_lex_smul, to_additive_reorder 1 4]
+lemma pow_to_lex [has_pow α β] (a : α) (b : β) : a ^ to_lex b = a ^ b := rfl
+@[simp, to_additive of_lex_smul, to_additive_reorder 1 4]
+lemma pow_of_lex [has_pow α β] (a : α) (b : lex β) : a ^ of_lex b = a ^ b := rfl

src/topology/algebra/const_mul_action.lean

@@ -106,6 +106,11 @@ instance has_continuous_const_smul.op [has_smul Mᵐᵒᵖ α] [is_central_scala
   has_continuous_const_smul M αᵐᵒᵖ :=
 ⟨λ c, mul_opposite.continuous_op.comp $ mul_opposite.continuous_unop.const_smul c⟩
 
+@[to_additive] instance : has_continuous_const_smul M αᵒᵈ := ‹has_continuous_const_smul M α›
+
+@[to_additive] instance order_dual.has_continuous_const_smul' : has_continuous_const_smul Mᵒᵈ α :=
+‹has_continuous_const_smul M α›
+
 @[to_additive]
 instance [has_smul M β] [has_continuous_const_smul M β] :
   has_continuous_const_smul M (α × β) :=
@@ -356,7 +361,7 @@ export properly_discontinuous_vadd (finite_disjoint_inter_image)
 
 /-- The quotient map by a group action is open, i.e. the quotient by a group action is an open
   quotient. -/
-@[to_additive "The quotient map by a group action is open, i.e. the quotient by a group 
+@[to_additive "The quotient map by a group action is open, i.e. the quotient by a group
 action is an open quotient. "]
 lemma is_open_map_quotient_mk_mul [has_continuous_const_smul Γ T] :
   is_open_map (quotient.mk : T → quotient (mul_action.orbit_rel Γ T)) :=