-- 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)
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

Tactic:
⟨⟨_, m, hm, rfl⟩, FaithfulSMul.algebraMap_injective (integralClosure R S) S ?_⟩

Premises used: Membership.mem, Subtype, Subtype.mk, integralClosure, FaithfulSMul.algebraMap_injective, And.intro, Exists.intro, rfl