From 316d7d6c006ec5e711fa4ce9580814adae53611c Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Fri, 26 Jun 2026 18:38:06 +0200
Subject: [PATCH 1/9] feat(RingTheory): etale lifting property of henselian
 local rings

---
 Mathlib/Algebra/Algebra/Equiv.lean        |   8 +-
 Mathlib/LinearAlgebra/Dimension/Free.lean |  11 +
 Mathlib/RingTheory/Henselian.lean         | 390 +++++++++++++++++++++-
 Mathlib/RingTheory/Idempotents.lean       |  35 ++
 4 files changed, 426 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean
index 9f592f5c7127d0..b64a4415704722 100644
--- a/Mathlib/Algebra/Algebra/Equiv.lean
+++ b/Mathlib/Algebra/Algebra/Equiv.lean
@@ -768,10 +768,10 @@ def algHomUnitsEquiv (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] :
 instance _root_.Finite.algEquiv [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂) :=
   Finite.of_injective _ AlgEquiv.coe_toAlgHom_injective
 
--- TODO Morally this is just `isLocalHom_equiv`: can we obviate the need for this instance?
-instance : IsLocalHom e.toAlgHom := by
-  have : IsLocalHom e.toRingEquiv := inferInstance
-  exact ⟨this.map_nonunit⟩
+-- TODO Morally these are just `isLocalHom_equiv`: can we obviate the need for this instance?
+instance : IsLocalHom e.toAlgHom := ⟨by simp⟩
+instance : IsLocalHom e.toRingEquiv.toRingHom := ⟨by simp⟩
+instance : IsLocalHom e.toAlgHom.toRingHom := ⟨by simp⟩
 
 end Semiring
 
diff --git a/Mathlib/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean
index 865262acab6c98..b4158658b90a7a 100644
--- a/Mathlib/LinearAlgebra/Dimension/Free.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Free.lean
@@ -360,6 +360,17 @@ noncomputable def _root_.LinearEquiv.smul_id_of_finrank_eq_one (d1 : Module.finr
     simp [← (LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one d1 _).choose_spec.2 c]
   right_inv u := ((u.existsUnique_eq_smul_id_of_finrank_eq_one d1).choose_spec.1).symm
 
+lemma finrank_eq_one_iff_algebraMap_bijective
+    {R S : Type*} [CommSemiring R] [CommSemiring S] [StrongRankCondition R] [Algebra R S]
+    [Module.Free R S] [Nontrivial R] :
+    Module.finrank R S = 1 ↔ Function.Bijective (algebraMap R S) := by
+  constructor
+  · intro H
+    let := (Module.basisUnique Unit H).repr ≪≫ₗ Finsupp.uniqueLinearEquiv _ _ .unit
+    exact (LinearEquiv.algEquivOfRing this.symm).bijective
+  · intro H
+    rw [← (AlgEquiv.ofBijective (Algebra.ofId R S) H).toLinearEquiv.finrank_eq, finrank_self]
+
 end Module
 
 end StrongRankCondition
diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
index 574b704be8d90f..8d0c5e48403449 100644
--- a/Mathlib/RingTheory/Henselian.lean
+++ b/Mathlib/RingTheory/Henselian.lean
@@ -1,13 +1,15 @@
 /-
 Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin
+Authors: Johan Commelin, Andrew Yang
 -/
 module
 
 public import Mathlib.Algebra.Polynomial.Taylor
 public import Mathlib.RingTheory.LocalRing.ResidueField.Basic
 public import Mathlib.RingTheory.AdicCompletion.Basic
+public import Mathlib.RingTheory.Etale.QuasiFinite
+public import Mathlib.RingTheory.Unramified.LocalStructure
 
 /-!
 # Henselian rings
@@ -36,22 +38,17 @@ In this case the first condition is automatic, and in the second condition we ma
 * `Henselian.TFAE`: equivalent ways of expressing the Henselian property for local rings
 * `IsAdicComplete.henselianRing`:
   a ring `R` with ideal `I` that is `I`-adically complete is Henselian at `I`
+* `HenselianLocalRing.ofId_comp_bijective`: The étale lifting property for henselian local rings:
+  If `R` is an henselian local ring with residue field `k`, then for any étale `R`-algebra `A`,
+  every `A →ₐ[R] k` lifts uniquely to an `A →ₐ[R] R`.
+* `HenselianLocalRing.of_finite`: Finite local extensions of henselian local rings are henselian.
+* `HenselianLocalRing.algEquivEquiv`: If `A` is finite local étale over a henselian local ring `R`,
+  then `Aut(A/R) ≃ Gal(k(A)/k(R))`.
 
 ## References
 
 https://stacks.math.columbia.edu/tag/04GE
 
-## TODO
-
-After a good API for étale ring homomorphisms has been developed,
-we can give more equivalent characterization of Henselian rings.
-
-In particular, this can give a proof that factorizations into coprime polynomials can be lifted
-from the residue field to the Henselian ring.
-
-The following gist contains some code sketches in that direction.
-https://gist.github.com/jcommelin/47d94e4af092641017a97f7f02bf9598
-
 -/
 
 public section
@@ -61,9 +58,12 @@ noncomputable section
 
 universe u v
 
-open Polynomial IsLocalRing Function List
+open Polynomial IsLocalRing List
 open scoped Ring
 
+local notation "𝓀[" R "]" => ResidueField R
+local notation "𝓂[" R "]" => maximalIdeal R
+
 theorem isLocalHom_of_le_jacobson_bot {R : Type*} [CommRing R] (I : Ideal R)
     (h : I ≤ Ideal.jacobson ⊥) : IsLocalHom (Ideal.Quotient.mk I) := by
   constructor
@@ -122,7 +122,7 @@ theorem HenselianLocalRing.TFAE (R : Type u) [CommRing R] [IsLocalRing R] :
         ∀ f : R[X], f.Monic → ∀ a₀ : ResidueField R, aeval a₀ f = 0 →
           aeval a₀ (derivative f) ≠ 0 → ∃ a : R, f.IsRoot a ∧ residue R a = a₀,
         ∀ {K : Type u} [Field K],
-          ∀ (φ : R →+* K), Surjective φ → ∀ f : R[X], f.Monic → ∀ a₀ : K,
+          ∀ (φ : R →+* K), Function.Surjective φ → ∀ f : R[X], f.Monic → ∀ a₀ : K,
             f.eval₂ φ a₀ = 0 → f.derivative.eval₂ φ a₀ ≠ 0 → ∃ a : R, f.IsRoot a ∧ φ a = a₀] := by
   tfae_have 3 → 2
   | H => H (residue R) Ideal.Quotient.mk_surjective
@@ -275,3 +275,365 @@ theorem IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub {R : Type*} [CommRing R
   replace this := (maximalIdeal R).add_mem this ((maximalIdeal R).mul_mem_left c h)
   ring_nf at this
   contradiction
+
+open Polynomial TensorProduct KaehlerDifferential
+
+open nonZeroDivisors
+
+variable {R A B : Type*} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
+
+attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
+/-- If `R` is an henselian local ring with residue field `k`, then for any étale `R`-algebra `A`,
+every `A →ₐ[R] k` lifts uniquely to an `A →ₐ[R] R`. -/
+@[stacks 04GG "(1) => (7)"]
+lemma HenselianLocalRing.ofId_comp_bijective [Algebra.Etale R A] [HenselianLocalRing R] :
+    Function.Bijective ((Algebra.ofId R 𝓀[R]).comp : (A →ₐ[R] R) → (A →ₐ[R] 𝓀[R])) := by
+  constructor
+  · intro f₁ f₂ H
+    wlog _ : Algebra.IsStandardEtale R A
+    · let P := RingHom.ker ((IsScalarTower.toAlgHom R R 𝓀[R]).comp f₁).toRingHom
+      have inst : P.IsPrime := RingHom.ker_isPrime _
+      obtain ⟨r, hrP, _⟩ := Algebra.IsEtaleAt.exists_isStandardEtale (R := R) P
+      have hf₁ : IsUnit (f₁ r) := by
+        rw [← residue_ne_zero_iff_isUnit]
+        exact hrP
+      have hf₂ : IsUnit (f₂ r) := by
+        rw [← residue_ne_zero_iff_isUnit]
+        refine congr($H r).symm.trans_ne hrP
+      have : IsLocalization.liftAlgHom (S := Localization.Away r) (f := f₁) (M := .powers r)
+            (by simp [Submonoid.mem_powers_iff, hf₁.pow _]) =
+          IsLocalization.liftAlgHom (f := f₂) (M := .powers r)
+            (by simp [Submonoid.mem_powers_iff, hf₂.pow _]) := by
+        refine this (IsLocalization.algHom_ext (.powers r) ?_) inferInstance
+        ext x
+        simpa [Algebra.algHom] using congr($H x)
+      ext x
+      simpa using congr($this (algebraMap _ _ x))
+    obtain ⟨𝓟⟩ := Algebra.IsStandardEtale.nonempty_standardEtalePresentation (R := R) (S := A)
+    apply 𝓟.hom_ext
+    apply IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub (f := 𝓟.f)
+    · rw [← coe_aeval_eq_eval, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]
+    · rw [← coe_aeval_eq_eval, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]
+    · rw [← mem_nonunits_iff, ← mem_maximalIdeal, ← residue_eq_zero_iff, map_sub, sub_eq_zero]
+      exact congr($H _)
+    · rw [← coe_aeval_eq_eval, aeval_algHom_apply]
+      simpa using 𝓟.hasMap.isUnit_derivative_f.map f₁
+  · intro f
+    let P := RingHom.ker f.toRingHom
+    have : P.IsPrime := RingHom.ker_isPrime _
+    obtain ⟨r, hrP, ⟨⟨𝓟⟩⟩⟩ := Algebra.IsEtaleAt.exists_isStandardEtale (R := R) P
+    let φ : Localization.Away r →ₐ[R] 𝓀[R] :=
+      IsLocalization.liftAlgHom (M := .powers r) (f := f) <| Subtype.forall.mpr <|
+        show Submonoid.powers r ≤ (IsUnit.submonoid _).comap _ from Submonoid.powers_le.mpr
+        (by simpa [IsUnit.mem_submonoid_iff])
+    obtain ⟨x, hx⟩ := residue_surjective (φ 𝓟.x)
+    obtain ⟨y, hy, hxy⟩ := HenselianLocalRing.is_henselian 𝓟.f 𝓟.monic_f x (by
+      rw [← residue_eq_zero_iff, ← ResidueField.algebraMap_eq, eval, hom_eval₂, RingHom.comp_id,
+        ← aeval_def, ResidueField.algebraMap_eq, hx, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]) (by
+      rw [← residue_ne_zero_iff_isUnit, ← ResidueField.algebraMap_eq, eval, hom_eval₂,
+        RingHom.comp_id, ← aeval_def, ResidueField.algebraMap_eq, hx, aeval_algHom_apply]
+      exact (𝓟.hasMap.isUnit_derivative_f.map φ).ne_zero)
+    rw [← residue_eq_zero_iff, map_sub, sub_eq_zero] at hxy
+    have Hy : 𝓟.HasMap y := by
+      refine ⟨hy, ?_⟩
+      rw [← residue_ne_zero_iff_isUnit, ← ResidueField.algebraMap_eq, ← aeval_algebraMap_apply,
+        ResidueField.algebraMap_eq, hxy, hx, aeval_algHom_apply]
+      exact (𝓟.hasMap.2.map φ).ne_zero
+    refine ⟨((𝓟.lift _ Hy).comp 𝓟.equivRing.toAlgHom).comp (IsScalarTower.toAlgHom _ _ _), ?_⟩
+    trans ((φ.comp 𝓟.equivRing.symm.toAlgHom).comp 𝓟.equivRing.toAlgHom).comp
+        (IsScalarTower.toAlgHom _ _ _)
+    · simp_rw [← AlgHom.comp_assoc]
+      congr 2
+      ext
+      simp [hxy, hx]
+    · ext; simp [φ]
+
+attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
+set_option backward.isDefEq.respectTransparency false in
+/-- A finite algebra over an henselian local ring is a product of (henselian) local rings.
+
+TODO: show that the local rings are exactly `Aₘ` with `m` maximal ideals of `A`. -/
+@[stacks 04GG "(1) => (10)"]
+lemma HenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRing
+    [HenselianLocalRing R] [Module.Finite R A] :
+    ∃ (n : ℕ) (e : Fin n → A) (he : CompleteOrthogonalIdempotents e),
+      ∀ i, IsLocalRing (he.idem i).Corner := by
+  obtain ⟨R', _, _, _, P, _, _, n, e, he, P', _, _, hP, hP', H⟩ :=
+    Algebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq (R := R) (S := A) 𝓂[R]
+  let φ : 𝓀[R] ≃ₐ[R] 𝓂[R].ResidueField := .ofBijective
+    (IsScalarTower.toAlgHom R (R ⧸ 𝓂[R]) 𝓂[R].ResidueField)
+    (Ideal.bijective_algebraMap_quotient_residueField _)
+  let φ' := φ.trans (AlgEquiv.ofBijective _ hP)
+  obtain ⟨ψ, hψ⟩ := HenselianLocalRing.ofId_comp_bijective.surjective
+    (φ'.symm.toAlgHom.comp (IsScalarTower.toAlgHom R R' _))
+  have hPeq : P = 𝓂[R].comap ψ.toRingHom := by
+    trans RingHom.ker (IsScalarTower.toAlgHom R R' P.ResidueField).toRingHom
+    · exact P.ker_algebraMap_residueField.symm
+    · rw [← RingHom.ker_comp_of_injective _ (f := RingHomClass.toRingHom φ'.symm) φ'.symm.injective,
+        ← AlgEquiv.toAlgHom_toRingHom, AlgHom.toRingHom_eq_coe, ← AlgHom.comp_toRingHom, ← hψ,
+        AlgHom.comp_toRingHom, ← RingHom.comap_ker, ← 𝓂[R].mk_ker]; rfl
+  have hψ : Function.Surjective ψ.toRingHom := fun x ↦ ⟨algebraMap _ _ x, by simp⟩
+  have : P.IsMaximal := by rw [hPeq]; exact Ideal.comap_isMaximal_of_surjective _ hψ
+  let ψ' : R' ⊗[R] A →ₐ[R] A :=
+    Algebra.TensorProduct.lift ((Algebra.ofId _ _).comp ψ) (.id R A) fun _ _ ↦ .all _ _
+  have hψ' : Function.Surjective ψ'.toRingHom := fun x ↦ ⟨1 ⊗ₜ x, by simp [ψ']⟩
+  have h₁ : ψ' (e (.last _)) = 0 := by
+    suffices IsUnit (1 - ψ' (e (Fin.last n))) by
+      simpa using this.mul_left_cancel
+        (((he.idem (.last n)).map ψ').one_sub.eq.trans (mul_one _).symm)
+    by_contra he'
+    obtain ⟨M, hM, heM⟩ := Ideal.exists_le_maximal (Ideal.span {1 - ψ' (e (Fin.last n))}) (by simpa)
+    have := (H (M.comap ψ'.toRingHom) inferInstance ⟨by
+      rw [Ideal.under, Ideal.comap_comap]
+      trans M.comap ((algebraMap R A).comp ψ.toRingHom); swap
+      · congr 1; ext; simp [ψ']
+      · rw [hPeq, ← Ideal.comap_comap,
+          eq_maximalIdeal (Ideal.isMaximal_comap_of_isIntegral_of_isMaximal (R := R) M)]⟩).1
+    simp only [AlgHom.toRingHom_eq_coe, Ideal.mem_comap, RingHom.coe_coe, Ideal.span_le,
+      Set.singleton_subset_iff, SetLike.mem_coe] at this heM
+    exact Ideal.one_notMem M (by convert add_mem this heM; ring)
+  refine ⟨n, ψ' ∘ e ∘ Fin.castSucc, ⟨(he.map ψ'.toRingHom).1.embedding Fin.castSuccEmb, ?_⟩, ?_⟩
+  · simpa [Fin.sum_univ_castSucc, h₁] using (he.map ψ'.toRingHom).2
+  · intro i
+    have he₀ := (he.idem i.castSucc).map ψ'
+    let Q := (P' i).comap Algebra.TensorProduct.includeRight.toRingHom
+    have _ : (P' i).LiesOver 𝓂[R] := .trans _ P _
+    have _ : Q.LiesOver 𝓂[R] :=
+      inferInstanceAs (((P' i).comap Algebra.TensorProduct.includeRight).LiesOver _)
+    have _ : (P' i).LiesOver 𝓂[R] := .trans _ P _
+    have : Q.IsMaximal := Ideal.isMaximal_of_isIntegral_of_isMaximal_comap (R := R) _
+      (by rw [← Ideal.under, ← Q.over_def 𝓂[R]]; infer_instance)
+    have hψ' : Function.Surjective ψ'.toRingHom := fun x ↦ ⟨1 ⊗ₜ x, by simp [ψ']⟩
+    have hQP' : Q.comap ψ'.toRingHom = P' i := by
+      have : (Ideal.comap ψ'.toRingHom Q).LiesOver P := by
+        rw [hPeq]
+        simp only [Ideal.liesOver_iff, Ideal.under, Ideal.comap_comap, Q, (P' i).over_def 𝓂[R]]
+        congr 1
+        ext a; simp [ψ']
+      apply Ideal.eq_of_comap_eq_comap_of_bijective_residueFieldMap hP
+      simp only [Ideal.comap_comap, Q]
+      congr 1; ext; simp [ψ']
+    have hQP'' : (P' i).comap Algebra.TensorProduct.includeRight.toRingHom = Q := by
+      rw [← hQP', Ideal.comap_comap]; convert Ideal.comap_id _; ext; simp [ψ']
+    have heQ : RingHom.ker (algebraMap A he₀.Corner) ≤ Q := by
+      rw [he₀.ker_toCorner, Ideal.span_le]
+      simp only [Set.singleton_subset_iff, SetLike.mem_coe]
+      rw [← Ideal.IsPrime.mul_mem_left_iff (I := Q) fun h ↦ hP' i (hQP'.le h)]
+      simp [mul_sub, ← map_mul, (he.idem _).eq]
+    have := Ideal.IsMaximal.map_of_surjective_of_ker_le he₀.toCorner_surjective heQ
+    refine IsLocalRing.of_unique_max_ideal ⟨Q.map (algebraMap A he₀.Corner), ‹_›, fun Q' hQ' ↦ ?_⟩
+    have inst := Ideal.comap_isMaximal_of_surjective _ he₀.toCorner_surjective (K := Q')
+    refine (hQ'.eq_of_le this.ne_top ?_)
+    refine Ideal.le_map_of_comap_le_of_surjective _ he₀.toCorner_surjective ?_
+    suffices (Q'.comap (algebraMap A _)).comap ψ'.toRingHom = P' i by
+      rw [← hQP'', ← this, Ideal.comap_comap,]
+      simp only [AlgHom.toRingHom_eq_coe, ← AlgHom.comp_toRingHom, ψ', Function.comp_apply, le_refl,
+        Algebra.TensorProduct.lift_comp_includeRight', AlgHom.id_toRingHom, Ideal.comap_id]
+    refine (H _ inferInstance ⟨?_⟩).2 _ ?_
+    · rw [hPeq, ← eq_maximalIdeal (Ideal.isMaximal_comap_of_isIntegral_of_isMaximal (R := R)
+        (Q'.comap (algebraMap A he₀.Corner)))]
+      simp only [Ideal.under, Ideal.comap_comap, RingHom.comp_assoc]
+      congr 2; ext; simp [ψ']
+    · have : algebraMap _ he₀.Corner (ψ' (e i.castSucc)) = 1 := Subtype.ext ((he.idem _).map ψ')
+      simpa [this] using Ideal.one_notMem Q'
+
+attribute [local instance] RingHom.ker_isPrime in
+private theorem HenselianLocalRing.of_finite_aux [IsLocalRing A]
+    (f : A[X]) (a₀ : A) (ha₀ : eval a₀ f ∈ 𝓂[A])
+    (ha₀' : IsUnit (eval a₀ (derivative f))) (e : AdjoinRoot f)
+    (he : IsIdempotentElem e) [IsLocalRing he.Corner]
+    (ha₀'' : AdjoinRoot.liftAlgHom _ (Algebra.ofId _ 𝓀[A]) (algebraMap _ _ a₀)
+      (by simpa using ha₀) e ≠ 0) :
+    1 ⊗ₜ[A] (algebraMap (AdjoinRoot f) he.Corner) (AdjoinRoot.root f) = residue A a₀ ⊗ₜ[A] 1 := by
+  let φ : AdjoinRoot f →ₐ[A] 𝓀[A] := AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _)
+    (algebraMap _ _ a₀) (by simpa using ha₀)
+  have hφ : Function.Surjective φ := residue_surjective.forall.mpr fun x ↦ ⟨.of f x, by simp [φ]⟩
+  set root := (1 : 𝓀[A]) ⊗ₜ[A] algebraMap _ he.Corner (AdjoinRoot.root f)
+  obtain ⟨g, hg⟩ : X - C (residue A a₀) ∣ f.map (residue A) := by
+    simpa [dvd_iff_isRoot, eval_map] using ha₀
+  obtain ⟨g, rfl⟩ := Polynomial.map_surjective _ residue_surjective g
+  have hga₀ : IsUnit (eval a₀ g) := by
+    rw [← residue_ne_zero_iff_isUnit, ← ResidueField.algebraMap_eq,
+      eval, hom_eval₂, RingHom.comp_id, ← eval_map, ResidueField.algebraMap_eq] at ha₀' ⊢
+    rw [← derivative_map, hg] at ha₀'
+    simpa using ha₀'
+  let φ' : he.Corner →ₐ[A] 𝓀[A] := by
+    refine AlgHom.liftOfSurjective (IsScalarTower.toAlgHom _ _ _)
+      he.toCorner_surjective φ ?_
+    refine he.ker_toCorner.trans_le ((Ideal.span_singleton_le_iff_mem _).mpr ?_)
+    rw [← Ideal.IsPrime.mul_mem_left_iff (by exact ha₀''), mul_sub, mul_one, he.eq, sub_self]
+    exact zero_mem _
+  have hφ' (x : AdjoinRoot f) : φ' (algebraMap _ _ x) = φ x :=
+    AlgHom.liftOfSurjective_apply ..
+  have hφ'' : IsLocalHom φ'.toRingHom :=
+    .of_surjective _ (AlgHom.liftOfSurjective_surjective _ _ _ _ hφ)
+  have hrootf : aeval root f = 0 := by
+    refine (aeval_algHom_apply Algebra.TensorProduct.includeRight _ _).trans ?_
+    simp [aeval_algebraMap_apply]
+  have hrootg : IsUnit (aeval root g) := by
+    have := hφ''.1 (algebraMap _ _ (AdjoinRoot.mk f g)) (by simpa [hφ', φ])
+    convert this.map (Algebra.TensorProduct.includeRight : _ →ₐ[A] 𝓀[A] ⊗[A] he.Corner)
+    rw [← AdjoinRoot.aeval_eq, ← aeval_algebraMap_apply, ← aeval_algHom_apply]
+    rfl
+  rw [← sub_eq_zero, ← hrootg.mul_left_inj]
+  simpa [← ResidueField.algebraMap_eq, hrootf, -mul_eq_zero, -mul_eq_left₀, -mul_eq_right₀] using
+    congr(aeval root $hg).symm
+
+/-- A finite local ring over an henselian local ring is also henselian.
+
+This proof hides the fact that
+(every finite extension is a product of local rings) implies henselian.
+
+Consider splitting this fact out (if useful) once we have a nice way of stating the
+former condition (as `Function.Surjective (MaximalSpectrum.toPiLocalization R)`). -/
+lemma HenselianLocalRing.of_finite
+    [HenselianLocalRing R] [Module.Finite R A] [IsLocalRing A] : HenselianLocalRing A := by
+  refine ⟨fun f hf a₀ ha₀ ha₀' ↦ ?_⟩
+  have := hf.finite_adjoinRoot
+  have := hf.free_adjoinRoot
+  have : Module.Finite R (AdjoinRoot f) := .trans A _
+  obtain ⟨n, e, he, h⟩ := HenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRing
+    (R := R) (A := AdjoinRoot f)
+  let φ : AdjoinRoot f →ₐ[A] 𝓀[A] := AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _)
+    (algebraMap _ _ a₀) (by simpa using ha₀)
+  have hφ : Function.Surjective φ := residue_surjective.forall.mpr fun x ↦ ⟨.of f x, by simp [φ]⟩
+  have : (RingHom.ker φ.toRingHom).IsMaximal := RingHom.ker_isMaximal_of_surjective _ hφ
+  obtain ⟨i, hi⟩ : ∃ i, e i ∉ RingHom.ker φ := by
+    by_contra! H
+    exact Ideal.one_notMem (RingHom.ker φ.toRingHom) (he.complete ▸ sum_mem fun i _ ↦ H i)
+  have : Module.Finite A (he.idem i).Corner := .of_surjective
+    (IsScalarTower.toAlgHom _ (AdjoinRoot f) _).toLinearMap (he.idem i).toCorner_surjective
+  have : Module.Free A (he.idem i).Corner :=
+    have : Module.Projective A (he.idem i).Corner :=
+      .of_split ⟨⟨Subtype.val, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩
+        (IsScalarTower.toAlgHom _ (AdjoinRoot f) _).toLinearMap
+        (LinearMap.ext fun a ↦ Subtype.ext ((Subsemigroup.mem_corner_iff (he.idem i)).mp a.2).2)
+    have : Module.Flat A (he.idem i).Corner := Module.Flat.of_projective
+    Module.free_of_flat_of_isLocalRing
+  have hroot :
+      1 ⊗ₜ algebraMap _ (he.idem i).Corner (AdjoinRoot.root f) = residue A a₀ ⊗ₜ[A] 1 :=
+    HenselianLocalRing.of_finite_aux f a₀ ha₀ ha₀' _ (he.idem i) hi
+  have H : Function.Surjective (algebraMap 𝓀[A] (𝓀[A] ⊗[A] (he.idem i).Corner)) := by
+    intro x
+    obtain ⟨x, rfl⟩ := Algebra.TensorProduct.includeRight_surjective _
+      (by exact residue_surjective) x
+    obtain ⟨x, rfl⟩ := (he.idem i).toCorner_surjective x
+    obtain ⟨g, rfl⟩ := AdjoinRoot.mk_surjective x
+    have h₁ : residue _ (eval a₀ g) = φ (.mk f g) := by simp [φ]
+    have h₂ : (IsScalarTower.toAlgHom _ _ (𝓀[A] ⊗[A] (he.idem i).Corner)).comp φ =
+        Algebra.TensorProduct.includeRight.comp (IsScalarTower.toAlgHom _ _ _) := by
+      ext; simp [φ, ← hroot]
+    use algebraMap _ _ (aeval a₀ g)
+    trans algebraMap _ _ (eval a₀ g)
+    · simp
+    · simpa [φ] using congr($h₂ (.mk f g))
+  have : Module.finrank A (he.idem i).Corner = 1 := by
+    apply le_antisymm ?_ ((Module.finrank_pos_iff_of_free _ _).mpr inferInstance)
+    · rw [← Module.finrank_baseChange (R := 𝓀[A]), finrank_le_one_iff]
+      refine ⟨1, H.forall.mpr fun x ↦ ⟨x, by simp [Algebra.smul_def]⟩⟩
+  rw [Module.finrank_eq_one_iff_algebraMap_bijective] at this
+  obtain ⟨a, ha⟩ := this.2 (algebraMap _ _ (AdjoinRoot.root f))
+  refine ⟨a, this.1 ?_, ?_⟩
+  · rw [eval, hom_eval₂, RingHom.comp_id, ← aeval_def, ha, aeval_algebraMap_apply]
+    simp
+  · rw [← residue_eq_zero_iff, map_sub, sub_eq_zero]
+    apply (algebraMap 𝓀[A] (𝓀[A] ⊗[A] (he.idem i).Corner)).injective
+    trans Algebra.TensorProduct.includeRight (algebraMap _ _ a)
+    · simp
+    · rw [ha]; simp [← hroot]
+
+instance {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R]
+    [Algebra.IsIntegral R S] [Nontrivial S] : IsLocalHom (algebraMap R S) := by
+  have : (algebraMap R S).kerLift.IsIntegral :=
+    .tower_top (Ideal.Quotient.mk _) _
+      (by have := algebraMap_isIntegral_iff.mpr ‹Algebra.IsIntegral R S›; exact this)
+  have := this.isLocalHom (algebraMap R S).kerLift_injective
+  have : Nontrivial (R ⧸ RingHom.ker (algebraMap R S)) :=
+    Ideal.Quotient.nontrivial_iff.mpr (RingHom.ker_ne_top _)
+  have : IsLocalHom (Ideal.Quotient.mk (RingHom.ker (algebraMap R S))) :=
+    .of_surjective _ Ideal.Quotient.mk_surjective
+  exact RingHom.isLocalHom_comp (algebraMap R S).kerLift (Ideal.Quotient.mk _)
+
+/-- Let `R` be an henselian local ring, `A, B` be local `R`-algebras.
+Suppose `A` is etale and `B` is module-finite, then any `k(R)`-algebra map `k(A) → k(B)` lifts to
+an `R`-algebra map `A → B`.
+
+See `HenselianLocalRing.eq_of_residueFieldMap_eq` for the uniqueness of the lift. -/
+lemma HenselianLocalRing.exist_residueFieldMap_eq_of_etale [HenselianLocalRing R] [IsLocalRing A]
+    [IsLocalHom (algebraMap R A)] [Algebra.Etale R A] [IsLocalRing B] [Module.Finite R B]
+    (f : 𝓀[A] →ₐ[𝓀[R]] 𝓀[B]) :
+    ∃ (g : A →ₐ[R] B) (_ : IsLocalHom g.toRingHom), ResidueField.map g.toRingHom = f.toRingHom := by
+  have : HenselianLocalRing B := .of_finite (R := R)
+  let f' : B ⊗[R] A →ₐ[B] 𝓀[B] :=
+    Algebra.TensorProduct.lift (Algebra.ofId _ _)
+      ((f.restrictScalars R).comp <| IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _
+  obtain ⟨g, hg⟩ := HenselianLocalRing.ofId_comp_bijective.surjective f'
+  let g' := (g.restrictScalars R).comp Algebra.TensorProduct.includeRight
+  have H (x : _) : residue B (g' x) = f (residue _ x) := by
+    trans f' (1 ⊗ₜ x)
+    · exact congr($hg (1 ⊗ₜ x))
+    · simp [f']
+  have : IsLocalHom g'.toRingHom := by
+    refine ⟨fun x hx ↦ ?_⟩
+    rw [← residue_ne_zero_iff_isUnit] at hx
+    simpa [H, f'] using hx
+  refine ⟨g', this, ?_⟩
+  ext x
+  obtain ⟨x, rfl⟩ := residue_surjective x
+  simp [ResidueField.map_residue, H]
+
+lemma HenselianLocalRing.eq_of_residueFieldMap_eq [HenselianLocalRing R]
+    [IsLocalRing A] [Algebra.Etale R A] [IsLocalRing B] [Module.Finite R B]
+    (f₁ f₂ : A →ₐ[R] B) [IsLocalHom f₁.toRingHom] [IsLocalHom f₂.toRingHom]
+    (H : ResidueField.map f₁.toRingHom = ResidueField.map f₂.toRingHom) : f₁ = f₂ := by
+  have : HenselianLocalRing B := .of_finite (R := R)
+  have := (HenselianLocalRing.ofId_comp_bijective (R := B) (A := B ⊗[R] A)).injective
+    (a₁ := (Algebra.TensorProduct.lift (Algebra.ofId _ _) f₁ fun _ _ ↦ .all _ _))
+    (a₂ := (Algebra.TensorProduct.lift (Algebra.ofId _ _) f₂ fun _ _ ↦ .all _ _))
+    (by ext a; simpa using congr($H (algebraMap _ _ a)))
+  ext x
+  simpa using congr($this (1 ⊗ₜ x))
+
+lemma HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale [HenselianLocalRing R]
+    [IsLocalRing A] [Module.Finite R A] [Algebra.Etale R A]
+    [IsLocalRing B] [Module.Finite R B] [Algebra.Etale R B]
+    (f : 𝓀[A] ≃ₐ[𝓀[R]] 𝓀[B]) :
+    ∃ (g : A ≃ₐ[R] B), ResidueField.map g.toRingHom = f.toRingHom := by
+  obtain ⟨φ, hφ, hφ'⟩ := exist_residueFieldMap_eq_of_etale f.toAlgHom
+  obtain ⟨ψ, hψ, hψ'⟩ := exist_residueFieldMap_eq_of_etale f.symm.toAlgHom
+  have : φ.comp ψ = .id _ _ := by
+    have : IsLocalHom (AlgHom.id R B).toRingHom := by dsimp; infer_instance
+    have : IsLocalHom (φ.comp ψ).toRingHom := by
+      dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢; exact RingHom.isLocalHom_comp _ _
+    apply HenselianLocalRing.eq_of_residueFieldMap_eq
+    dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢ hφ' hψ'
+    simp only [ResidueField.map_comp, ResidueField.map_id, *]
+    ext; simp
+  have : ψ.comp φ = .id _ _ := by
+    have : IsLocalHom (AlgHom.id R A).toRingHom := by dsimp; infer_instance
+    have : IsLocalHom (ψ.comp φ).toRingHom := by
+      dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢; exact RingHom.isLocalHom_comp _ _
+    apply HenselianLocalRing.eq_of_residueFieldMap_eq
+    dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢ hφ' hψ'
+    simp only [ResidueField.map_comp, ResidueField.map_id, *]
+    ext; simp
+  exact ⟨.ofAlgHom φ ψ ‹_› ‹_›, hφ'⟩
+
+/-- Suppose `R` is a henselian local ring and `A` is a finite étale local `R-`algebra.
+Then `Aut(A/R) ≃ Gal(k(A)/k(R))`.
+
+Paired with `galRestrict`, this shows that `Gal(Frac A / Frac R) ≃* Gal(k(A)/k(R))`. -/
+def HenselianLocalRing.algEquivEquiv [HenselianLocalRing R]
+    [IsLocalRing A] [Module.Finite R A] [Algebra.Etale R A] :
+    (A ≃ₐ[R] A) ≃* Gal(𝓀[A]/𝓀[R]) :=
+  .ofBijective (F := MonoidHom _ _)
+    { toFun f :=
+      { __ := ResidueField.mapEquiv f,
+        commutes' r := by obtain ⟨r, rfl⟩ := residue_surjective r; simp  }
+      map_one' := AlgEquiv.ext fun _ ↦ congr($ResidueField.map_id _)
+      map_mul' f g :=
+        AlgEquiv.ext fun x ↦ congr($(ResidueField.map_comp g.toRingHom f.toRingHom) x) } <|
+    ⟨fun f g e ↦ AlgEquiv.coe_toAlgHom_injective (HenselianLocalRing.eq_of_residueFieldMap_eq
+      f.toAlgHom g.toAlgHom congr(($e).toRingHom)), fun f ↦ by
+    have ⟨g, hg⟩ := HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale f
+    exact ⟨g, AlgEquiv.ext fun _ ↦ congr($hg _)⟩⟩
diff --git a/Mathlib/RingTheory/Idempotents.lean b/Mathlib/RingTheory/Idempotents.lean
index 815c057d4267b7..89fbebcf07e122 100644
--- a/Mathlib/RingTheory/Idempotents.lean
+++ b/Mathlib/RingTheory/Idempotents.lean
@@ -5,6 +5,7 @@ Authors: Andrew Yang
 -/
 module
 
+public import Mathlib.Algebra.Algebra.Tower
 public import Mathlib.Algebra.BigOperators.Fin
 public import Mathlib.Algebra.Ring.GeomSum
 public import Mathlib.RingTheory.Ideal.Quotient.Operations
@@ -587,6 +588,40 @@ instance [NonUnitalCommRing R] (idem : IsIdempotentElem e) : CommRing idem.Corne
   __ : NonUnitalCommRing idem.Corner :=
     inferInstanceAs <| NonUnitalCommRing (NonUnitalRing.corner e)
 
+instance {R S : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
+    {e : S} (he : IsIdempotentElem e) : Algebra R he.Corner where
+  smul r x := ⟨r • x.1, by
+    simp [he, Subsemigroup.mem_corner_iff, (Subsemigroup.mem_corner_iff he).mp x.2]⟩
+  algebraMap :=
+  { toFun r := ⟨r • e, by simp [he, Subsemigroup.mem_corner_iff, he.eq]⟩
+    map_one' := by simp; rfl
+    map_mul' a b := Subtype.ext <| show (a * b) • e = (a • e) * (b • e) by
+      simp [he.eq, ← mul_smul, mul_comm]
+    map_zero' := by simp; rfl
+    map_add' a b := Subtype.ext (add_smul _ _ _) }
+  commutes' r x := Subtype.ext (show r • e * x.1 = x.1 * r • e by
+    simp [(Subsemigroup.mem_corner_iff he).mp x.2])
+  smul_def' r x := Subtype.ext (show r • x.1 = (r • e) * x.1 by
+    simp [(Subsemigroup.mem_corner_iff he).mp x.2])
+
+instance {R R' S : Type*} [CommSemiring R] [CommSemiring R'] [Semiring S] [Algebra R S]
+    [Algebra R R'] [Algebra R' S] [IsScalarTower R R' S]
+    {e : S} (he : IsIdempotentElem e) : IsScalarTower R R' he.Corner :=
+  .of_algebraMap_eq fun _ ↦ Subtype.ext (IsScalarTower.algebraMap_smul _ _ _).symm
+
+lemma IsIdempotentElem.toCorner_surjective [CommSemiring R] {e : R} (he : IsIdempotentElem e) :
+    Function.Surjective (algebraMap R he.Corner) :=
+  fun x ↦ ⟨x.1, Subtype.ext ((Subsemigroup.mem_corner_iff he).mp x.2).2⟩
+
+lemma IsIdempotentElem.ker_toCorner [CommRing R] {e : R} (he : IsIdempotentElem e) :
+    RingHom.ker (algebraMap R he.Corner) = Ideal.span {1 - e} := by
+  apply le_antisymm
+  · intro x hx
+    refine Ideal.mem_span_singleton.mpr ⟨x, ?_⟩
+    simp [show x * e = 0 from congr($(hx).1), sub_mul, mul_comm e]
+  · simpa [Ideal.span_le, sub_eq_zero, -FaithfulSMul.ker_algebraMap_eq_bot] using!
+      Subtype.ext he.eq.symm
+
 variable {I : Type*} [Fintype I] {e : I → R}
 
 /-- A complete orthogonal family of central idempotents in a semiring

From a3b4e386713f04369f04367e9c9aa5190aba46b6 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Fri, 26 Jun 2026 23:33:28 +0200
Subject: [PATCH 2/9] fix

---
 Mathlib/LinearAlgebra/Dimension/Free.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean
index b4158658b90a7a..b850a4a71c08b7 100644
--- a/Mathlib/LinearAlgebra/Dimension/Free.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Free.lean
@@ -362,7 +362,7 @@ noncomputable def _root_.LinearEquiv.smul_id_of_finrank_eq_one (d1 : Module.finr
 
 lemma finrank_eq_one_iff_algebraMap_bijective
     {R S : Type*} [CommSemiring R] [CommSemiring S] [StrongRankCondition R] [Algebra R S]
-    [Module.Free R S] [Nontrivial R] :
+    [Module.Free R S] :
     Module.finrank R S = 1 ↔ Function.Bijective (algebraMap R S) := by
   constructor
   · intro H

From 3b7d37987e0261e8317d6c688140a7f4e293226d Mon Sep 17 00:00:00 2001
From: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Date: Sat, 27 Jun 2026 12:00:39 +0200
Subject: [PATCH 3/9] Apply suggestions from code review

Co-authored-by: Christian Merten <christian@merten.dev>
---
 Mathlib/RingTheory/Henselian.lean | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
index 8d0c5e48403449..404a9a99f125e7 100644
--- a/Mathlib/RingTheory/Henselian.lean
+++ b/Mathlib/RingTheory/Henselian.lean
@@ -38,11 +38,11 @@ In this case the first condition is automatic, and in the second condition we ma
 * `Henselian.TFAE`: equivalent ways of expressing the Henselian property for local rings
 * `IsAdicComplete.henselianRing`:
   a ring `R` with ideal `I` that is `I`-adically complete is Henselian at `I`
-* `HenselianLocalRing.ofId_comp_bijective`: The étale lifting property for henselian local rings:
-  If `R` is an henselian local ring with residue field `k`, then for any étale `R`-algebra `A`,
+* `HenselianLocalRing.ofId_comp_bijective`: The étale lifting property for Henselian local rings:
+  If `R` is a Henselian local ring with residue field `k`, then for any étale `R`-algebra `A`,
   every `A →ₐ[R] k` lifts uniquely to an `A →ₐ[R] R`.
-* `HenselianLocalRing.of_finite`: Finite local extensions of henselian local rings are henselian.
-* `HenselianLocalRing.algEquivEquiv`: If `A` is finite local étale over a henselian local ring `R`,
+* `HenselianLocalRing.of_finite`: Finite local extensions of Henselian local rings are Henselian.
+* `HenselianLocalRing.algEquivEquiv`: If `A` is finite local étale over a Henselian local ring `R`,
   then `Aut(A/R) ≃ Gal(k(A)/k(R))`.
 
 ## References
@@ -283,7 +283,7 @@ open nonZeroDivisors
 variable {R A B : Type*} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
 
 attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
-/-- If `R` is an henselian local ring with residue field `k`, then for any étale `R`-algebra `A`,
+/-- If `R` is a Henselian local ring with residue field `k`, then for any étale `R`-algebra `A`,
 every `A →ₐ[R] k` lifts uniquely to an `A →ₐ[R] R`. -/
 @[stacks 04GG "(1) => (7)"]
 lemma HenselianLocalRing.ofId_comp_bijective [Algebra.Etale R A] [HenselianLocalRing R] :
@@ -299,7 +299,7 @@ lemma HenselianLocalRing.ofId_comp_bijective [Algebra.Etale R A] [HenselianLocal
         exact hrP
       have hf₂ : IsUnit (f₂ r) := by
         rw [← residue_ne_zero_iff_isUnit]
-        refine congr($H r).symm.trans_ne hrP
+        exact congr($H r).symm.trans_ne hrP
       have : IsLocalization.liftAlgHom (S := Localization.Away r) (f := f₁) (M := .powers r)
             (by simp [Submonoid.mem_powers_iff, hf₁.pow _]) =
           IsLocalization.liftAlgHom (f := f₂) (M := .powers r)
@@ -479,7 +479,7 @@ private theorem HenselianLocalRing.of_finite_aux [IsLocalRing A]
   simpa [← ResidueField.algebraMap_eq, hrootf, -mul_eq_zero, -mul_eq_left₀, -mul_eq_right₀] using
     congr(aeval root $hg).symm
 
-/-- A finite local ring over an henselian local ring is also henselian.
+/-- A finite local ring over a Henselian local ring is also Henselian.
 
 This proof hides the fact that
 (every finite extension is a product of local rings) implies henselian.
@@ -508,7 +508,6 @@ lemma HenselianLocalRing.of_finite
       .of_split ⟨⟨Subtype.val, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩
         (IsScalarTower.toAlgHom _ (AdjoinRoot f) _).toLinearMap
         (LinearMap.ext fun a ↦ Subtype.ext ((Subsemigroup.mem_corner_iff (he.idem i)).mp a.2).2)
-    have : Module.Flat A (he.idem i).Corner := Module.Flat.of_projective
     Module.free_of_flat_of_isLocalRing
   have hroot :
       1 ⊗ₜ algebraMap _ (he.idem i).Corner (AdjoinRoot.root f) = residue A a₀ ⊗ₜ[A] 1 :=

From 0598017aba237c8eaed9a18f3fb8bc445192d26d Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sat, 27 Jun 2026 12:56:00 +0200
Subject: [PATCH 4/9] address comments

---
 Mathlib/RingTheory/Henselian.lean             | 182 ++++++++----------
 Mathlib/RingTheory/Idempotents.lean           |  11 +-
 .../IsIntegralClosure/Basic.lean              |  13 ++
 3 files changed, 107 insertions(+), 99 deletions(-)

diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
index 8d0c5e48403449..826399d8d9c1d7 100644
--- a/Mathlib/RingTheory/Henselian.lean
+++ b/Mathlib/RingTheory/Henselian.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Polynomial.Taylor
 public import Mathlib.RingTheory.LocalRing.ResidueField.Basic
 public import Mathlib.RingTheory.AdicCompletion.Basic
 public import Mathlib.RingTheory.Etale.QuasiFinite
+public import Mathlib.RingTheory.IdempotentInstances
 public import Mathlib.RingTheory.Unramified.LocalStructure
 
 /-!
@@ -282,75 +283,81 @@ open nonZeroDivisors
 
 variable {R A B : Type*} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
 
+attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
+/-- If `R` is an local ring with residue field `k`, then for any étale `R`-algebra `A`,
+every `A →ₐ[R] k` lifts to at most one an `A →ₐ[R] R`. -/
+lemma IsLocalRing.ofId_comp_injective [Algebra.Etale R A] [IsLocalRing R] :
+    Function.Injective ((Algebra.ofId R 𝓀[R]).comp : (A →ₐ[R] R) → (A →ₐ[R] 𝓀[R])) := by
+  intro f₁ f₂ H
+  wlog _ : Algebra.IsStandardEtale R A
+  · let P := RingHom.ker ((IsScalarTower.toAlgHom R R 𝓀[R]).comp f₁).toRingHom
+    have inst : P.IsPrime := RingHom.ker_isPrime _
+    obtain ⟨r, hrP, _⟩ := Algebra.IsEtaleAt.exists_isStandardEtale (R := R) P
+    have hf₁ : IsUnit (f₁ r) := by
+      rw [← residue_ne_zero_iff_isUnit]
+      exact hrP
+    have hf₂ : IsUnit (f₂ r) := by
+      rw [← residue_ne_zero_iff_isUnit]
+      refine congr($H r).symm.trans_ne hrP
+    have : IsLocalization.liftAlgHom (S := Localization.Away r) (f := f₁) (M := .powers r)
+          (by simp [Submonoid.mem_powers_iff, hf₁.pow _]) =
+        IsLocalization.liftAlgHom (f := f₂) (M := .powers r)
+          (by simp [Submonoid.mem_powers_iff, hf₂.pow _]) := by
+      refine this (IsLocalization.algHom_ext (.powers r) ?_) inferInstance
+      ext x
+      simpa [Algebra.algHom] using congr($H x)
+    ext x
+    simpa using congr($this (algebraMap _ _ x))
+  obtain ⟨𝓟⟩ := Algebra.IsStandardEtale.nonempty_standardEtalePresentation (R := R) (S := A)
+  apply 𝓟.hom_ext
+  apply IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub (f := 𝓟.f)
+  · rw [← coe_aeval_eq_eval, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]
+  · rw [← coe_aeval_eq_eval, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]
+  · rw [← mem_nonunits_iff, ← mem_maximalIdeal, ← residue_eq_zero_iff, map_sub, sub_eq_zero]
+    exact congr($H _)
+  · rw [← coe_aeval_eq_eval, aeval_algHom_apply]
+    simpa using 𝓟.hasMap.isUnit_derivative_f.map f₁
+
 attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
 /-- If `R` is an henselian local ring with residue field `k`, then for any étale `R`-algebra `A`,
 every `A →ₐ[R] k` lifts uniquely to an `A →ₐ[R] R`. -/
 @[stacks 04GG "(1) => (7)"]
 lemma HenselianLocalRing.ofId_comp_bijective [Algebra.Etale R A] [HenselianLocalRing R] :
     Function.Bijective ((Algebra.ofId R 𝓀[R]).comp : (A →ₐ[R] R) → (A →ₐ[R] 𝓀[R])) := by
-  constructor
-  · intro f₁ f₂ H
-    wlog _ : Algebra.IsStandardEtale R A
-    · let P := RingHom.ker ((IsScalarTower.toAlgHom R R 𝓀[R]).comp f₁).toRingHom
-      have inst : P.IsPrime := RingHom.ker_isPrime _
-      obtain ⟨r, hrP, _⟩ := Algebra.IsEtaleAt.exists_isStandardEtale (R := R) P
-      have hf₁ : IsUnit (f₁ r) := by
-        rw [← residue_ne_zero_iff_isUnit]
-        exact hrP
-      have hf₂ : IsUnit (f₂ r) := by
-        rw [← residue_ne_zero_iff_isUnit]
-        refine congr($H r).symm.trans_ne hrP
-      have : IsLocalization.liftAlgHom (S := Localization.Away r) (f := f₁) (M := .powers r)
-            (by simp [Submonoid.mem_powers_iff, hf₁.pow _]) =
-          IsLocalization.liftAlgHom (f := f₂) (M := .powers r)
-            (by simp [Submonoid.mem_powers_iff, hf₂.pow _]) := by
-        refine this (IsLocalization.algHom_ext (.powers r) ?_) inferInstance
-        ext x
-        simpa [Algebra.algHom] using congr($H x)
-      ext x
-      simpa using congr($this (algebraMap _ _ x))
-    obtain ⟨𝓟⟩ := Algebra.IsStandardEtale.nonempty_standardEtalePresentation (R := R) (S := A)
-    apply 𝓟.hom_ext
-    apply IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub (f := 𝓟.f)
-    · rw [← coe_aeval_eq_eval, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]
-    · rw [← coe_aeval_eq_eval, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]
-    · rw [← mem_nonunits_iff, ← mem_maximalIdeal, ← residue_eq_zero_iff, map_sub, sub_eq_zero]
-      exact congr($H _)
-    · rw [← coe_aeval_eq_eval, aeval_algHom_apply]
-      simpa using 𝓟.hasMap.isUnit_derivative_f.map f₁
-  · intro f
-    let P := RingHom.ker f.toRingHom
-    have : P.IsPrime := RingHom.ker_isPrime _
-    obtain ⟨r, hrP, ⟨⟨𝓟⟩⟩⟩ := Algebra.IsEtaleAt.exists_isStandardEtale (R := R) P
-    let φ : Localization.Away r →ₐ[R] 𝓀[R] :=
-      IsLocalization.liftAlgHom (M := .powers r) (f := f) <| Subtype.forall.mpr <|
-        show Submonoid.powers r ≤ (IsUnit.submonoid _).comap _ from Submonoid.powers_le.mpr
-        (by simpa [IsUnit.mem_submonoid_iff])
-    obtain ⟨x, hx⟩ := residue_surjective (φ 𝓟.x)
-    obtain ⟨y, hy, hxy⟩ := HenselianLocalRing.is_henselian 𝓟.f 𝓟.monic_f x (by
-      rw [← residue_eq_zero_iff, ← ResidueField.algebraMap_eq, eval, hom_eval₂, RingHom.comp_id,
-        ← aeval_def, ResidueField.algebraMap_eq, hx, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]) (by
-      rw [← residue_ne_zero_iff_isUnit, ← ResidueField.algebraMap_eq, eval, hom_eval₂,
-        RingHom.comp_id, ← aeval_def, ResidueField.algebraMap_eq, hx, aeval_algHom_apply]
-      exact (𝓟.hasMap.isUnit_derivative_f.map φ).ne_zero)
-    rw [← residue_eq_zero_iff, map_sub, sub_eq_zero] at hxy
-    have Hy : 𝓟.HasMap y := by
-      refine ⟨hy, ?_⟩
-      rw [← residue_ne_zero_iff_isUnit, ← ResidueField.algebraMap_eq, ← aeval_algebraMap_apply,
-        ResidueField.algebraMap_eq, hxy, hx, aeval_algHom_apply]
-      exact (𝓟.hasMap.2.map φ).ne_zero
-    refine ⟨((𝓟.lift _ Hy).comp 𝓟.equivRing.toAlgHom).comp (IsScalarTower.toAlgHom _ _ _), ?_⟩
-    trans ((φ.comp 𝓟.equivRing.symm.toAlgHom).comp 𝓟.equivRing.toAlgHom).comp
-        (IsScalarTower.toAlgHom _ _ _)
-    · simp_rw [← AlgHom.comp_assoc]
-      congr 2
-      ext
-      simp [hxy, hx]
-    · ext; simp [φ]
+  refine ⟨IsLocalRing.ofId_comp_injective, fun f ↦ ?_⟩
+  let P := RingHom.ker f.toRingHom
+  have : P.IsPrime := RingHom.ker_isPrime _
+  obtain ⟨r, hrP, ⟨⟨𝓟⟩⟩⟩ := Algebra.IsEtaleAt.exists_isStandardEtale (R := R) P
+  let φ : Localization.Away r →ₐ[R] 𝓀[R] :=
+    IsLocalization.liftAlgHom (M := .powers r) (f := f) <| Subtype.forall.mpr <|
+      show Submonoid.powers r ≤ (IsUnit.submonoid _).comap _ from Submonoid.powers_le.mpr
+      (by simpa [IsUnit.mem_submonoid_iff])
+  obtain ⟨x, hx⟩ := residue_surjective (φ 𝓟.x)
+  obtain ⟨y, hy, hxy⟩ := HenselianLocalRing.is_henselian 𝓟.f 𝓟.monic_f x (by
+    rw [← residue_eq_zero_iff, ← ResidueField.algebraMap_eq, eval, hom_eval₂, RingHom.comp_id,
+      ← aeval_def, ResidueField.algebraMap_eq, hx, aeval_algHom_apply, 𝓟.hasMap.1, map_zero]) (by
+    rw [← residue_ne_zero_iff_isUnit, ← ResidueField.algebraMap_eq, eval, hom_eval₂,
+      RingHom.comp_id, ← aeval_def, ResidueField.algebraMap_eq, hx, aeval_algHom_apply]
+    exact (𝓟.hasMap.isUnit_derivative_f.map φ).ne_zero)
+  rw [← residue_eq_zero_iff, map_sub, sub_eq_zero] at hxy
+  have Hy : 𝓟.HasMap y := by
+    refine ⟨hy, ?_⟩
+    rw [← residue_ne_zero_iff_isUnit, ← ResidueField.algebraMap_eq, ← aeval_algebraMap_apply,
+      ResidueField.algebraMap_eq, hxy, hx, aeval_algHom_apply]
+    exact (𝓟.hasMap.2.map φ).ne_zero
+  refine ⟨((𝓟.lift _ Hy).comp 𝓟.equivRing.toAlgHom).comp (IsScalarTower.toAlgHom _ _ _), ?_⟩
+  trans ((φ.comp 𝓟.equivRing.symm.toAlgHom).comp 𝓟.equivRing.toAlgHom).comp
+      (IsScalarTower.toAlgHom _ _ _)
+  · simp_rw [← AlgHom.comp_assoc]
+    congr 2
+    ext
+    simp [hxy, hx]
+  · ext; simp [φ]
 
 attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
 set_option backward.isDefEq.respectTransparency false in
-/-- A finite algebra over an henselian local ring is a product of (henselian) local rings.
+/-- A finite algebra over a Henselian local ring is a product of (Henselian) local rings.
+(See `HenselianLocalRing.of_finite` for the Henselian part)
 
 TODO: show that the local rings are exactly `Aₘ` with `m` maximal ideals of `A`. -/
 @[stacks 04GG "(1) => (10)"]
@@ -416,15 +423,15 @@ lemma HenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRing
     have hQP'' : (P' i).comap Algebra.TensorProduct.includeRight.toRingHom = Q := by
       rw [← hQP', Ideal.comap_comap]; convert Ideal.comap_id _; ext; simp [ψ']
     have heQ : RingHom.ker (algebraMap A he₀.Corner) ≤ Q := by
-      rw [he₀.ker_toCorner, Ideal.span_le]
+      rw [he₀.ker_algebraMap_corner, Ideal.span_le]
       simp only [Set.singleton_subset_iff, SetLike.mem_coe]
       rw [← Ideal.IsPrime.mul_mem_left_iff (I := Q) fun h ↦ hP' i (hQP'.le h)]
       simp [mul_sub, ← map_mul, (he.idem _).eq]
-    have := Ideal.IsMaximal.map_of_surjective_of_ker_le he₀.toCorner_surjective heQ
+    have := Ideal.IsMaximal.map_of_surjective_of_ker_le he₀.algebraMap_corner_surjective heQ
     refine IsLocalRing.of_unique_max_ideal ⟨Q.map (algebraMap A he₀.Corner), ‹_›, fun Q' hQ' ↦ ?_⟩
-    have inst := Ideal.comap_isMaximal_of_surjective _ he₀.toCorner_surjective (K := Q')
+    have inst := Ideal.comap_isMaximal_of_surjective _ he₀.algebraMap_corner_surjective (K := Q')
     refine (hQ'.eq_of_le this.ne_top ?_)
-    refine Ideal.le_map_of_comap_le_of_surjective _ he₀.toCorner_surjective ?_
+    refine Ideal.le_map_of_comap_le_of_surjective _ he₀.algebraMap_corner_surjective ?_
     suffices (Q'.comap (algebraMap A _)).comap ψ'.toRingHom = P' i by
       rw [← hQP'', ← this, Ideal.comap_comap,]
       simp only [AlgHom.toRingHom_eq_coe, ← AlgHom.comp_toRingHom, ψ', Function.comp_apply, le_refl,
@@ -459,8 +466,8 @@ private theorem HenselianLocalRing.of_finite_aux [IsLocalRing A]
     simpa using ha₀'
   let φ' : he.Corner →ₐ[A] 𝓀[A] := by
     refine AlgHom.liftOfSurjective (IsScalarTower.toAlgHom _ _ _)
-      he.toCorner_surjective φ ?_
-    refine he.ker_toCorner.trans_le ((Ideal.span_singleton_le_iff_mem _).mpr ?_)
+      he.algebraMap_corner_surjective φ ?_
+    refine he.ker_algebraMap_corner.trans_le ((Ideal.span_singleton_le_iff_mem _).mpr ?_)
     rw [← Ideal.IsPrime.mul_mem_left_iff (by exact ha₀''), mul_sub, mul_one, he.eq, sub_self]
     exact zero_mem _
   have hφ' (x : AdjoinRoot f) : φ' (algebraMap _ _ x) = φ x :=
@@ -502,14 +509,8 @@ lemma HenselianLocalRing.of_finite
     by_contra! H
     exact Ideal.one_notMem (RingHom.ker φ.toRingHom) (he.complete ▸ sum_mem fun i _ ↦ H i)
   have : Module.Finite A (he.idem i).Corner := .of_surjective
-    (IsScalarTower.toAlgHom _ (AdjoinRoot f) _).toLinearMap (he.idem i).toCorner_surjective
-  have : Module.Free A (he.idem i).Corner :=
-    have : Module.Projective A (he.idem i).Corner :=
-      .of_split ⟨⟨Subtype.val, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩
-        (IsScalarTower.toAlgHom _ (AdjoinRoot f) _).toLinearMap
-        (LinearMap.ext fun a ↦ Subtype.ext ((Subsemigroup.mem_corner_iff (he.idem i)).mp a.2).2)
-    have : Module.Flat A (he.idem i).Corner := Module.Flat.of_projective
-    Module.free_of_flat_of_isLocalRing
+    (IsScalarTower.toAlgHom _ (AdjoinRoot f) _).toLinearMap (he.idem i).algebraMap_corner_surjective
+  have : Module.Free A (he.idem i).Corner := Module.free_of_flat_of_isLocalRing
   have hroot :
       1 ⊗ₜ algebraMap _ (he.idem i).Corner (AdjoinRoot.root f) = residue A a₀ ⊗ₜ[A] 1 :=
     HenselianLocalRing.of_finite_aux f a₀ ha₀ ha₀' _ (he.idem i) hi
@@ -517,7 +518,7 @@ lemma HenselianLocalRing.of_finite
     intro x
     obtain ⟨x, rfl⟩ := Algebra.TensorProduct.includeRight_surjective _
       (by exact residue_surjective) x
-    obtain ⟨x, rfl⟩ := (he.idem i).toCorner_surjective x
+    obtain ⟨x, rfl⟩ := (he.idem i).algebraMap_corner_surjective x
     obtain ⟨g, rfl⟩ := AdjoinRoot.mk_surjective x
     have h₁ : residue _ (eval a₀ g) = φ (.mk f g) := by simp [φ]
     have h₂ : (IsScalarTower.toAlgHom _ _ (𝓀[A] ⊗[A] (he.idem i).Corner)).comp φ =
@@ -531,7 +532,7 @@ lemma HenselianLocalRing.of_finite
     apply le_antisymm ?_ ((Module.finrank_pos_iff_of_free _ _).mpr inferInstance)
     · rw [← Module.finrank_baseChange (R := 𝓀[A]), finrank_le_one_iff]
       refine ⟨1, H.forall.mpr fun x ↦ ⟨x, by simp [Algebra.smul_def]⟩⟩
-  rw [Module.finrank_eq_one_iff_algebraMap_bijective] at this
+  rw [Algebra.finrank_eq_one_iff_bijective_algebraMap] at this
   obtain ⟨a, ha⟩ := this.2 (algebraMap _ _ (AdjoinRoot.root f))
   refine ⟨a, this.1 ?_, ?_⟩
   · rw [eval, hom_eval₂, RingHom.comp_id, ← aeval_def, ha, aeval_algebraMap_apply]
@@ -542,24 +543,12 @@ lemma HenselianLocalRing.of_finite
     · simp
     · rw [ha]; simp [← hroot]
 
-instance {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R]
-    [Algebra.IsIntegral R S] [Nontrivial S] : IsLocalHom (algebraMap R S) := by
-  have : (algebraMap R S).kerLift.IsIntegral :=
-    .tower_top (Ideal.Quotient.mk _) _
-      (by have := algebraMap_isIntegral_iff.mpr ‹Algebra.IsIntegral R S›; exact this)
-  have := this.isLocalHom (algebraMap R S).kerLift_injective
-  have : Nontrivial (R ⧸ RingHom.ker (algebraMap R S)) :=
-    Ideal.Quotient.nontrivial_iff.mpr (RingHom.ker_ne_top _)
-  have : IsLocalHom (Ideal.Quotient.mk (RingHom.ker (algebraMap R S))) :=
-    .of_surjective _ Ideal.Quotient.mk_surjective
-  exact RingHom.isLocalHom_comp (algebraMap R S).kerLift (Ideal.Quotient.mk _)
-
 /-- Let `R` be an henselian local ring, `A, B` be local `R`-algebras.
 Suppose `A` is etale and `B` is module-finite, then any `k(R)`-algebra map `k(A) → k(B)` lifts to
 an `R`-algebra map `A → B`.
 
 See `HenselianLocalRing.eq_of_residueFieldMap_eq` for the uniqueness of the lift. -/
-lemma HenselianLocalRing.exist_residueFieldMap_eq_of_etale [HenselianLocalRing R] [IsLocalRing A]
+lemma HenselianLocalRing.exists_residueFieldMap_eq_of_etale [HenselianLocalRing R] [IsLocalRing A]
     [IsLocalHom (algebraMap R A)] [Algebra.Etale R A] [IsLocalRing B] [Module.Finite R B]
     (f : 𝓀[A] →ₐ[𝓀[R]] 𝓀[B]) :
     ∃ (g : A →ₐ[R] B) (_ : IsLocalHom g.toRingHom), ResidueField.map g.toRingHom = f.toRingHom := by
@@ -582,12 +571,11 @@ lemma HenselianLocalRing.exist_residueFieldMap_eq_of_etale [HenselianLocalRing R
   obtain ⟨x, rfl⟩ := residue_surjective x
   simp [ResidueField.map_residue, H]
 
-lemma HenselianLocalRing.eq_of_residueFieldMap_eq [HenselianLocalRing R]
+lemma IsLocalRing.eq_of_residueFieldMap_eq
     [IsLocalRing A] [Algebra.Etale R A] [IsLocalRing B] [Module.Finite R B]
     (f₁ f₂ : A →ₐ[R] B) [IsLocalHom f₁.toRingHom] [IsLocalHom f₂.toRingHom]
     (H : ResidueField.map f₁.toRingHom = ResidueField.map f₂.toRingHom) : f₁ = f₂ := by
-  have : HenselianLocalRing B := .of_finite (R := R)
-  have := (HenselianLocalRing.ofId_comp_bijective (R := B) (A := B ⊗[R] A)).injective
+  have := (IsLocalRing.ofId_comp_injective (R := B) (A := B ⊗[R] A))
     (a₁ := (Algebra.TensorProduct.lift (Algebra.ofId _ _) f₁ fun _ _ ↦ .all _ _))
     (a₂ := (Algebra.TensorProduct.lift (Algebra.ofId _ _) f₂ fun _ _ ↦ .all _ _))
     (by ext a; simpa using congr($H (algebraMap _ _ a)))
@@ -599,13 +587,13 @@ lemma HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale [HenselianLo
     [IsLocalRing B] [Module.Finite R B] [Algebra.Etale R B]
     (f : 𝓀[A] ≃ₐ[𝓀[R]] 𝓀[B]) :
     ∃ (g : A ≃ₐ[R] B), ResidueField.map g.toRingHom = f.toRingHom := by
-  obtain ⟨φ, hφ, hφ'⟩ := exist_residueFieldMap_eq_of_etale f.toAlgHom
-  obtain ⟨ψ, hψ, hψ'⟩ := exist_residueFieldMap_eq_of_etale f.symm.toAlgHom
+  obtain ⟨φ, hφ, hφ'⟩ := exists_residueFieldMap_eq_of_etale f.toAlgHom
+  obtain ⟨ψ, hψ, hψ'⟩ := exists_residueFieldMap_eq_of_etale f.symm.toAlgHom
   have : φ.comp ψ = .id _ _ := by
     have : IsLocalHom (AlgHom.id R B).toRingHom := by dsimp; infer_instance
     have : IsLocalHom (φ.comp ψ).toRingHom := by
       dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢; exact RingHom.isLocalHom_comp _ _
-    apply HenselianLocalRing.eq_of_residueFieldMap_eq
+    apply IsLocalRing.eq_of_residueFieldMap_eq
     dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢ hφ' hψ'
     simp only [ResidueField.map_comp, ResidueField.map_id, *]
     ext; simp
@@ -613,7 +601,7 @@ lemma HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale [HenselianLo
     have : IsLocalHom (AlgHom.id R A).toRingHom := by dsimp; infer_instance
     have : IsLocalHom (ψ.comp φ).toRingHom := by
       dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢; exact RingHom.isLocalHom_comp _ _
-    apply HenselianLocalRing.eq_of_residueFieldMap_eq
+    apply IsLocalRing.eq_of_residueFieldMap_eq
     dsimp [AlgHom.comp_toRingHom] at hφ hψ ⊢ hφ' hψ'
     simp only [ResidueField.map_comp, ResidueField.map_id, *]
     ext; simp
@@ -633,7 +621,7 @@ def HenselianLocalRing.algEquivEquiv [HenselianLocalRing R]
       map_one' := AlgEquiv.ext fun _ ↦ congr($ResidueField.map_id _)
       map_mul' f g :=
         AlgEquiv.ext fun x ↦ congr($(ResidueField.map_comp g.toRingHom f.toRingHom) x) } <|
-    ⟨fun f g e ↦ AlgEquiv.coe_toAlgHom_injective (HenselianLocalRing.eq_of_residueFieldMap_eq
+    ⟨fun f g e ↦ AlgEquiv.coe_toAlgHom_injective (IsLocalRing.eq_of_residueFieldMap_eq
       f.toAlgHom g.toAlgHom congr(($e).toRingHom)), fun f ↦ by
     have ⟨g, hg⟩ := HenselianLocalRing.exist_algEquiv_residueFieldMap_eq_of_etale f
     exact ⟨g, AlgEquiv.ext fun _ ↦ congr($hg _)⟩⟩
diff --git a/Mathlib/RingTheory/Idempotents.lean b/Mathlib/RingTheory/Idempotents.lean
index 89fbebcf07e122..be373ee26a487d 100644
--- a/Mathlib/RingTheory/Idempotents.lean
+++ b/Mathlib/RingTheory/Idempotents.lean
@@ -609,11 +609,18 @@ instance {R R' S : Type*} [CommSemiring R] [CommSemiring R'] [Semiring S] [Algeb
     {e : S} (he : IsIdempotentElem e) : IsScalarTower R R' he.Corner :=
   .of_algebraMap_eq fun _ ↦ Subtype.ext (IsScalarTower.algebraMap_smul _ _ _).symm
 
-lemma IsIdempotentElem.toCorner_surjective [CommSemiring R] {e : R} (he : IsIdempotentElem e) :
+@[simp]
+lemma IsIdempotentElem.algebraMap_corner_apply
+    {R S : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
+    {e : S} (he : IsIdempotentElem e) (x : R) :
+    (algebraMap R he.Corner x).1 = x • e := rfl
+
+lemma IsIdempotentElem.algebraMap_corner_surjective [CommSemiring R]
+    {e : R} (he : IsIdempotentElem e) :
     Function.Surjective (algebraMap R he.Corner) :=
   fun x ↦ ⟨x.1, Subtype.ext ((Subsemigroup.mem_corner_iff he).mp x.2).2⟩
 
-lemma IsIdempotentElem.ker_toCorner [CommRing R] {e : R} (he : IsIdempotentElem e) :
+lemma IsIdempotentElem.ker_algebraMap_corner [CommRing R] {e : R} (he : IsIdempotentElem e) :
     RingHom.ker (algebraMap R he.Corner) = Ideal.span {1 - e} := by
   apply le_antisymm
   · intro x hx
diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
index 13ef5f6e66b7ec..415f311fb1fd22 100644
--- a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
+++ b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Ring.Int.Field
 public import Mathlib.RingTheory.FiniteType
 public import Mathlib.RingTheory.IntegralClosure.Algebra.Basic
 public import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs
+public import Mathlib.RingTheory.LocalRing.RingHom.Basic
 public import Mathlib.RingTheory.Polynomial.IntegralNormalization
 public import Mathlib.RingTheory.Polynomial.ScaleRoots
 public import Mathlib.RingTheory.TensorProduct.MvPolynomial
@@ -613,6 +614,18 @@ theorem RingHom.IsIntegral.isLocalHom {f : R →+* S} (hf : f.IsIntegral)
       ← (injective_iff_map_eq_zero' _).mp inj, ← eval₂_hom]
     rwa [← eval₂_reverse_eq_zero_iff] at hp
 
+instance [Algebra R S] [IsLocalRing R] [Algebra.IsIntegral R S] [Nontrivial S] :
+    IsLocalHom (algebraMap R S) := by
+  have : (algebraMap R S).kerLift.IsIntegral :=
+    .tower_top (Ideal.Quotient.mk _) _
+      (by have := algebraMap_isIntegral_iff.mpr ‹Algebra.IsIntegral R S›; exact this)
+  have := this.isLocalHom (algebraMap R S).kerLift_injective
+  have : Nontrivial (R ⧸ RingHom.ker (algebraMap R S)) :=
+    Ideal.Quotient.nontrivial_iff.mpr (RingHom.ker_ne_top _)
+  have : IsLocalHom (Ideal.Quotient.mk (RingHom.ker (algebraMap R S))) :=
+    .of_surjective _ Ideal.Quotient.mk_surjective
+  exact RingHom.isLocalHom_comp (algebraMap R S).kerLift (Ideal.Quotient.mk _)
+
 variable [Algebra R S] [Algebra.IsIntegral R S]
 
 variable (R S) in

From 8ae282f7a3f3a554c7d61975461ff413f0f5dc3d Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sat, 27 Jun 2026 15:05:34 +0200
Subject: [PATCH 5/9] fix

---
 Mathlib.lean                                  |  1 +
 Mathlib/RingTheory/Henselian.lean             |  3 ++-
 .../IsIntegralClosure/Basic.lean              | 13 ----------
 .../LocalRing/RingHom/IsIntegral.lean         | 26 +++++++++++++++++++
 4 files changed, 29 insertions(+), 14 deletions(-)
 create mode 100644 Mathlib/RingTheory/LocalRing/RingHom/IsIntegral.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 1e5e2a2ac83c42..6744e68189da42 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6747,6 +6747,7 @@ public import Mathlib.RingTheory.LocalRing.ResidueField.Ideal
 public import Mathlib.RingTheory.LocalRing.ResidueField.Instances
 public import Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
 public import Mathlib.RingTheory.LocalRing.RingHom.Basic
+public import Mathlib.RingTheory.LocalRing.RingHom.IsIntegral
 public import Mathlib.RingTheory.LocalRing.Subring
 public import Mathlib.RingTheory.Localization.Algebra
 public import Mathlib.RingTheory.Localization.AsSubring
diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
index 4db4c87eced839..8689e341212baa 100644
--- a/Mathlib/RingTheory/Henselian.lean
+++ b/Mathlib/RingTheory/Henselian.lean
@@ -6,10 +6,11 @@ Authors: Johan Commelin, Andrew Yang
 module
 
 public import Mathlib.Algebra.Polynomial.Taylor
-public import Mathlib.RingTheory.LocalRing.ResidueField.Basic
 public import Mathlib.RingTheory.AdicCompletion.Basic
 public import Mathlib.RingTheory.Etale.QuasiFinite
 public import Mathlib.RingTheory.IdempotentInstances
+public import Mathlib.RingTheory.LocalRing.ResidueField.Basic
+public import Mathlib.RingTheory.LocalRing.RingHom.IsIntegral
 public import Mathlib.RingTheory.Unramified.LocalStructure
 
 /-!
diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
index 415f311fb1fd22..13ef5f6e66b7ec 100644
--- a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
+++ b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
@@ -10,7 +10,6 @@ public import Mathlib.Algebra.Ring.Int.Field
 public import Mathlib.RingTheory.FiniteType
 public import Mathlib.RingTheory.IntegralClosure.Algebra.Basic
 public import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs
-public import Mathlib.RingTheory.LocalRing.RingHom.Basic
 public import Mathlib.RingTheory.Polynomial.IntegralNormalization
 public import Mathlib.RingTheory.Polynomial.ScaleRoots
 public import Mathlib.RingTheory.TensorProduct.MvPolynomial
@@ -614,18 +613,6 @@ theorem RingHom.IsIntegral.isLocalHom {f : R →+* S} (hf : f.IsIntegral)
       ← (injective_iff_map_eq_zero' _).mp inj, ← eval₂_hom]
     rwa [← eval₂_reverse_eq_zero_iff] at hp
 
-instance [Algebra R S] [IsLocalRing R] [Algebra.IsIntegral R S] [Nontrivial S] :
-    IsLocalHom (algebraMap R S) := by
-  have : (algebraMap R S).kerLift.IsIntegral :=
-    .tower_top (Ideal.Quotient.mk _) _
-      (by have := algebraMap_isIntegral_iff.mpr ‹Algebra.IsIntegral R S›; exact this)
-  have := this.isLocalHom (algebraMap R S).kerLift_injective
-  have : Nontrivial (R ⧸ RingHom.ker (algebraMap R S)) :=
-    Ideal.Quotient.nontrivial_iff.mpr (RingHom.ker_ne_top _)
-  have : IsLocalHom (Ideal.Quotient.mk (RingHom.ker (algebraMap R S))) :=
-    .of_surjective _ Ideal.Quotient.mk_surjective
-  exact RingHom.isLocalHom_comp (algebraMap R S).kerLift (Ideal.Quotient.mk _)
-
 variable [Algebra R S] [Algebra.IsIntegral R S]
 
 variable (R S) in
diff --git a/Mathlib/RingTheory/LocalRing/RingHom/IsIntegral.lean b/Mathlib/RingTheory/LocalRing/RingHom/IsIntegral.lean
new file mode 100644
index 00000000000000..e91b91dda9aaf7
--- /dev/null
+++ b/Mathlib/RingTheory/LocalRing/RingHom/IsIntegral.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+public import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
+public import Mathlib.RingTheory.LocalRing.RingHom.Basic
+
+/-! # Integral ring homomorphisms over local rings are local -/
+
+@[expose] public section
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+
+instance [IsLocalRing R] [Algebra.IsIntegral R S] [Nontrivial S] :
+    IsLocalHom (algebraMap R S) := by
+  have : (algebraMap R S).kerLift.IsIntegral :=
+    .tower_top (Ideal.Quotient.mk _) _
+      (by have := algebraMap_isIntegral_iff.mpr ‹Algebra.IsIntegral R S›; exact this)
+  have := this.isLocalHom (algebraMap R S).kerLift_injective
+  have : Nontrivial (R ⧸ RingHom.ker (algebraMap R S)) :=
+    Ideal.Quotient.nontrivial_iff.mpr (RingHom.ker_ne_top _)
+  have : IsLocalHom (Ideal.Quotient.mk (RingHom.ker (algebraMap R S))) :=
+    .of_surjective _ Ideal.Quotient.mk_surjective
+  exact RingHom.isLocalHom_comp (algebraMap R S).kerLift (Ideal.Quotient.mk _)

From b50adef96c112997bf25aeaa57f9da4626a43b97 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sat, 27 Jun 2026 15:30:11 +0200
Subject: [PATCH 6/9] oops

---
 Mathlib.lean                                |  1 +
 Mathlib/RingTheory/IdempotentInstances.lean | 28 +++++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 Mathlib/RingTheory/IdempotentInstances.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 6744e68189da42..03587418af61dc 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6669,6 +6669,7 @@ public import Mathlib.RingTheory.Ideal.Quotient.PowTransition
 public import Mathlib.RingTheory.Ideal.Span
 public import Mathlib.RingTheory.IdealFilter.Basic
 public import Mathlib.RingTheory.IdealFilter.Topology
+public import Mathlib.RingTheory.IdempotentInstances
 public import Mathlib.RingTheory.Idempotents
 public import Mathlib.RingTheory.Int.Basic
 public import Mathlib.RingTheory.IntegralClosure.Algebra.Basic
diff --git a/Mathlib/RingTheory/IdempotentInstances.lean b/Mathlib/RingTheory/IdempotentInstances.lean
new file mode 100644
index 00000000000000..eeb4285e487cd3
--- /dev/null
+++ b/Mathlib/RingTheory/IdempotentInstances.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+
+public import Mathlib.RingTheory.Flat.Stability
+public import Mathlib.RingTheory.Idempotents
+
+/-! # Instances on corners -/
+
+@[expose] public section
+
+variable {R A : Type*} [CommSemiring R]
+  [CommSemiring A] [Algebra R A] {e : A} (he : IsIdempotentElem e)
+
+instance [Module.Projective R A] : Module.Projective R he.Corner :=
+  .of_split ⟨⟨Subtype.val, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩
+    (IsScalarTower.toAlgHom _ A _).toLinearMap
+    (LinearMap.ext fun a ↦ Subtype.ext ((Subsemigroup.mem_corner_iff he).mp a.2).2)
+
+instance [Module.Flat R A] : Module.Flat R he.Corner :=
+  .trans R A _
+
+instance [Module.Finite R A] : Module.Finite R he.Corner :=
+  .of_surjective (IsScalarTower.toAlgHom _ _ _).toLinearMap he.algebraMap_corner_surjective
+#min_imports

From f95fe6ae2c02ee59340216de78649370823c6065 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sat, 27 Jun 2026 16:46:13 +0200
Subject: [PATCH 7/9] oops

---
 Mathlib/RingTheory/IdempotentInstances.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/RingTheory/IdempotentInstances.lean b/Mathlib/RingTheory/IdempotentInstances.lean
index eeb4285e487cd3..749f0f87a93c26 100644
--- a/Mathlib/RingTheory/IdempotentInstances.lean
+++ b/Mathlib/RingTheory/IdempotentInstances.lean
@@ -25,4 +25,3 @@ instance [Module.Flat R A] : Module.Flat R he.Corner :=
 
 instance [Module.Finite R A] : Module.Finite R he.Corner :=
   .of_surjective (IsScalarTower.toAlgHom _ _ _).toLinearMap he.algebraMap_corner_surjective
-#min_imports

From d3b6170aa7562e7f0a546306d6d8e20cc8db863f Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sat, 27 Jun 2026 17:48:55 +0200
Subject: [PATCH 8/9] fix

---
 Mathlib/RingTheory/Henselian.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
index 8689e341212baa..d9bd85373e1537 100644
--- a/Mathlib/RingTheory/Henselian.lean
+++ b/Mathlib/RingTheory/Henselian.lean
@@ -571,7 +571,7 @@ lemma HenselianLocalRing.exists_residueFieldMap_eq_of_etale [HenselianLocalRing
   simp [ResidueField.map_residue, H]
 
 lemma IsLocalRing.eq_of_residueFieldMap_eq
-    [IsLocalRing A] [Algebra.Etale R A] [IsLocalRing B] [Module.Finite R B]
+    [IsLocalRing A] [Algebra.Etale R A] [IsLocalRing B]
     (f₁ f₂ : A →ₐ[R] B) [IsLocalHom f₁.toRingHom] [IsLocalHom f₂.toRingHom]
     (H : ResidueField.map f₁.toRingHom = ResidueField.map f₂.toRingHom) : f₁ = f₂ := by
   have := (IsLocalRing.ofId_comp_injective (R := B) (A := B ⊗[R] A))

From a010cae47a32f30dafa2e9d241e4befab9e512a5 Mon Sep 17 00:00:00 2001
From: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Date: Sat, 27 Jun 2026 21:42:31 +0200
Subject: [PATCH 9/9] Apply suggestion from @chrisflav

Co-authored-by: Christian Merten <christian@merten.dev>
---
 Mathlib/RingTheory/Henselian.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean
index d9bd85373e1537..ca2e1c39d6d506 100644
--- a/Mathlib/RingTheory/Henselian.lean
+++ b/Mathlib/RingTheory/Henselian.lean
@@ -285,7 +285,7 @@ open nonZeroDivisors
 variable {R A B : Type*} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B]
 
 attribute [local instance] Localization.AtPrime.algebraOfLiesOver in
-/-- If `R` is an local ring with residue field `k`, then for any étale `R`-algebra `A`,
+/-- If `R` is a local ring with residue field `k`, then for any étale `R`-algebra `A`,
 every `A →ₐ[R] k` lifts to at most one an `A →ₐ[R] R`. -/
 lemma IsLocalRing.ofId_comp_injective [Algebra.Etale R A] [IsLocalRing R] :
     Function.Injective ((Algebra.ofId R 𝓀[R]).comp : (A →ₐ[R] R) → (A →ₐ[R] 𝓀[R])) := by