-- 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₂
this :
  Eq.{u_3 + 1} (α := T) ((algebraMap R T : (a : R) → T) (y₁ * (↑s₂ : R)) : T)
      ((algebraMap R T : (a : R) → T) (y₂ * (↑s₁ : R)) : T) →
    ∃ (a : ↥N),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₁ * (↑s₂ : R))) : S)
        ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₂ * (↑s₁ : R))) : S)
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)
⊢ 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₁ : 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₂
Tactic: simp only [IsScalarTower.algebraMap_apply R S T, map_mul, ← e₁, ← e₂, ← mul_assoc,
        mul_right_comm _ (algebraMap R S s₂),
        (IsLocalization.map_units S s₁).mul_left_inj,
        (IsLocalization.map_units S s₂).mul_left_inj] at this
Cleared hypotheses: this