-- Module: Mathlib.RingTheory.Unramified.LocalRing
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
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
inst_5 : q.LiesOver p
H :
  Function.Injective.{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 R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S))),
    ∃ r ∉ p,
      ∀ (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'))
obtain₁ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p)),
    ∃ r ∉ p,
      ∀ (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'))
obtain₂ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0),
    ∃ r ∉ p,
      ∀ (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'))
obtain₃ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R))))),
    ∃ r ∉ p,
      ∀ (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'))
obtain₄ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' : R),
    (↑(∏ i : ↥s, m i) : 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'))
obtain₅ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1),
    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'))
obtain₆ obtain₇ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1) (x : Away r')
    (hx :
      Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (((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'))
            x :
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (0 : Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))),
    x = 0
obtain₈ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1) (x : R) (w : ↥(Submonoid.powers r'))
    (hx :
      Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (((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'))
            (IsLocalization.mk' (Away r') x w) :
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (0 : Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))),
    Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
obtain₉ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1) (x : R) (w : ↥(Submonoid.powers r'))
    (hx :
      ∃ (m : ↥(Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S)),
        HMul.hMul (β := S) (↑m : S) ((algebraMap R S : (a : R) → S) x : S) = 0),
    Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
obtain₁₀ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1) (x : R) (w : ↥(Submonoid.powers r')) (n : ℕ)
    (hn :
      HMul.hMul (β := S)
          (↑(Subtype.mk (p := fun (x : S) ↦
                Membership.mem (γ := Submonoid S) (Submonoid.powers ((algebraMap R S : (a : R) → S) r') : Submonoid S)
                  x)
                ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r' : S) x) n) ⋯) :
            S)
          ((algebraMap R S : (a : R) → S) x : S) =
        0),
    Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
obtain₁₁ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1) (x : R) (w : ↥(Submonoid.powers r')) (n : ℕ)
    (hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)),
    Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
obtain₁₂ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1) (x : R) (w : ↥(Submonoid.powers r')) (n : ℕ)
    (hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)) (k : ℕ)
    (hk :
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑(∏ i : ↥s, m i) : R)) x)
                ((fun (x : ℕ) ↦ HPow.hPow (α := R) (↑(∏ i : ↥s, m i) : R) x) k) ⋯) :
            R) *
          (r' ^ n * x) =
        0),
    Eq (α := Away r') (IsLocalization.mk' (Away r') x w) 0
obtain₁₃ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1) (x : R) (w : ↥(Submonoid.powers r')) (n : ℕ)
    (hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)) (k : ℕ)
    (hk :
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑(∏ i : ↥s, m i) : R)) x)
                ((fun (x : ℕ) ↦ HPow.hPow (α := R) (↑(∏ i : ↥s, m i) : R) x) k) ⋯) :
            R) *
          (r' ^ n * x) =
        0),
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
              ((fun (x : ℕ) ↦ r' ^ x) (k + n)) ⋯) :
          R) *
        x =
      0
obtain₁₄ :
  ∀ (s : Finset R) (hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) (RingHom.ker (F := R →+* S) (algebraMap R S)))
    (this :
      ∀ (x : ↥s),
        Eq (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x : R) : Localization.AtPrime p)
          (0 : Localization.AtPrime p))
    (m : (x : ↥s) → ↥p.primeCompl) (hm : ∀ (x : ↥s), (↑(m x) : R) * (↑x : R) = 0)
    (H :
      LE.le (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S))
        (RingHom.ker (F := R →+* Away (M := R) (↑(∏ i : ↥s, m i) : R))
          (algebraMap R (Away (M := R) (↑(∏ i : ↥s, m i) : R)))))
    (r' s_1 : R) (e : r' = (↑(∏ i : ↥s, m i) : R) * s_1) (x : R) (w : ↥(Submonoid.powers r')) (n : ℕ)
    (hn : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (r' ^ n * x) : S) (0 : S)) (k : ℕ)
    (hk : HPow.hPow (α := R) (↑(∏ i : ↥s, m i) : R) k * (r' ^ n * x) = 0), r' ^ (k + n) * x = 0
⊢ ∃ r ∉ p,
    ∀ (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'))

Tactic:
classical
  obtain ⟨s, hs⟩ := hRS
  have (x : s) : algebraMap R (Localization.AtPrime p) x.1 = 0 := by
    apply H
    simp [localRingHom_to_map, -FaithfulSMul.algebraMap_eq_zero_iff,
      show algebraMap R S _ = 0 from hs.le (Ideal.subset_span x.2)]
  choose m hm using fun x ↦ (IsLocalization.map_eq_zero_iff p.primeCompl _ _).mp (this x)
  have H : RingHom.ker (algebraMap R S) ≤ RingHom.ker
      (algebraMap R (Localization.Away (∏ i, m i).1)) := by
    rw [← hs, Ideal.span_le]
    intro x hxs
    refine (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mpr ⟨⟨_, 1, rfl⟩, ?_⟩
    simp only [pow_one]
    rw [Fintype.prod_eq_mul_prod_compl ⟨x, hxs⟩, Submonoid.coe_mul, mul_assoc, mul_left_comm, hm,
      mul_zero]
  refine ⟨_, (∏ i : s, m i).2, ?_⟩
  rintro r' ⟨s, e⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  obtain ⟨x, _, rfl⟩ := IsLocalization.exists_mk'_eq (.powers r') x
  simp only [awayMap, IsLocalization.Away.map, IsLocalization.map_mk',
    IsLocalization.mk'_eq_zero_iff] at hx
  obtain ⟨⟨_, n, rfl⟩, hn⟩ := hx
  simp only [← map_pow, ← map_mul] at hn
  obtain ⟨⟨_, k, rfl⟩, hk⟩ := (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mp (H hn)
  refine (IsLocalization.mk'_eq_zero_iff _ _).mpr ⟨⟨_, k + n, rfl⟩, ?_⟩
  dsimp only at hk ⊢
  rw [pow_add, mul_assoc, e, mul_pow, ← e, mul_assoc, mul_left_comm, hk, mul_zero]

Premises used: IsLocalization.map_mk', mul_assoc, pow_add, map_pow, mul_left_comm, MulZeroClass.mul_zero, map_mul, IsLocalization.Away.map, injective_iff_map_eq_zero, Localization.r', IsLocalization.mk'_eq_zero_iff, Localization.awayMap, mul_pow, rfl