-- 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 :
  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
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    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))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1

Tactic:
refine ⟨⟨⟨_, hm₃s⟩, _, _, mul_mem hm₁ (mul_mem hm₂ hm₃), rfl⟩, ?_⟩