refactor(ring_theory/algebra): re-bundle subalgebra (#4180)

This PR makes `subalgebra` extend `subsemiring` instead of using `subsemiring` as a field in its definition. The refactor is needed because `intermediate_field` should simultaneously extend `subalgebra` and `subfield`, and so the type of the `carrier` fields should match.

I added some copies of definitions that use `subring` instead of `is_subring` if I needed to change these definitions anyway.

Author: Vierkantor

src/algebra/category/Algebra/limits.lean

@@ -39,8 +39,8 @@ The flat sections of a functor into `Algebra R` form a submodule of all sections
 -/
 def sections_subalgebra (F : J ⥤ Algebra R) :
   subalgebra R (Π j, F.obj j) :=
-{ carrier := SemiRing.sections_subsemiring (F ⋙ forget₂ (Algebra R) Ring ⋙ forget₂ Ring SemiRing),
-  algebra_map_mem' := λ r j j' f, (F.map f).commutes r, }
+{ algebra_map_mem' := λ r j j' f, (F.map f).commutes r,
+  ..SemiRing.sections_subsemiring (F ⋙ forget₂ (Algebra R) Ring ⋙ forget₂ Ring SemiRing) }
 
 
 instance limit_semiring (F : J ⥤ Algebra R) :

src/field_theory/adjoin.lean

@@ -32,12 +32,11 @@ variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)
 `adjoin F S` extends a field `F` by adjoining a set `S ⊆ E`.
 -/
 def adjoin : subalgebra F E :=
-{ carrier :=
-  { carrier := field.closure (set.range (algebra_map F E) ∪ S),
-    one_mem' := is_submonoid.one_mem,
-    mul_mem' := λ x y, is_submonoid.mul_mem,
-    zero_mem' := is_add_submonoid.zero_mem,
-    add_mem' := λ x y, is_add_submonoid.add_mem },
+{ carrier := field.closure (set.range (algebra_map F E) ∪ S),
+  one_mem' := is_submonoid.one_mem,
+  mul_mem' := λ x y, is_submonoid.mul_mem,
+  zero_mem' := is_add_submonoid.zero_mem,
+  add_mem' := λ x y, is_add_submonoid.add_mem,
   algebra_map_mem' := λ x, field.mem_closure (or.inl (set.mem_range.mpr ⟨x,rfl⟩)) }
 
 lemma adjoin.algebra_map_mem (x : F) : algebra_map F E x ∈ adjoin F S :=

src/field_theory/fixed.lean

@@ -64,7 +64,7 @@ polynomial.induction_on p
   (λ n x ih, by rw [smul_mul', polynomial.smul_C, smul, smul_pow, polynomial.smul_X])
 
 instance : algebra (fixed_points G F) F :=
-algebra.of_subring _
+algebra.of_is_subring _
 
 theorem coe_algebra_map :
   algebra_map (fixed_points G F) F = is_subring.subtype (fixed_points G F) :=

src/field_theory/splitting_field.lean

@@ -328,11 +328,11 @@ alg_equiv.symm $ alg_equiv.of_bijective
   (alg_hom.cod_restrict
     (adjoin_root.alg_hom _ x $ minimal_polynomial.aeval hx) _
     (λ p, adjoin_root.induction_on _ p $ λ p,
-      (algebra.adjoin_singleton_eq_range F x).symm ▸ ⟨p, rfl⟩))
+      (algebra.adjoin_singleton_eq_range F x).symm ▸ (polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩))
   ⟨(alg_hom.injective_cod_restrict _ _ _).2 $ (alg_hom.injective_iff _).2 $ λ p,
     adjoin_root.induction_on _ p $ λ p hp, ideal.quotient.eq_zero_iff_mem.2 $
     ideal.mem_span_singleton.2 $ minimal_polynomial.dvd hx hp,
-  λ y, let ⟨p, hp⟩ := (subalgebra.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) y).1 y.2 in
+  λ y, let ⟨p, _, hp⟩ := (subalgebra.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) y).1 y.2 in
   ⟨adjoin_root.mk _ p, subtype.eq hp⟩⟩
 
 open finset

src/field_theory/subfield.lean

@@ -61,7 +61,6 @@ subfield, subfields
 open_locale big_operators
 universes u v w
 
-open group
 variables {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M]
 
 set_option old_structure_cmd true

src/ring_theory/adjoin.lean

@@ -96,18 +96,20 @@ le_antisymm
 theorem adjoin_eq_range :
   adjoin R s = (mv_polynomial.aeval (coe : s → A)).range :=
 le_antisymm
-  (adjoin_le $ λ x hx, ⟨mv_polynomial.X ⟨x, hx⟩, mv_polynomial.eval₂_X _ _ _⟩)
-  (λ x ⟨p, hp⟩, hp ▸ mv_polynomial.induction_on p
-    (λ r, by rw [mv_polynomial.aeval_def, mv_polynomial.eval₂_C]; exact (adjoin R s).2 r)
+  (adjoin_le $ λ x hx, ⟨mv_polynomial.X ⟨x, hx⟩, set.mem_univ _, mv_polynomial.eval₂_X _ _ _⟩)
+  (λ x ⟨p, _, (hp : mv_polynomial.aeval coe p = x)⟩, hp ▸ mv_polynomial.induction_on p
+    (λ r, by { rw [mv_polynomial.aeval_def, mv_polynomial.eval₂_C],
+               exact (adjoin R s).algebra_map_mem r })
     (λ p q hp hq, by rw alg_hom.map_add; exact is_add_submonoid.add_mem hp hq)
     (λ p ⟨n, hn⟩ hp, by rw [alg_hom.map_mul, mv_polynomial.aeval_def _ (mv_polynomial.X _),
       mv_polynomial.eval₂_X]; exact is_submonoid.mul_mem hp (subset_adjoin hn)))
 
 theorem adjoin_singleton_eq_range (x : A) : adjoin R {x} = (polynomial.aeval x).range :=
 le_antisymm
-  (adjoin_le $ set.singleton_subset_iff.2 ⟨polynomial.X, polynomial.eval₂_X _ _⟩)
-  (λ y ⟨p, hp⟩, hp ▸ polynomial.induction_on p
-    (λ r, by rw [polynomial.aeval_def, polynomial.eval₂_C]; exact (adjoin R _).2 r)
+  (adjoin_le $ set.singleton_subset_iff.2 ⟨polynomial.X, set.mem_univ _, polynomial.eval₂_X _ _⟩)
+  (λ y ⟨p, _, (hp : polynomial.aeval x p = y)⟩, hp ▸ polynomial.induction_on p
+    (λ r, by { rw [polynomial.aeval_def, polynomial.eval₂_C],
+               exact (adjoin R _).algebra_map_mem r })
     (λ p q hp hq, by rw alg_hom.map_add; exact is_add_submonoid.add_mem hp hq)
     (λ n r ih, by { rw [pow_succ', ← mul_assoc, alg_hom.map_mul,
       polynomial.aeval_def _ polynomial.X, polynomial.eval₂_X],
@@ -128,7 +130,7 @@ variables [algebra R A] {s t : set A}
 variables {R s t}
 open ring
 
-theorem adjoin_int (s : set R) : adjoin ℤ s = subalgebra_of_subring (closure s) :=
+theorem adjoin_int (s : set R) : adjoin ℤ s = subalgebra_of_is_subring (closure s) :=
 le_antisymm (adjoin_le subset_closure) (closure_subset subset_adjoin)
 
 theorem mem_adjoin_iff {s : set A} {x : A} :
@@ -231,5 +233,5 @@ convert alg_hom.is_noetherian_ring_range _; apply_instance
 
 theorem is_noetherian_ring_closure (s : set R) (hs : s.finite) :
   is_noetherian_ring (ring.closure s) :=
-show is_noetherian_ring (subalgebra_of_subring (ring.closure s)), from
+show is_noetherian_ring (subalgebra_of_is_subring (ring.closure s)), from
 algebra.adjoin_int s ▸ is_noetherian_ring_of_fg (subalgebra.fg_def.2 ⟨s, hs, rfl⟩)

src/ring_theory/adjoin_root.lean

@@ -92,7 +92,7 @@ polynomial.induction_on p (λ x, by { rw aeval_C, refl })
 
 theorem adjoin_root_eq_top : algebra.adjoin R ({root f} : set (adjoin_root f)) = ⊤ :=
 algebra.eq_top_iff.2 $ λ x, induction_on f x $ λ p,
-(algebra.adjoin_singleton_eq_range R (root f)).symm ▸ ⟨p, aeval_eq p⟩
+(algebra.adjoin_singleton_eq_range R (root f)).symm ▸ ⟨p, set.mem_univ _, aeval_eq p⟩
 
 @[simp] lemma eval₂_root (f : polynomial R) : f.eval₂ (of f) (root f) = 0 :=
 by rw [← algebra_map_eq, ← aeval_def, aeval_eq, mk_self]

src/ring_theory/algebra.lean

@@ -5,7 +5,7 @@ Authors: Kenny Lau, Yury Kudryashov
 -/
 import data.matrix.basic
 import linear_algebra.tensor_product
-import ring_theory.subsemiring
+import ring_theory.subring
 import deprecated.subring
 
 /-!
@@ -187,19 +187,33 @@ instance of_subsemiring (S : subsemiring R) : algebra S A :=
 
 /-- Algebra over a subring. -/
 instance of_subring {R A : Type*} [comm_ring R] [ring A] [algebra R A]
-  (S : set R) [is_subring S] : algebra S A :=
+  (S : subring R) : algebra S A :=
 { smul := λ s x, (s : R) • x,
   commutes' := λ r x, algebra.commutes r x,
   smul_def' := λ r x, algebra.smul_def r x,
-  .. (algebra_map R A).comp (⟨coe, rfl, λ _ _, rfl, rfl, λ _ _, rfl⟩ : S →+* R) }
+  .. (algebra_map R A).comp (subring.subtype S) }
+
+lemma algebra_map_of_subring {R : Type*} [comm_ring R] (S : subring R) :
+  (algebra_map S R : S →+* R) = subring.subtype S := rfl
+
+lemma coe_algebra_map_of_subring {R : Type*} [comm_ring R] (S : subring R) :
+  (algebra_map S R : S → R) = subtype.val := rfl
+
+lemma algebra_map_of_subring_apply {R : Type*} [comm_ring R] (S : subring R) (x : S) :
+  algebra_map S R x = x := rfl
 
-lemma subring_coe_algebra_map_hom {R : Type*} [comm_ring R] (S : set R) [is_subring S] :
+/-- Algebra over a set that is closed under the ring operations. -/
+instance of_is_subring {R A : Type*} [comm_ring R] [ring A] [algebra R A]
+  (S : set R) [is_subring S] : algebra S A :=
+algebra.of_subring S.to_subring
+
+lemma is_subring_coe_algebra_map_hom {R : Type*} [comm_ring R] (S : set R) [is_subring S] :
   (algebra_map S R : S →+* R) = is_subring.subtype S := rfl
 
-lemma subring_coe_algebra_map {R : Type*} [comm_ring R] (S : set R) [is_subring S] :
+lemma is_subring_coe_algebra_map {R : Type*} [comm_ring R] (S : set R) [is_subring S] :
   (algebra_map S R : S → R) = subtype.val := rfl
 
-lemma subring_algebra_map_apply {R : Type*} [comm_ring R] (S : set R) [is_subring S] (x : S) :
+lemma is_subring_algebra_map_apply {R : Type*} [comm_ring R] (S : set R) [is_subring S] (x : S) :
   algebra_map S R x = x := rfl
 
 lemma set_range_subset {R : Type*} [comm_ring R] {T₁ T₂ : set R} [is_subring T₁] (hyp : T₁ ⊆ T₂) :
@@ -471,6 +485,19 @@ variables [algebra R A] [algebra R B] [algebra R C] (φ : A →ₐ[R] B)
 
 end ring
 
+section division_ring
+
+variables [comm_ring R] [division_ring A] [division_ring B]
+variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
+
+@[simp] lemma map_inv (x) : φ (x⁻¹) = (φ x)⁻¹ :=
+φ.to_ring_hom.map_inv x
+
+@[simp] lemma map_div (x y) : φ (x / y) = φ x / φ y :=
+φ.to_ring_hom.map_div x y
+
+end division_ring
+
 theorem injective_iff {R A B : Type*} [comm_semiring R] [ring A] [semiring B]
   [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
   function.injective f ↔ (∀ x, f x = 0 → x = 0) :=
@@ -744,20 +771,22 @@ instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=
 
 end rat
 
-/-- A subalgebra is a subring that includes the range of `algebra_map`. -/
+/-- A subalgebra is a sub(semi)ring that includes the range of `algebra_map`. -/
 structure subalgebra (R : Type u) (A : Type v)
-  [comm_semiring R] [semiring A] [algebra R A] : Type v :=
-(carrier : subsemiring A)
+  [comm_semiring R] [semiring A] [algebra R A] extends subsemiring A : Type v :=
 (algebra_map_mem' : ∀ r, algebra_map R A r ∈ carrier)
 
+/-- Reinterpret a `subalgebra` as a `subsemiring`. -/
+add_decl_doc subalgebra.to_subsemiring
+
 namespace subalgebra
 
 variables {R : Type u} {A : Type v} {B : Type w}
 variables [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B]
 include R
 
 instance : has_coe (subalgebra R A) (subsemiring A) :=
-⟨λ S, S.carrier⟩
+⟨λ S, { ..S }⟩
 
 instance : has_mem A (subalgebra R A) :=
 ⟨λ x S, x ∈ (S : set A)⟩
@@ -859,6 +888,12 @@ instance {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A]
 { one_mem := S.one_mem,
   mul_mem := λ _ _, S.mul_mem }
 
+/-- A subalgebra over a ring is also a `subring`. -/
+def to_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
+  subring A :=
+{ neg_mem' := λ _, S.neg_mem,
+  .. S.to_subsemiring }
+
 instance {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
   is_subring (S : set A) :=
 { neg_mem := λ _, S.neg_mem }
@@ -928,27 +963,27 @@ instance : partial_order (subalgebra R A) :=
 def comap {R : Type u} {S : Type v} {A : Type w}
   [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A]
   (iSB : subalgebra S A) : subalgebra R (algebra.comap R S A) :=
-{ carrier := (iSB : subsemiring A),
-  algebra_map_mem' := λ r, iSB.algebra_map_mem (algebra_map R S r) }
+{ algebra_map_mem' := λ r, iSB.algebra_map_mem (algebra_map R S r),
+  .. iSB }
 
 /-- If `S` is an `R`-subalgebra of `A` and `T` is an `S`-subalgebra of `A`,
 then `T` is an `R`-subalgebra of `A`. -/
 def under {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
   {i : algebra R A} (S : subalgebra R A)
   (T : subalgebra S A) : subalgebra R A :=
-{ carrier := T,
-  algebra_map_mem' := λ r, T.algebra_map_mem ⟨algebra_map R A r, S.algebra_map_mem r⟩ }
+{ algebra_map_mem' := λ r, T.algebra_map_mem ⟨algebra_map R A r, S.algebra_map_mem r⟩,
+  .. T }
 
 /-- Transport a subalgebra via an algebra homomorphism. -/
 def map (S : subalgebra R A) (f : A →ₐ[R] B) : subalgebra R B :=
-{ carrier := subsemiring.map (f : A →+* B) S,
-  algebra_map_mem' := λ r, f.commutes r ▸ set.mem_image_of_mem _ (S.algebra_map_mem r) }
+{ algebra_map_mem' := λ r, f.commutes r ▸ set.mem_image_of_mem _ (S.algebra_map_mem r),
+  .. subsemiring.map (f : A →+* B) S,}
 
 /-- Preimage of a subalgebra under an algebra homomorphism. -/
 def comap' (S : subalgebra R B) (f : A →ₐ[R] B) : subalgebra R A :=
-{ carrier := subsemiring.comap (f : A →+* B) S,
-  algebra_map_mem' := λ r, show f (algebra_map R A r) ∈ S,
-    from (f.commutes r).symm ▸ S.algebra_map_mem r }
+{ algebra_map_mem' := λ r, show f (algebra_map R A r) ∈ S,
+    from (f.commutes r).symm ▸ S.algebra_map_mem r,
+  .. subsemiring.comap (f : A →+* B) S,}
 
 theorem map_le {S : subalgebra R A} {f : A →ₐ[R] B} {U : subalgebra R B} :
   map S f ≤ U ↔ S ≤ comap' U f :=
@@ -972,13 +1007,14 @@ variables (φ : A →ₐ[R] B)
 
 /-- Range of an `alg_hom` as a subalgebra. -/
 protected def range (φ : A →ₐ[R] B) : subalgebra R B :=
-{ carrier :=
-  { carrier := set.range φ,
-    one_mem' := ⟨1, φ.map_one⟩,
-    mul_mem' := λ _ _ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x * y, by rw [φ.map_mul, hx, hy]⟩,
-    zero_mem' := ⟨0, φ.map_zero⟩,
-    add_mem' := λ _ _ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x + y, by rw [φ.map_add, hx, hy]⟩ },
-  algebra_map_mem' := λ r, ⟨algebra_map R A r, φ.commutes r⟩ }
+{ algebra_map_mem' := λ r, ⟨algebra_map R A r, set.mem_univ _, φ.commutes r⟩,
+  .. φ.to_ring_hom.srange }
+
+@[simp] lemma mem_range (φ : A →ₐ[R] B) {y : B} :
+  y ∈ φ.range ↔ ∃ x, φ x = y := ring_hom.mem_srange
+
+@[simp] lemma coe_range (φ : A →ₐ[R] B) : (φ.range : set B) = set.range φ :=
+by { ext, rw [subalgebra.mem_coe, mem_range], refl }
 
 /-- Restrict the codomain of an algebra homomorphism. -/
 def cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) : A →ₐ[R] S :=
@@ -1013,8 +1049,8 @@ variables [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B
 
 /-- The minimal subalgebra that includes `s`. -/
 def adjoin (s : set A) : subalgebra R A :=
-{ carrier := subsemiring.closure (set.range (algebra_map R A) ∪ s),
-  algebra_map_mem' := λ r, subsemiring.subset_closure $ or.inl ⟨r, rfl⟩ }
+{ algebra_map_mem' := λ r, subsemiring.subset_closure $ or.inl ⟨r, rfl⟩,
+  .. subsemiring.closure (set.range (algebra_map R A) ∪ s) }
 variables {R}
 
 protected lemma gc : galois_connection (adjoin R : set A → subalgebra R A) coe :=
@@ -1034,8 +1070,9 @@ galois_insertion.lift_complete_lattice algebra.gi
 instance : inhabited (subalgebra R A) := ⟨⊥⟩
 
 theorem mem_bot {x : A} : x ∈ (⊥ : subalgebra R A) ↔ x ∈ set.range (algebra_map R A) :=
-suffices (⊥ : subalgebra R A) = (of_id R A).range, by rw this; refl,
-le_antisymm bot_le $ subalgebra.range_le _
+suffices (of_id R A).range = (⊥ : subalgebra R A),
+by { rw [← this, ← subalgebra.mem_coe, alg_hom.coe_range], refl },
+le_bot_iff.mp (λ x hx, subalgebra.range_le _ ((of_id R A).coe_range ▸ hx))
 
 theorem mem_top {x : A} : x ∈ (⊤ : subalgebra R A) :=
 subsemiring.subset_closure $ or.inr trivial
@@ -1048,7 +1085,8 @@ theorem eq_top_iff {S : subalgebra R A} :
 ⟨λ h x, by rw h; exact mem_top, λ h, by ext x; exact ⟨λ _, mem_top, λ _, h x⟩⟩
 
 @[simp] theorem map_top (f : A →ₐ[R] B) : subalgebra.map (⊤ : subalgebra R A) f = f.range :=
-subalgebra.ext $ λ x, ⟨λ ⟨y, _, hy⟩, ⟨y, hy⟩, λ ⟨y, hy⟩, ⟨y, algebra.mem_top, hy⟩⟩
+subalgebra.ext $ λ x,
+  ⟨λ ⟨y, _, hy⟩, ⟨y, set.mem_univ _, hy⟩, λ ⟨y, mem, hy⟩, ⟨y, algebra.mem_top, hy⟩⟩
 
 @[simp] theorem map_bot (f : A →ₐ[R] B) : subalgebra.map (⊥ : subalgebra R A) f = ⊥ :=
 eq_bot_iff.2 $ λ x ⟨y, hy, hfy⟩, let ⟨r, hr⟩ := mem_bot.1 hy in subalgebra.range_le _
@@ -1105,8 +1143,8 @@ instance algebra_nat : algebra ℕ R :=
 variables {R}
 /-- A subsemiring is a `ℕ`-subalgebra. -/
 def subalgebra_of_subsemiring (S : subsemiring R) : subalgebra ℕ R :=
-{ carrier := S,
-  algebra_map_mem' := λ i, S.coe_nat_mem i }
+{ algebra_map_mem' := λ i, S.coe_nat_mem i,
+  .. S }
 
 @[simp] lemma mem_subalgebra_of_subsemiring {x : R} {S : subsemiring R} :
   x ∈ subalgebra_of_subsemiring S ↔ x ∈ S :=
@@ -1153,19 +1191,18 @@ def ring_hom.to_int_alg_hom {R S : Type*} [ring R] [ring S] (f : R →+* S) : R
   .. f }
 
 variables {R}
+
 /-- A subring is a `ℤ`-subalgebra. -/
-def subalgebra_of_subring (S : set R) [is_subring S] : subalgebra ℤ R :=
-{ carrier :=
-  { carrier := S,
-    one_mem' := is_submonoid.one_mem,
-    mul_mem' := λ _ _, is_submonoid.mul_mem,
-    zero_mem' := is_add_submonoid.zero_mem,
-    add_mem' := λ _ _, is_add_submonoid.add_mem, },
-  algebra_map_mem' := λ i, int.induction_on i (show (0 : R) ∈ S, from is_add_submonoid.zero_mem)
-    (λ i ih, show (i + 1 : R) ∈ S, from is_add_submonoid.add_mem ih is_submonoid.one_mem)
-    (λ i ih, show ((-i - 1 : ℤ) : R) ∈ S, by { rw [int.cast_sub, int.cast_one],
-      exact is_add_subgroup.sub_mem S _ _ ih is_submonoid.one_mem }) }
+def subalgebra_of_subring (S : subring R) : subalgebra ℤ R :=
+{ algebra_map_mem' := λ i, int.induction_on i S.zero_mem
+  (λ i ih, S.add_mem ih S.one_mem)
+  (λ i ih, show ((-i - 1 : ℤ) : R) ∈ S, by { rw [int.cast_sub, int.cast_one],
+    exact S.sub_mem ih S.one_mem }),
+  .. S }
 
+/-- A subset closed under the ring operations is a `ℤ`-subalgebra. -/
+def subalgebra_of_is_subring (S : set R) [is_subring S] : subalgebra ℤ R :=
+subalgebra_of_subring S.to_subring
 
 section
 variables {S : Type*} [ring S]
@@ -1181,10 +1218,14 @@ instance nat_algebra_subsingleton : subsingleton (algebra ℕ S) :=
 ⟨λ P Q, by { ext, simp, }⟩
 end
 
-@[simp] lemma mem_subalgebra_of_subring {x : R} {S : set R} [is_subring S] :
+@[simp] lemma mem_subalgebra_of_subring {x : R} {S : subring R} :
   x ∈ subalgebra_of_subring S ↔ x ∈ S :=
 iff.rfl
 
+@[simp] lemma mem_subalgebra_of_is_subring {x : R} {S : set R} [is_subring S] :
+  x ∈ subalgebra_of_is_subring S ↔ x ∈ S :=
+iff.rfl
+
 section span_int
 open submodule
 

src/ring_theory/algebra_tower.lean

@@ -189,8 +189,8 @@ variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
 /-- If A/S/R is a tower of algebras then the `res`triction of a S-subalgebra of A is an R-subalgebra of A. -/
 def res (U : subalgebra S A) : subalgebra R A :=
-{ carrier := U,
-  algebra_map_mem' := λ x, by { rw algebra_map_apply R S A, exact U.algebra_map_mem _ } }
+{ algebra_map_mem' := λ x, by { rw algebra_map_apply R S A, exact U.algebra_map_mem _ },
+  .. U}
 
 @[simp] lemma res_top : res R (⊤ : subalgebra S A) = ⊤ :=
 algebra.eq_top_iff.2 $ λ _, show _ ∈ (⊤ : subalgebra S A), from algebra.mem_top
@@ -223,7 +223,7 @@ show z ∈ subsemiring.closure (set.range (algebra_map (to_alg_hom R S A).range
   z ∈ subsemiring.closure (set.range (algebra_map S A) ∪ t : set A),
 from suffices set.range (algebra_map (to_alg_hom R S A).range A) = set.range (algebra_map S A),
   by rw this,
-by { ext z, exact ⟨λ ⟨⟨x, y, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩, ⟨⟨z, y, hy⟩, rfl⟩⟩ }
+by { ext z, exact ⟨λ ⟨⟨x, y, _, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩, ⟨⟨z, y, set.mem_univ _, hy⟩, rfl⟩⟩ }
 
 end is_scalar_tower