-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
a : S
ha : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a
b : S
hb : Membership.mem (γ := Subalgebra R S) (integralClosure R S) b
e :
  Eq.{u_6 + 1} (α := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
      ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
      ↥(integralClosure Rf Sf))
this_1 :
  Eq (α := Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
          ↥(integralClosure Rf Sf)) :
      Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
          ↥(integralClosure Rf Sf)) :
      Sf)
this : Eq.{u_6 + 1} (α := Sf) ((algebraMap S Sf : (a : S) → Sf) a : Sf) ((algebraMap S Sf : (a : S) → Sf) b : Sf)
refine_3 :
  ∀ (m : R) (hm : m ∈ (↑M : Set R))
    (h :
      HMul.hMul (α := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                  ((algebraMap R S : (a : R) → S) m) ⋯) :
              S) :
            S)
          a =
        HMul.hMul (α := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                  ((algebraMap R S : (a : R) → S) m) ⋯) :
              S) :
            S)
          b),
    ∃ (c : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
      (↑c : ↥(integralClosure R S)) *
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha =
        (↑c : ↥(integralClosure R S)) *
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    (↑c : ↥(integralClosure R S)) *
        Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha =
      (↑c : ↥(integralClosure R S)) *
        Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb

Tactic:
obtain ⟨⟨_, m, hm, rfl⟩, h⟩ :=
      (IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S M) _).mp this

Premises used: Iff.mp, Algebra.algebraMapSubmonoid, rfl, IsLocalization.eq_iff_exists