golf away simp lemma

Author: ROTARTSI82

Mathlib/RingTheory/IsAdjoinRoot.lean

@@ -653,46 +653,36 @@ theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyCl
             (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
       rw [mul_one]
 
-section mkOfAdjoinEqTop'
-
-variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
-
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
 def mkOfAdjoinEqTop'
+    [Module.Finite R S] [Module.Free R S] [Nontrivial R]
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
-    IsAdjoinRootMonic S (minpoly R α) := by
-  set f := minpoly R α
-  have hf : f.Monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
-  letI : Module R (AdjoinRoot f) := Algebra.toModule
-  haveI := hf.free_adjoinRoot; haveI finite := hf.finite_adjoinRoot
-  let φ : AdjoinRoot f →ₐ[R] S :=
-    AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
-  have hφ_surj : Function.Surjective φ := by
-    rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
-    exact fun s =>
-      let ⟨p, hp⟩ := hα s; ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-  have hrank : f.natDegree = Module.finrank R S := le_antisymm (minpoly.natDegree_le') (by
-    have e := φ.toLinearMap.quotKerEquivRange.trans
-      (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ_surj))
-    rw [← e.finrank_eq]
-    exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le)
-  have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
-    ((finrank_quotient_span_eq_natDegree' hf).trans hrank)
-  have hφ_inj : Function.Injective φ :=
-    fun x y h => OrzechProperty.injective_of_surjective_endomorphism
-    (e.symm.toLinearMap.comp φ.toLinearMap) (e.symm.surjective.comp hφ_surj) (congr_arg e.symm h)
-  exact
-    { IsAdjoinRoot.ofAdjoinRootEquiv
-        (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
-
-@[simp]
-lemma mkOfAdjoinEqTop'_map
-    {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
-    (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = (aeval α) := by
-  unfold IsAdjoinRootMonic.mkOfAdjoinEqTop'
-  ext; simp
-
-end mkOfAdjoinEqTop'
+    IsAdjoinRootMonic S (minpoly R α) where
+  map := aeval α
+  ker_map := by
+    set f := minpoly R α
+    have hf := minpoly.monic (Algebra.IsIntegral.isIntegral (R := R) α)
+    let φ : AdjoinRoot f →ₐ[R] S :=
+      AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
+    have hφ : Function.Surjective φ := by
+      rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
+      intro s; obtain ⟨p, hp⟩ := hα s
+      exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
+    refine IsAdjoinRoot.ofAdjoinRootEquiv (AlgEquiv.ofBijective φ ⟨?_, hφ⟩) |>.ker_map
+    haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+    letI : Module R (AdjoinRoot f) := Algebra.toModule
+    have e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S
+      ((finrank_quotient_span_eq_natDegree' hf).trans <|
+        le_antisymm minpoly.natDegree_le' ?_)
+    · exact fun x y h => OrzechProperty.injective_of_surjective_endomorphism
+        (e.symm.toLinearMap.comp φ.toLinearMap)
+        (e.symm.surjective.comp hφ) (congr_arg e.symm h)
+    · rw [← φ.toLinearMap.quotKerEquivRange.trans
+        (LinearEquiv.ofTop _ (LinearMap.range_eq_top.mpr hφ)) |>.finrank_eq]
+      exact (Submodule.finrank_quotient_le _).trans (finrank_quotient_span_eq_natDegree' hf).le
+  map_surjective := by
+    rwa [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+  monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
 
 end IsAdjoinRootMonic