chore: make fields of algebraic (iso)morphisms protected (#7150)

Pretty much all these fields are implementation details, and not intended as API. There is no point in `open MonoidHom` bringing `toFun` or `map_mul'` into the environment, as neither are the preferred way to spell those things.

Mathlib/Algebra/Algebra/Equiv.lean

@@ -32,7 +32,7 @@ universe u v w u₁ v₁
 structure AlgEquiv (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B]
   [Algebra R A] [Algebra R B] extends A ≃ B, A ≃* B, A ≃+ B, A ≃+* B where
   /-- An equivalence of algebras commutes with the action of scalars. -/
-  commutes' : ∀ r : R, toFun (algebraMap R A r) = algebraMap R B r
+  protected commutes' : ∀ r : R, toFun (algebraMap R A r) = algebraMap R B r
 #align alg_equiv AlgEquiv
 
 attribute [nolint docBlame] AlgEquiv.toRingEquiv
@@ -108,9 +108,9 @@ instance : AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂ where
     obtain ⟨⟨f,_⟩,_⟩ := f
     obtain ⟨⟨g,_⟩,_⟩ := g
     congr
-  map_add := map_add'
-  map_mul := map_mul'
-  commutes := commutes'
+  map_add f := f.map_add'
+  map_mul f := f.map_mul'
+  commutes f := f.commutes'
   left_inv f := f.left_inv
   right_inv f := f.right_inv
 

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -205,7 +205,7 @@ instance [Mul M] [Mul N] : MulEquivClass (M ≃* N) M N where
     cases g
     congr
     apply Equiv.coe_fn_injective h₁
-  map_mul := map_mul'
+  map_mul f := f.map_mul'
 
 @[to_additive] -- shortcut instance that doesn't generate any subgoals
 instance [Mul M] [Mul N] : CoeFun (M ≃* N) fun _ => M → N where

Mathlib/Algebra/Hom/Group/Defs.lean

@@ -80,9 +80,9 @@ When you extend this structure, make sure to also extend `ZeroHomClass`.
 -/
 structure ZeroHom (M : Type*) (N : Type*) [Zero M] [Zero N] where
   /-- The underlying function -/
-  toFun : M → N
+  protected toFun : M → N
   /-- The proposition that the function preserves 0 -/
-  map_zero' : toFun 0 = 0
+  protected map_zero' : toFun 0 = 0
 #align zero_hom ZeroHom
 #align zero_hom.map_zero' ZeroHom.map_zero'
 
@@ -111,9 +111,9 @@ When you extend this structure, make sure to extend `AddHomClass`.
 -/
 structure AddHom (M : Type*) (N : Type*) [Add M] [Add N] where
   /-- The underlying function -/
-  toFun : M → N
+  protected toFun : M → N
   /-- The proposition that the function preserves addition -/
-  map_add' : ∀ x y, toFun (x + y) = toFun x + toFun y
+  protected map_add' : ∀ x y, toFun (x + y) = toFun x + toFun y
 #align add_hom AddHom
 
 /-- `AddHomClass F M N` states that `F` is a type of addition-preserving homomorphisms.
@@ -175,9 +175,9 @@ When you extend this structure, make sure to also extend `OneHomClass`.
 @[to_additive]
 structure OneHom (M : Type*) (N : Type*) [One M] [One N] where
   /-- The underlying function -/
-  toFun : M → N
+  protected toFun : M → N
   /-- The proposition that the function preserves 1 -/
-  map_one' : toFun 1 = 1
+  protected map_one' : toFun 1 = 1
 #align one_hom OneHom
 
 /-- `OneHomClass F M N` states that `F` is a type of one-preserving homomorphisms.
@@ -267,9 +267,9 @@ When you extend this structure, make sure to extend `MulHomClass`.
 @[to_additive]
 structure MulHom (M : Type*) (N : Type*) [Mul M] [Mul N] where
   /-- The underlying function -/
-  toFun : M → N
+  protected toFun : M → N
   /-- The proposition that the function preserves multiplication -/
-  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y
+  protected map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y
 #align mul_hom MulHom
 
 /-- `M →ₙ* N` denotes the type of multiplication-preserving maps from `M` to `N`. -/

Mathlib/Algebra/Hom/GroupAction.lean

@@ -61,9 +61,9 @@ variable (T : Type*) [Semiring T] [MulSemiringAction M T]
 -- @[nolint has_nonempty_instance]
 structure MulActionHom where
   /-- The underlying function. -/
-  toFun : X → Y
+  protected toFun : X → Y
   /-- The proposition that the function preserves the action. -/
-  map_smul' : ∀ (m : M') (x : X), toFun (m • x) = m • toFun x
+  protected map_smul' : ∀ (m : M') (x : X), toFun (m • x) = m • toFun x
 #align mul_action_hom MulActionHom
 
 /- Porting note: local notation given a name, conflict with Algebra.Hom.GroupAction

Mathlib/Algebra/Module/LinearMap.lean

@@ -92,7 +92,7 @@ structure LinearMap {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R 
     AddHom M M₂ where
   /-- A linear map preserves scalar multiplication.
   We prefer the spelling `_root_.map_smul` instead. -/
-  map_smul' : ∀ (r : R) (x : M), toFun (r • x) = σ r • toFun x
+  protected map_smul' : ∀ (r : R) (x : M), toFun (r • x) = σ r • toFun x
 #align linear_map LinearMap
 
 /-- The `AddHom` underlying a `LinearMap`. -/

Mathlib/Algebra/Ring/Equiv.lean

@@ -144,8 +144,8 @@ instance : RingEquivClass (R ≃+* S) R S where
     cases f
     congr
     apply Equiv.coe_fn_injective h₁
-  map_add := map_add'
-  map_mul := map_mul'
+  map_add f := f.map_add'
+  map_mul f := f.map_mul'
   left_inv f := f.left_inv
   right_inv f := f.right_inv
 

Mathlib/LinearAlgebra/Matrix/Determinant.lean

@@ -669,9 +669,8 @@ theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Mat
     · intro σ₁ σ₂ h₁ h₂
       dsimp only
       intro h
-      have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x := by
-        intro x
-        exact congr_fun (congr_arg toFun h) x
+      have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
+        FunLike.congr_fun h
       simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
         Sum.inr.injEq] at h2
       ext x

Mathlib/Logic/Equiv/Defs.lean

@@ -65,10 +65,10 @@ variable {α : Sort u} {β : Sort v} {γ : Sort w}
 
 /-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
 structure Equiv (α : Sort*) (β : Sort _) where
-  toFun : α → β
-  invFun : β → α
-  left_inv : LeftInverse invFun toFun
-  right_inv : RightInverse invFun toFun
+  protected toFun : α → β
+  protected invFun : β → α
+  protected left_inv : LeftInverse invFun toFun
+  protected right_inv : RightInverse invFun toFun
 #align equiv Equiv
 
 infixl:25 " ≃ " => Equiv
@@ -95,10 +95,10 @@ def Equiv.Perm (α : Sort*) :=
 namespace Equiv
 
 instance : EquivLike (α ≃ β) α β where
-  coe := toFun
-  inv := invFun
-  left_inv := left_inv
-  right_inv := right_inv
+  coe := Equiv.toFun
+  inv := Equiv.invFun
+  left_inv := Equiv.left_inv
+  right_inv := Equiv.right_inv
   coe_injective' e₁ e₂ h₁ h₂ := by cases e₁; cases e₂; congr
 
 /-- Helper instance when inference gets stuck on following the normal chain