chore: make pseudoparents of algebraic substructures reducible (leanprover-community#36097)

Make functions that take an algebraic substructure and return a sibling class reducible, this matches actual parents and resolves some usage of `set_option backward.isDefEq.respectTransparency false`. For example it ensures that the field instance on `IntermediateField` has a compatible `Semiring` instance to the one from it extending a `Subalgebra`.
Also remove @[simp] from `adjoin_toSubsemiring`, since it prevents other simp lemmas on `adjoin` from applying.

Co-authored-by: Matthew Jasper <mjjasper1@gmail.com>

Author: matthewjasper

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -178,11 +178,11 @@ instance instNonUnitalSubringClass : NonUnitalSubringClass (NonUnitalSubalgebra
     neg_mem {_ x} hx := neg_one_smul R x ▸ SMulMemClass.smul_mem _ hx }
 
 /-- A non-unital subalgebra over a ring is also a `Subring`. -/
+@[reducible]
 def toNonUnitalSubring (S : NonUnitalSubalgebra R A) : NonUnitalSubring A where
   toNonUnitalSubsemiring := S.toNonUnitalSubsemiring
   neg_mem' := neg_mem (s := S)
 
-@[simp]
 theorem mem_toNonUnitalSubring {S : NonUnitalSubalgebra R A} {x} :
     x ∈ S.toNonUnitalSubring ↔ x ∈ S :=
   Iff.rfl

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -192,6 +192,7 @@ protected theorem prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemir
   prod_mem h
 
 /-- Turn a `Subalgebra` into a `NonUnitalSubalgebra` by forgetting that it contains `1`. -/
+@[reducible]
 def toNonUnitalSubalgebra (S : Subalgebra R A) : NonUnitalSubalgebra R A where
   __ := S
   smul_mem' r _x hx := S.smul_mem hx r
@@ -208,7 +209,6 @@ lemma toNonUnitalSubalgebra_injective : Function.Injective
     (toNonUnitalSubalgebra : Subalgebra R A → NonUnitalSubalgebra R A) :=
   fun _ _ ↦ by simp [SetLike.ext_iff]
 
-@[simp]
 lemma toNonUnitalSubalgebra_inj {S U : Subalgebra R A} :
     S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra ↔ S = U :=
   toNonUnitalSubalgebra_injective.eq_iff
@@ -234,7 +234,7 @@ protected theorem intCast_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [A
   intCast_mem S n
 
 /-- The projection from a subalgebra of `A` to an additive submonoid of `A`. -/
-@[simps coe]
+@[reducible]
 def toAddSubmonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A]
     (S : Subalgebra R A) : AddSubmonoid A :=
   S.toSubsemiring.toAddSubmonoid
@@ -316,13 +316,13 @@ section
 
 instance (priority := low) module' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] :
     Module R' S :=
-  S.toSubmodule.module'
+  inferInstance
 
 instance : Module R S :=
-  S.module'
+  inferInstance
 
 instance [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : IsScalarTower R' R S :=
-  inferInstanceAs (IsScalarTower R' R (toSubmodule S))
+  inferInstance
 
 /- More general form of `Subalgebra.algebra`.
 

Mathlib/Algebra/Field/Subfield/Defs.lean

@@ -141,6 +141,7 @@ add_decl_doc Subfield.toSubring
 namespace Subfield
 
 /-- The underlying `AddSubgroup` of a subfield. -/
+@[reducible]
 def toAddSubgroup (s : Subfield K) : AddSubgroup K :=
   { s.toSubring.toAddSubgroup with }
 
@@ -345,7 +346,6 @@ theorem mem_toSubmonoid {s : Subfield K} {x : K} : x ∈ s.toSubmonoid ↔ x ∈
 theorem coe_toSubmonoid : (s.toSubmonoid : Set K) = s :=
   rfl
 
-@[simp]
 theorem mem_toAddSubgroup {s : Subfield K} {x : K} : x ∈ s.toAddSubgroup ↔ x ∈ s :=
   Iff.rfl
 

Mathlib/Algebra/Ring/Subring/Defs.lean

@@ -222,6 +222,7 @@ instance : SubringClass (Subring R) R where
   neg_mem {s} := s.neg_mem'
 
 /-- Turn a `Subring` into a `NonUnitalSubring` by forgetting that it contains `1`. -/
+@[reducible]
 def toNonUnitalSubring (S : Subring R) : NonUnitalSubring R where __ := S
 
 @[simp]

Mathlib/Algebra/Ring/Subsemiring/Defs.lean

@@ -174,6 +174,7 @@ instance : SubsemiringClass (Subsemiring R) R where
   mul_mem {s} := Subsemigroup.mul_mem' s.toSubmonoid.toSubsemigroup
 
 /-- Turn a `Subsemiring` into a `NonUnitalSubsemiring` by forgetting that it contains `1`. -/
+@[reducible]
 def toNonUnitalSubsemiring (S : Subsemiring R) : NonUnitalSubsemiring R where __ := S
 
 @[simp]
@@ -224,7 +225,6 @@ lemma toNonUnitalSubsemiring_injective :
   fun S₁ S₂ h => SetLike.ext'_iff.2
     (show (S₁.toNonUnitalSubsemiring : Set R) = S₂ from SetLike.ext'_iff.1 h)
 
-@[simp]
 lemma toNonUnitalSubsemiring_inj {S₁ S₂ : Subsemiring R} :
     S₁.toNonUnitalSubsemiring = S₂.toNonUnitalSubsemiring ↔ S₁ = S₂ :=
   toNonUnitalSubsemiring_injective.eq_iff

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -215,12 +215,12 @@ theorem copy_eq (S : NonUnitalStarSubalgebra R A) (s : Set A) (hs : s = ↑S) :
 variable (S : NonUnitalStarSubalgebra R A)
 
 /-- A non-unital star subalgebra over a ring is also a `Subring`. -/
+@[reducible]
 def toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A]
     [Star A] (S : NonUnitalStarSubalgebra R A) : NonUnitalSubring A where
   toNonUnitalSubsemiring := S.toNonUnitalSubsemiring
   neg_mem' := neg_mem (s := S)
 
-@[simp]
 theorem mem_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A]
     [Star A] {S : NonUnitalStarSubalgebra R A} {x} : x ∈ S.toNonUnitalSubring ↔ x ∈ S :=
   Iff.rfl

Mathlib/Algebra/Star/Subalgebra.lean

@@ -104,6 +104,7 @@ instance starModule (s : StarSubalgebra R A) : StarModule R s where
   star_smul r a := Subtype.ext (star_smul r (a : A))
 
 /-- Turn a `StarSubalgebra` into a `NonUnitalStarSubalgebra` by forgetting that it contains `1`. -/
+@[reducible]
 def toNonUnitalStarSubalgebra (S : StarSubalgebra R A) : NonUnitalStarSubalgebra R A where
   __ := S
   smul_mem' r _x hx := S.smul_mem hx r
@@ -120,7 +121,6 @@ lemma toNonUnitalStarSubalgebra_injective : Function.Injective
     (toNonUnitalStarSubalgebra : StarSubalgebra R A → NonUnitalStarSubalgebra R A) :=
   fun _ _ ↦ by simp [SetLike.ext_iff]
 
-@[simp]
 lemma toNonUnitalStarSubalgebra_inj {S U : StarSubalgebra R A} :
     S.toNonUnitalStarSubalgebra = U.toNonUnitalStarSubalgebra ↔ S = U :=
   toNonUnitalStarSubalgebra_injective.eq_iff

Mathlib/RingTheory/NonUnitalSubring/Defs.lean

@@ -129,6 +129,7 @@ add_decl_doc NonUnitalSubring.toAddSubgroup
 namespace NonUnitalSubring
 
 /-- The underlying submonoid of a `NonUnitalSubring`. -/
+@[reducible]
 def toSubsemigroup (s : NonUnitalSubring R) : Subsemigroup R :=
   { s.toNonUnitalSubsemiring.toSubsemigroup with carrier := s.carrier }
 
@@ -329,7 +330,6 @@ instance toNonUnitalCommRing {R} [NonUnitalCommRing R] (s : NonUnitalSubring R)
 /-! ## Partial order -/
 
 
-@[simp]
 theorem mem_toSubsemigroup {s : NonUnitalSubring R} {x : R} : x ∈ s.toSubsemigroup ↔ x ∈ s :=
   Iff.rfl