-- 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)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
m₃ : R
hm₃ : m₃ ∈ M
hm₃s : IsIntegral R (m₃ • m₂ • x)
refine_2 :
  Eq (α := Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        (HMul.hMul (β := ↥(integralClosure Rf Sf))
          (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
          ((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)
                        (m₃ • m₂ • x) hm₃s,
                      Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
                        Membership.mem (γ := Submonoid ↥(integralClosure R S))
                          (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
                        ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) (m₁ * (m₂ * m₃)))
                        ⋯).2 :
                ↥(integralClosure R S)) :
            ↥(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) (m₃ • m₂ • x)
                    hm₃s,
                  Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
                    Membership.mem (γ := Submonoid ↥(integralClosure R S))
                      (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
                    ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) (m₁ * (m₂ * m₃))) ⋯) :
                ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)).1 :
          ↥(integralClosure Rf Sf)) :
      Sf)
⊢ HMul.hMul (β := ↥(integralClosure Rf Sf))
      (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
      ((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) (m₃ • m₂ • x)
                    hm₃s,
                  Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
                    Membership.mem (γ := Submonoid ↥(integralClosure R S))
                      (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
                    ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) (m₁ * (m₂ * m₃))) ⋯).2 :
            ↥(integralClosure R S)) :
        ↥(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) (m₃ • m₂ • x) hm₃s,
            Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
              Membership.mem (γ := Submonoid ↥(integralClosure R S))
                (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
              ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) (m₁ * (m₂ * m₃))) ⋯) :
          ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)).1

Tactic:
apply (FaithfulSMul.algebraMap_injective (integralClosure Rf Sf) Sf)

Premises used: Membership.mem, Subtype, integralClosure, FaithfulSMul.algebraMap_injective