feat(algebra/group/conj): instances + misc (#13943)

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/algebra/group/conj.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2018  Patrick Massot. All rights reserved.
+Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Chris Hughes, Michael Howes
 -/
@@ -31,6 +31,9 @@ def is_conj (a b : α) := ∃ c : αˣ, semiconj_by ↑c a b
 @[symm] lemma is_conj.symm {a b : α} : is_conj a b → is_conj b a
 | ⟨c, hc⟩ := ⟨c⁻¹, hc.units_inv_symm_left⟩
 
+lemma is_conj_comm {g h : α} : is_conj g h ↔ is_conj h g :=
+⟨is_conj.symm, is_conj.symm⟩
+
 @[trans] lemma is_conj.trans {a b c : α} : is_conj a b → is_conj b c → is_conj a c
 | ⟨c₁, hc₁⟩ ⟨c₂, hc₂⟩ := ⟨c₂ * c₁, hc₂.mul_left hc₁⟩
 
@@ -46,9 +49,11 @@ protected lemma monoid_hom.map_is_conj (f : α →* β) {a b : α} : is_conj a b
 end monoid
 
 section cancel_monoid
+
 variables [cancel_monoid α]
--- These lemmas hold for either `left_cancel_monoid` or `right_cancel_monoid`,
--- with slightly different proofs; so far these don't seem necessary.
+-- These lemmas hold for `right_cancel_monoid` with the current proofs, but for the sake of
+-- not duplicating code (these lemmas also hold for `left_cancel_monoids`) we leave these
+-- not generalised.
 
 @[simp] lemma is_conj_one_right {a : α} : is_conj 1 a  ↔ a = 1 :=
 ⟨λ ⟨c, hc⟩, mul_right_cancel (hc.symm.trans ((mul_one _).trans (one_mul _).symm)), λ h, by rw [h]⟩
@@ -172,6 +177,43 @@ instance [fintype α] [decidable_rel (is_conj : α → α → Prop)] :
   fintype (conj_classes α) :=
 quotient.fintype (is_conj.setoid α)
 
+/--
+Certain instances trigger further searches when they are considered as candidate instances;
+these instances should be assigned a priority lower than the default of 1000 (for example, 900).
+
+The conditions for this rule are as follows:
+ * a class `C` has instances `instT : C T` and `instT' : C T'`
+ * types `T` and `T'` are both specializations of another type `S`
+ * the parameters supplied to `S` to produce `T` are not (fully) determined by `instT`,
+   instead they have to be found by instance search
+If those conditions hold, the instance `instT` should be assigned lower priority.
+
+For example, suppose the search for an instance of `decidable_eq (multiset α)` tries the
+candidate instance `con.quotient.decidable_eq (c : con M) : decidable_eq c.quotient`.
+Since `multiset` and `con.quotient` are both quotient types, unification will check
+that the relations `list.perm` and `c.to_setoid.r` unify. However, `c.to_setoid` depends on 
+a `has_mul M` instance, so this unification triggers a search for `has_mul (list α)`;
+this will traverse all subclasses of `has_mul` before failing.
+On the other hand, the search for an instance of `decidable_eq (con.quotient c)` for `c : con M`
+can quickly reject the candidate instance `multiset.has_decidable_eq` because the type of
+`list.perm : list ?m_1 → list ?m_1 → Prop` does not unify with `M → M → Prop`.
+Therefore, we should assign `con.quotient.decidable_eq` a lower priority because it fails slowly.
+(In terms of the rules above, `C := decidable_eq`, `T := con.quotient`,
+`instT := con.quotient.decidable_eq`, `T' := multiset`, `instT' := multiset.has_decidable_eq`,
+and `S := quot`.)
+
+If the type involved is a free variable (rather than an instantiation of some type `S`),
+the instance priority should be even lower, see Note [lower instance priority].
+-/
+library_note "slow-failing instance priority"
+
+@[priority 900] -- see Note [slow-failing instance priority]
+instance [decidable_rel (is_conj : α → α → Prop)] : decidable_eq (conj_classes α) :=
+quotient.decidable_eq
+
+instance [decidable_eq α] [fintype α] : decidable_rel (is_conj : α → α → Prop) :=
+λ a b, by { delta is_conj semiconj_by, apply_instance }
+
 end monoid
 
 section comm_monoid
@@ -215,6 +257,9 @@ lemma is_conj_iff_conjugates_of_eq {a b : α} :
   rwa ← h at ha,
 end⟩
 
+instance [fintype α] [decidable_rel (is_conj : α → α → Prop)] {a : α} : fintype (conjugates_of a) :=
+@subtype.fintype _ _ (‹decidable_rel is_conj› a) _
+
 end monoid
 
 namespace conj_classes
@@ -243,4 +288,13 @@ lemma carrier_eq_preimage_mk {a : conj_classes α} :
   a.carrier = conj_classes.mk ⁻¹' {a} :=
 set.ext (λ x, mem_carrier_iff_mk_eq)
 
+section fintype
+
+variables [fintype α] [decidable_rel (is_conj : α → α → Prop)]
+
+instance {x : conj_classes α} : fintype (carrier x) :=
+quotient.rec_on_subsingleton x $ λ a, conjugates_of.fintype
+
+end fintype
+
 end conj_classes

src/group_theory/commuting_probability.lean

@@ -56,9 +56,9 @@ end
 
 variables (G : Type*) [group G] [fintype G]
 
-lemma card_comm_eq_card_conj_classes_mul_card :
-  card {p : G × G // p.1 * p.2 = p.2 * p.1} = card (conj_classes G) * card G :=
-calc card {p : G × G // p.1 * p.2 = p.2 * p.1} = card (Σ g, {h // g * h = h * g}) :
+lemma card_comm_eq_card_conj_classes_mul_card [h : fintype (conj_classes G)] :
+  card {p : G × G // p.1 * p.2 = p.2 * p.1} = @card (conj_classes G) h * card G :=
+by convert calc card {p : G × G // p.1 * p.2 = p.2 * p.1} = card (Σ g, {h // g * h = h * g}) :
   card_congr (equiv.subtype_prod_equiv_sigma_subtype (λ g h : G, g * h = h * g))
 ... = ∑ g, card {h // g * h = h * g} : card_sigma _
 ... = ∑ g, card (mul_action.fixed_by (conj_act G) G g) : sum_equiv conj_act.to_conj_act.to_equiv
@@ -97,8 +97,9 @@ begin
     conjugacy classes as `G ⧸ H`. -/
   rw [comm_prob_def', comm_prob_def', div_le_iff, mul_assoc, ←nat.cast_mul, mul_comm (card H),
       ←subgroup.card_eq_card_quotient_mul_card_subgroup, div_mul_cancel, nat.cast_le],
-  { exact card_le_of_surjective (conj_classes.map (quotient_group.mk' H))
-      (conj_classes.map_surjective quotient.surjective_quotient_mk') },
+  { apply card_le_of_surjective,
+    show function.surjective (conj_classes.map (quotient_group.mk' H)),
+    exact (conj_classes.map_surjective quotient.surjective_quotient_mk') },
   { exact nat.cast_ne_zero.mpr card_ne_zero },
   { exact nat.cast_pos.mpr card_pos },
 end