-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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)
⊢ ∃ (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
have 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₃))) sorry).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₃))) sorry) :
        ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)).1
Tactic: refine ⟨⟨⟨_, hm₃s⟩, _, _, mul_mem hm₁ (mul_mem hm₂ hm₃), rfl⟩, ?_⟩