refactor(*): Protect Function.Commute (#6456)

This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.

Author: tb65536

Mathlib/Algebra/Hom/Iterate.lean

@@ -239,7 +239,7 @@ theorem SemiconjBy.function_semiconj_mul_left (h : SemiconjBy a b c) :
 #align add_semiconj_by.function_semiconj_add_left AddSemiconjBy.function_semiconj_add_left
 
 @[to_additive]
-theorem Commute.function_commute_mul_left (h : _root_.Commute a b) :
+theorem Commute.function_commute_mul_left (h : Commute a b) :
     Function.Commute (a * ·) (b * ·) :=
   SemiconjBy.function_semiconj_mul_left h
 #align commute.function_commute_mul_left Commute.function_commute_mul_left
@@ -252,7 +252,7 @@ theorem SemiconjBy.function_semiconj_mul_right_swap (h : SemiconjBy a b c) :
 #align add_semiconj_by.function_semiconj_add_right_swap AddSemiconjBy.function_semiconj_add_right_swap
 
 @[to_additive]
-theorem Commute.function_commute_mul_right (h : _root_.Commute a b) :
+theorem Commute.function_commute_mul_right (h : Commute a b) :
   Function.Commute (· * a) (· * b) :=
   SemiconjBy.function_semiconj_mul_right_swap h
 #align commute.function_commute_mul_right Commute.function_commute_mul_right

Mathlib/Data/Fintype/Card.lean

@@ -1062,7 +1062,7 @@ instance Prod.infinite_of_left [Infinite α] [Nonempty β] : Infinite (α × β)
 #align prod.infinite_of_left Prod.infinite_of_left
 
 instance instInfiniteProdSubtypeCommute [Mul α] [Infinite α] :
-    Infinite { p : α × α // _root_.Commute p.1 p.2 } :=
+    Infinite { p : α × α // Commute p.1 p.2 } :=
   Infinite.of_injective (fun a => ⟨⟨a, a⟩, rfl⟩) (by intro; simp)
 
 namespace Infinite

Mathlib/Dynamics/FixedPoints/Basic.lean

@@ -33,6 +33,8 @@ variable {α : Type u} {β : Type v} {f fa g : α → α} {x y : α} {fb : β 
 
 namespace Function
 
+open Function (Commute)
+
 /-- A point `x` is a fixed point of `f : α → α` if `f x = x`. -/
 def IsFixedPt (f : α → α) (x : α) :=
   f x = x

Mathlib/Dynamics/PeriodicPts.lean

@@ -46,6 +46,8 @@ open Set
 
 namespace Function
 
+open Function (Commute)
+
 variable {α : Type*} {β : Type*} {f fa : α → α} {fb : β → β} {x y : α} {m n : ℕ}
 
 /-- A point `x` is a periodic point of `f : α → α` of period `n` if `f^[n] x = x`.
@@ -421,18 +423,18 @@ theorem minimalPeriod_eq_prime_pow {p k : ℕ} [hp : Fact p.Prime] (hk : ¬IsPer
     rwa [← isPeriodicPt_iff_minimalPeriod_dvd]
 #align function.minimal_period_eq_prime_pow Function.minimalPeriod_eq_prime_pow
 
-theorem Commute.minimalPeriod_of_comp_dvd_lcm {g : α → α} (h : Function.Commute f g) :
+theorem Commute.minimalPeriod_of_comp_dvd_lcm {g : α → α} (h : Commute f g) :
     minimalPeriod (f ∘ g) x ∣ Nat.lcm (minimalPeriod f x) (minimalPeriod g x) := by
   rw [← isPeriodicPt_iff_minimalPeriod_dvd]
   exact (isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)
 #align function.commute.minimal_period_of_comp_dvd_lcm Function.Commute.minimalPeriod_of_comp_dvd_lcm
 
-theorem Commute.minimalPeriod_of_comp_dvd_mul {g : α → α} (h : Function.Commute f g) :
+theorem Commute.minimalPeriod_of_comp_dvd_mul {g : α → α} (h : Commute f g) :
     minimalPeriod (f ∘ g) x ∣ minimalPeriod f x * minimalPeriod g x :=
   dvd_trans h.minimalPeriod_of_comp_dvd_lcm (lcm_dvd_mul _ _)
 #align function.commute.minimal_period_of_comp_dvd_mul Function.Commute.minimalPeriod_of_comp_dvd_mul
 
-theorem Commute.minimalPeriod_of_comp_eq_mul_of_coprime {g : α → α} (h : Function.Commute f g)
+theorem Commute.minimalPeriod_of_comp_eq_mul_of_coprime {g : α → α} (h : Commute f g)
     (hco : coprime (minimalPeriod f x) (minimalPeriod g x)) :
     minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x := by
   apply h.minimalPeriod_of_comp_dvd_mul.antisymm

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -418,14 +418,14 @@ section conjClasses
 open Fintype
 
 theorem card_comm_eq_card_conjClasses_mul_card (G : Type*) [Group G] :
-    Nat.card { p : G × G // _root_.Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G := by
+    Nat.card { p : G × G // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G := by
   classical
   rcases fintypeOrInfinite G; swap
   · rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
   simp only [Nat.card_eq_fintype_card]
   -- Porting note: Changed `calc` proof into a `rw` proof.
-  rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype _root_.Commute), card_sigma,
-    sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // _root_.Commute a b })
+  rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute), card_sigma,
+    sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
       (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g))
       fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
     MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group]

Mathlib/GroupTheory/OrderOfElement.lean

@@ -375,7 +375,7 @@ theorem orderOf_pow_coprime (h : (orderOf y).coprime m) : orderOf (y ^ m) = orde
 
 namespace Commute
 
-variable {x} (h : _root_.Commute x y)
+variable {x} (h : Commute x y)
 
 @[to_additive]
 theorem orderOf_mul_dvd_lcm : orderOf (x * y) ∣ Nat.lcm (orderOf x) (orderOf y) := by

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -1106,7 +1106,7 @@ theorem pow_apply_eq_pow_mod_orderOf_cycleOf_apply (f : Perm α) (n : ℕ) (x :
   rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_eq_mod_orderOf]
 #align equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply Equiv.Perm.pow_apply_eq_pow_mod_orderOf_cycleOf_apply
 
-theorem cycleOf_mul_of_apply_right_eq_self (h : _root_.Commute f g) (x : α) (hx : g x = x) :
+theorem cycleOf_mul_of_apply_right_eq_self (h : Commute f g) (x : α) (hx : g x = x) :
     (f * g).cycleOf x = f.cycleOf x := by
   ext y
   by_cases hxy : (f * g).SameCycle x y

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -3622,7 +3622,7 @@ theorem SubgroupNormal.mem_comm {H K : Subgroup G} (hK : H ≤ K) [hN : (H.subgr
 @[to_additive "Elements of disjoint, normal subgroups commute."]
 theorem commute_of_normal_of_disjoint (H₁ H₂ : Subgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal)
     -- Porting note: Goal was `Commute x y`. Removed ambiguity.
-    (hdis : Disjoint H₁ H₂) (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : _root_.Commute x y := by
+    (hdis : Disjoint H₁ H₂) (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : Commute x y := by
   suffices x * y * x⁻¹ * y⁻¹ = 1 by
     show x * y = y * x
     · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this

Mathlib/GroupTheory/Sylow.lean

@@ -785,7 +785,7 @@ noncomputable def directProductOfNormal [Fintype G]
   set ps := (Fintype.card G).factorization.support
   -- “The” Sylow subgroup for p
   let P : ∀ p, Sylow p G := default
-  have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → _root_.Commute x y := by
+  have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y := by
     rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
     haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁)
     haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂)

Mathlib/Logic/Function/Conjugate.lean

@@ -81,10 +81,12 @@ Two maps `f g : α → α` commute if `f (g x) = g (f x)` for all `x : α`.
 Given `h : Function.commute f g` and `a : α`, we have `h a : f (g a) = g (f a)` and
 `h.comp_eq : f ∘ g = g ∘ f`.
 -/
-def Commute (f g : α → α) : Prop :=
+protected def Commute (f g : α → α) : Prop :=
   Semiconj f g g
 #align function.commute Function.Commute
 
+open Function (Commute)
+
 /-- Reinterpret `Function.Semiconj f g g` as `Function.Commute f g`. These two predicates are
 definitionally equal but have different dot-notation lemmas. -/
 theorem Semiconj.commute {f g : α → α} (h : Semiconj f g g) : Commute f g := h