-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
inst_6 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this : p.IsPrime
have have₁ have₂ have₃ :
  ∀ (this : IsArtinianRing (p.Fiber S)),
    ∃ t ∉ Q,
      (∀ (Q' : Ideal S),
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
        Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
          (Ideal.ResidueField
              (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
          ⊤
have₄ :
  ∀ (this_1 : IsArtinianRing (p.Fiber S)) (x : Q.ResidueField) (hx0 : x ≠ 0)
    (hx : Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField) p.ResidueField[x] ⊤),
    ∃ t ∉ Q,
      (∀ (Q' : Ideal S),
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
        Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
          (Ideal.ResidueField
              (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
          ⊤
have₅ :
  ∀ (this_1 : IsArtinianRing (p.Fiber S)) (x : p.ResidueField ⊗[R] S)
    (hx0 :
      Ne.{u_3 + 1} (α := Q.ResidueField)
        (((TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
                p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
              (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
            x :
          Q.ResidueField)
        (0 : Q.ResidueField))
    (hx :
      Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
        p.ResidueField[(((TensorProduct.lift (ofId p.ResidueField Q.ResidueField)
                    (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯ :
                  p.ResidueField ⊗[R] S →ₐ[p.ResidueField] Q.ResidueField) :
                (a : p.ResidueField ⊗[R] S) → Q.ResidueField)
              x :
            Q.ResidueField)]
        ⊤),
    ∃ t ∉ Q,
      (∀ (Q' : Ideal S),
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
        Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
          (Ideal.ResidueField
              (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
          ⊤
have₆ :
  ∀ (this_1 : IsArtinianRing (p.Fiber S)) (x : p.ResidueField ⊗[R] S),
    let φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
      TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯;
    ∀
      (hx0 :
        Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
          (0 : Q.ResidueField))
      (hx :
        Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
          p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤),
      ∃ t ∉ Q,
        (∀ (Q' : Ideal S),
            Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
          Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
            (Ideal.ResidueField
                (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
            ⊤
⊢ ∃ t ∉ Q,
    (∀ (Q' : Ideal S),
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
      Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
        (Ideal.ResidueField
            (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
        ⊤
have have₇ : ∀ (this_1 : IsArtinianRing (p.Fiber S)),
  let α : (↑(p.primesOver S) : Type u_3) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p;
  ∀ (x : p.ResidueField ⊗[R] S),
    let φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
      TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) sorry;
    ∀
      (hx0 :
        Ne.{u_3 + 1} (α := Q.ResidueField) ((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)
          (0 : Q.ResidueField))
      (hx :
        Eq (α := Subalgebra.{u_1, u_3} p.ResidueField Q.ResidueField)
          p.ResidueField[((φ : (a : p.ResidueField ⊗[R] S) → Q.ResidueField) x : Q.ResidueField)] ⊤)
      (r : p.Fiber S)
      (hrQ :
        r ∉
          PrimeSpectrum.asIdeal
            ((α : (a : (↑(p.primesOver S) : Type u_3)) → PrimeSpectrum (p.Fiber S))
              (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) Q sorry)))
      (hrid : IsIdempotentElem r)
      (hr :
        ∀ (q : Ideal (p.Fiber S)),
          q.IsPrime →
            q ≠
                PrimeSpectrum.asIdeal
                  ((α : (a : (↑(p.primesOver S) : Type u_3)) → PrimeSpectrum (p.Fiber S))
                    (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (p.primesOver S) x) Q
                      sorry)) →
              r ∈ q),
      ∃ t ∉ Q,
        (∀ (Q' : Ideal S),
            Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q') ∧
          Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
            (Ideal.ResidueField
                (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
            ⊤
Tactic: classical
  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 _ _) _