-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
obtain :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤),
    ∃ r ∉ p,
      ∀ (r' : R),
        r ∣ r' →
          Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
obtain₁ :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤)
    (this :
      ∀ (x : S),
        ∃ (a : R),
          ∃ b ∉ p, (algebraMap R S : (a : R) → S) a = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) b : S)),
    ∃ r ∉ p,
      ∀ (r' : R),
        r ∣ r' →
          Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
obtain₂ :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤) (a b : (x : S) → R)
    (hbp : ∀ (x : S), b x ∉ p)
    (e :
      ∀ (x : S),
        (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)),
    ∃ r ∉ p,
      ∀ (r' : R),
        r ∣ r' →
          Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
obtain₃ :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤) (a b : (x : S) → R)
    (hbp : ∀ (x : S), b x ∉ p)
    (e :
      ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S))
    (r : R) (hrp : r ∉ p)
    (hr :
      ∀ (r' : R),
        r ∣ r' →
          Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))),
    ∃ r ∉ p,
      ∀ (r' : R),
        r ∣ r' →
          Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
obtain₄ :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤) (a b : (x : S) → R)
    (hbp : ∀ (x : S), b x ∉ p)
    (e :
      ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S))
    (r : R) (hrp : r ∉ p)
    (hr :
      ∀ (r' : R),
        r ∣ r' →
          Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r')))
    (r' : R),
    r * ∏ i ∈ s, b i ∣ r' →
      Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
obtain₅ :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤) (a b : (x : S) → R)
    (hbp : ∀ (x : S), b x ∉ p)
    (e :
      ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S))
    (r : R) (hrp : r ∉ p)
    (hr :
      ∀ (r' : R),
        r ∣ r' →
          Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r')))
    (r' : R) (hr' : r * ∏ i ∈ s, b i ∣ r'),
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
obtain₆ :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤) (a b : (x : S) → R)
    (hbp : ∀ (x : S), b x ∉ p)
    (e :
      ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S))
    (r : R) (hrp : r ∉ p)
    (hr :
      ∀ (r' : R),
        r ∣ r' →
          Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
            Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
            (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r')))
    (r' : R) (hr' : r * ∏ i ∈ s, b i ∣ r')
    (H :
      LE.le (α := Subalgebra R (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
        (AlgHom.range (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))))
        (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))),
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
have obtain₇ : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤) (a b : (x : S) → R)
  (hbp : ∀ (x : S), b x ∉ p)
  (e :
    ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S))
  (r : R) (hrp : r ∉ p)
  (hr :
    ∀ (r' : R),
      r ∣ r' →
        Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r')))
  (r' : R) (hr' : r * ∏ i ∈ s, b i ∣ r')
  (H :
    LE.le (α := Subalgebra R (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
      (AlgHom.range (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))))
      (AlgHom.range (awayMapₐ (Algebra.ofId R S) r')))
  (x : Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)),
  ∃ (a : Away r'),
    ((awayMap (algebraMap R S) r' :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
        a =
      x
Tactic: classical
  obtain ⟨s, hs⟩ := Algebra.FiniteType.out (R := R) (A := S)
  have (x : S) : ∃ a, ∃ b ∉ p, algebraMap R S a = x * algebraMap R S b := by
    have := (IsLocalization.mk'_surjective p.primeCompl).exists.mp (H.2 (algebraMap _ _ x))
    simp only [localRingHom_mk', Prod.exists, Subtype.exists, Ideal.mem_primeCompl_iff,
      IsLocalization.mk'_eq_iff_eq_mul, exists_prop, ← map_mul,
      IsLocalization.eq_iff_exists q.primeCompl] at this
    obtain ⟨a, b, hbp, c, hcq, hc⟩ := this
    obtain ⟨d, hd, e, he⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hcq
    exact ⟨d * a, d * b, ‹p.IsPrime›.mul_notMem hd hbp, by grind⟩
  choose a b hbp e using this
  obtain ⟨r, hrp, hr⟩ := Localization.exists_awayMap_injective_of_localRingHom_injective hRS H.1
  refine ⟨r * ∏ i ∈ s, b i, mul_mem (s := p.primeCompl) hrp (prod_mem fun _ _ ↦ hbp _), ?_⟩
  refine fun r' hr' ↦ ⟨hr _ (.trans ⟨_, rfl⟩ hr'), ?_⟩
  have H : (IsScalarTower.toAlgHom R S _).range ≤ (awayMapₐ (Algebra.ofId R S) r').range := by
    rw [← Algebra.map_top, Subalgebra.map_le, ← hs, Algebra.adjoin_le_iff]
    intro x hxs
    obtain ⟨r'', hr'⟩ := hr'
    refine ⟨IsLocalization.mk' (M := .powers r') _
      (r'' * r * (∏ i ∈ s.erase x, b i) * a x) ⟨_, 1, rfl⟩, ?_⟩
    dsimp [awayMapₐ, IsLocalization.Away.map]
    simp only [pow_one, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul,
      ← map_mul (algebraMap S _), map_mul (algebraMap R _), e]
    congr 1
    rw [hr', ← Finset.prod_erase_mul s b hxs, map_mul, map_mul, map_mul]
    ring_nf
  intro x
  obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers (algebraMap R S r')) x
  obtain ⟨y, hy : awayMap _ _ _ = _⟩ := H ⟨x, rfl⟩
  dsimp at hy
  refine ⟨y * Localization.Away.invSelf _ ^ n, ?_⟩
  simp only [map_mul, hy]
  simp [Away.invSelf, Localization.mk_eq_mk', awayMap, IsLocalization.Away.map,
    IsLocalization.map_mk', ← Algebra.smul_def, IsLocalization.smul_mk', ← IsLocalization.mk'_pow]