Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
⊢ ∃ t ∉ Q,
    (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧
      (Ideal.under R Q).ResidueField[(algebraMap S Q.ResidueField) t] = ⊤

Tactic:
by
  let p := Q.under R
  #adaptation_note /-- Needed after nightly-2023-02-23 -/
  have : p.IsPrime := Ideal.IsPrime.under R Q
  #adaptation_note /-- After nightly-2026-04-06, typeclass synthesis fails to find these
  instances; provide them explicitly. -/
  let : Module p.ResidueField (p.Fiber S) := TensorProduct.leftModule
  let : SMul p.ResidueField (p.Fiber S) := this.toSMul -- added for #13807 (2026-05-20)
  let : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
  let : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
  have : IsArtinianRing (p.Fiber S) := .of_finite p.ResidueField _
  let α := PrimeSpectrum.primesOverOrderIsoFiber R S p
  obtain ⟨x, hx0, hx⟩ : ∃ x : Q.ResidueField, x ≠ 0 ∧ p.ResidueField[x] = ⊤ := by
    obtain ⟨x, hx⟩ := Field.exists_primitive_element p.ResidueField Q.ResidueField
    rw [IntermediateField.adjoin_eq_top_iff] at hx
    by_cases hx0 : x = 0
    · exact ⟨1, by simp, by simpa [p, hx0] using hx⟩
    · exact ⟨x, hx0, hx⟩
  obtain ⟨x, rfl⟩ := Ideal.Fiber.lift_residueField_surjective p _ x
  set φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField := TensorProduct.lift
      (Algebra.ofId _ _) (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _
  obtain ⟨r, hrQ, hrid, hr⟩ :=
    IsArtinianRing.exists_not_mem_forall_mem_of_ne (α ⟨Q, ‹_›, ⟨rfl⟩⟩).asIdeal
  obtain ⟨s, hsQ, t, e⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ (r * x)
  have hrQ' : φ r ≠ 0 := by
    have : Ideal.ResidueField.mapₐ p Q (ofId R S) (Ideal.over_def Q p) =
      AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField) := by ext
    rw [← AlgHom.restrictScalars_apply R, Algebra.TensorProduct.restrictScalars_lift]
    convert! hrQ
    rw [← SetLike.mem_coe, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal]
    simp [this]
  have hsQ' : algebraMap R Q.ResidueField s ≠ 0 := by
    simpa [IsScalarTower.algebraMap_apply R S Q.ResidueField]
  replace hrQ' : φ r = 1 := by
    simpa [hrQ', sub_eq_zero, @eq_comm _ _ (φ r)] using (hrid.map φ).one_sub_mul_self
  have e' : algebraMap _ _ s * φ x = algebraMap _ _ t := by
    simpa [φ, smul_def, mul_assoc, hrQ'] using congr(φ $e)
  refine ⟨t, ?_, ?_, ?_⟩
  · rw [← Ideal.algebraMap_residueField_eq_zero, ← e']
    simpa [hx0, IsScalarTower.algebraMap_apply R S Q.ResidueField]
  · rintro Q' ⟨_, _⟩ H
    let := Localization.AtPrime.algebraOfLiesOver p Q'
    have hsQ'' : algebraMap R Q'.ResidueField s ≠ 0 := by
      suffices s ∉ Q'.under _ by simpa [IsScalarTower.algebraMap_apply R S Q'.ResidueField]
      rwa [← Q'.over_def p]
    let φ' : p.Fiber S →ₐ[p.ResidueField] Q'.ResidueField := TensorProduct.lift
        (Algebra.ofId _ _) (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _
    have H : φ' r = 0 := (hr (α ⟨Q', ⟨‹_›, ‹_›⟩⟩).asIdeal inferInstance (by
        rwa [ne_eq, ← PrimeSpectrum.ext_iff, EmbeddingLike.apply_eq_iff_eq, Subtype.mk.injEq]) :)
    rw [← Ideal.algebraMap_residueField_eq_zero]
    trans φ' (1 ⊗ₜ t)
    · simp [φ']
    · simpa [smul_def, H] using congr(φ' $e).symm
  · have : φ x = (algebraMap _ p.ResidueField s)⁻¹ • algebraMap _ _ t := by
      simpa [smul_def, ← IsScalarTower.algebraMap_apply, eq_inv_mul_iff_mul_eq₀ hsQ']
    rw [← top_le_iff, ← hx, this]
    refine adjoin_singleton_le ?_
    exact Subalgebra.smul_mem _ (self_mem_adjoin_singleton _ _) _

Goal state after: