-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) = (algebraMap R S : (a : R) → S) y₁
y₂ : R
s₂ : ↥M
e₂ : HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) = (algebraMap R S : (a : R) → S) y₂
h₁ :
  HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T) ↔
    Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T)
h₂ :
  HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
          ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T))
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) : T) =
      HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
          ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T))
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) : T) ↔
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T)
this :
  HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
          ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T))
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) : T) =
      HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
          ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T))
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) : T) →
    ∃ (a : ↥N),
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₁ =
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₂
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (a : (↑(↑N : Set R) : Type u_1)),
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₁ =
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₂
have this₁ : Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
  ∃ (a : ↥N),
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₁ =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₂
Tactic: rw [h₂, h₁] at this
Cleared hypotheses: this