chore(ring_theory/algebraic): speedup slow proof (#3336)

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Author: jcommelin

src/ring_theory/algebra.lean

@@ -723,9 +723,15 @@ instance to_algebra {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A
   [algebra R A] (S : subalgebra R A) : algebra S A :=
 algebra.of_subsemiring _
 
+-- todo: standardize on the names these morphisms
+-- compare with submodule.subtype
+
 /-- Embedding of a subalgebra into the algebra. -/
 def val : S →ₐ[R] A :=
-by refine_struct { to_fun := subtype.val }; intros; refl
+by refine_struct { to_fun := (coe : S → A) }; intros; refl
+
+@[simp]
+lemma val_apply (x : S) : S.val x = (x : A) := rfl
 
 /-- Convert a `subalgebra` to `submodule` -/
 def to_submodule : submodule R A :=

src/ring_theory/algebraic.lean

@@ -42,7 +42,7 @@ variables {R A}
 
 /-- A subalgebra is algebraic if and only if it is algebraic an algebra. -/
 lemma subalgebra.is_algebraic_iff (S : subalgebra R A) :
-  S.is_algebraic ↔ @algebra.is_algebraic R S _ _ (by convert S.algebra) :=
+  S.is_algebraic ↔ @algebra.is_algebraic R S _ _ (S.algebra) :=
 begin
   delta algebra.is_algebraic subalgebra.is_algebraic,
   rw [subtype.forall'],
@@ -51,12 +51,7 @@ begin
   apply and_congr iff.rfl,
   have h : function.injective (S.val) := subtype.val_injective,
   conv_rhs { rw [← h.eq_iff, alg_hom.map_zero], },
-  apply eq_iff_eq_cancel_right.mpr,
-  symmetry,
-  -- TODO: add an `aeval`-specific version of `hom_eval₂`
-  simp only [aeval_def],
-  convert hom_eval₂ p (algebra_map R S) ↑S.val ⟨x, hx⟩,
-  refl
+  rw [← aeval_alg_hom_apply, S.val_apply, subtype.val_eq_coe],
 end
 
 /-- An algebra is algebraic if and only if it is algebraic as a subalgebra. -/