From f0cb135b57f5445de74ac7a91ff938d8b4badfe9 Mon Sep 17 00:00:00 2001
From: Aditya Menon <63695868+menon-codes@users.noreply.github.com>
Date: Thu, 30 Jul 2026 03:12:19 +0530
Subject: [PATCH] refactor: making trans usage explicit with kerLift

---
 Mathlib/RingTheory/NoetherNormalization.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Mathlib/RingTheory/NoetherNormalization.lean b/Mathlib/RingTheory/NoetherNormalization.lean
index c30969e30f41e9..8ab91c489361ac 100644
--- a/Mathlib/RingTheory/NoetherNormalization.lean
+++ b/Mathlib/RingTheory/NoetherNormalization.lean
@@ -258,11 +258,9 @@ theorem exists_integral_inj_algHom_of_quotient (I : Ideal (MvPolynomial (Fin n)
       set ϕ := kerLiftAlg <| hom2 f I
       have := Quotient.nontrivial_iff.mpr hi
       obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)
-      have comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k <| ker <| hom2 f I) = (hom2 f I) :=
-        AlgHom.ext fun a ↦ by
-          simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk]
-      exact ⟨s, by lia, ϕ.comp g, (ϕ.coe_comp  g) ▸ (kerLiftAlg_injective _).comp injg,
-        intg.trans _ _ <| (comp ▸ hom2_isIntegral f I fne fi).tower_top _ _⟩
+      have intgϕ := (hom2_isIntegral f I fne fi).kerLift
+      exact ⟨s, by lia, ϕ.comp g, (ϕ.coe_comp g) ▸ (kerLiftAlg_injective _).comp injg,
+        intg.trans g.toRingHom ϕ.toRingHom intgϕ⟩
 
 variable (k R : Type*) [Field k] [CommRing R] [Nontrivial R] [a : Algebra k R]
   [fin : Algebra.FiniteType k R]