awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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) (↑(y₁, s₁).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (y₁, s₁).1
y₂ : R
s₂ : ↥M
e₂ :
  HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑(y₂, s₂).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (y₂, s₂).1
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂

Tactic:
(Set.exists_image_iff (algebraMap R S) N fun c => c * x₁ = c * x₂).mpr.comp ?_

Premises used: Iff.mpr, HMul.hMul, Algebra.algebraMap, Set.Mem, setOf, Function.comp, SetLike.coe, Set.image, Set.exists_image_iff, Eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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) (↑(y₁, s₁).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (y₁, s₁).1
y₂ : R
s₂ : ↥M
e₂ :
  HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑(y₂, s₂).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (y₂, s₂).1
refine :
  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₂
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂

Tactic:
refine (Set.exists_image_iff (algebraMap R S) N fun c => c * x₁ = c * x₂).mpr.comp ?_

Premises used: Iff.mpr, HMul.hMul, Algebra.algebraMap, Function.comp, SetLike.coe, Set.exists_image_iff, Eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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)
⊢ HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) ↔
    Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T)

Tactic:
have h₁ := @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂)
        (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) ↔
    Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T)
⊢ HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
          ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T))
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₂ : R) ⋯) : R) : T) =
      HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
          ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T))
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₂ : R) ⋯) : R) : T) ↔
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T) ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T)

Tactic:
have h₂ := @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
        ((algebraMap S T x₂) * (algebraMap R T s₁))
        (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : 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 R T : (a : R) → T) (↑s₁ : R) : T))
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₂ : R) ⋯) : R) : T) =
      HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
          ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T))
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₂ : R) ⋯) : R) : T) ↔
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T) ((algebraMap R T : (a : R) → T) (↑s₁ : R) : 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)

Tactic:
simp only [IsScalarTower.algebraMap_apply R S T] at h₁ h₂

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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),
      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
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 :
  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₂
⊢ 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₂

Tactic:
simpa only [mul_comm] using this

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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₂
suffices :
  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)
⊢ 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₂

Tactic:
suffices algebraMap R T (y₁ * s₂) = algebraMap R T (y₂ * s₁) →
        ∃ a : N, algebraMap R S (a * (y₁ * s₂)) = algebraMap R S (a * (y₂ * s₁)) by
      have h₁ := @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂)
        (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)
      have h₂ := @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
        ((algebraMap S T x₂) * (algebraMap R T s₁))
        (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)
      simp only [IsScalarTower.algebraMap_apply R S T] at h₁ h₂
      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
      rw [h₂, h₁] at this
      simpa only [mul_comm] using this
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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₂
simp_rw :
  (∃ (c : ↥N), (↑c : R) * (y₁ * (↑s₂ : R)) = (↑c : R) * (y₂ * (↑s₁ : R))) →
    ∃ (a : ↥N) (c : ↥M), (↑c : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑c : R) * ((↑a : R) * (y₂ * (↑s₁ : R)))
⊢ 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)

Tactic:
simp_rw [IsLocalization.eq_iff_exists N T, IsLocalization.eq_iff_exists M S]

Premises used: IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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₂
a : ↥N
e : (↑a : R) * (y₁ * (↑s₂ : R)) = (↑a : R) * (y₂ * (↑s₁ : R))
⊢ (↑a : R) * (y₁ * (↑s₂ : R)) = (↑a : R) * (y₂ * (↑s₁ : R))

Tactic:
e
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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₂
a : ↥N
e : (↑a : R) * (y₁ * (↑s₂ : R)) = (↑a : R) * (y₂ * (↑s₁ : R))
h₁ : (↑1 : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑a : R) * (y₁ * (↑s₂ : R))
h₂ : (↑1 : R) * ((↑a : R) * (y₂ * (↑s₁ : R))) = (↑a : R) * (y₂ * (↑s₁ : R))
⊢ (↑1 : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑1 : R) * ((↑a : R) * (y₂ * (↑s₁ : R)))

Tactic:
convert! e using 1
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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₂
a : ↥N
e : (↑a : R) * (y₁ * (↑s₂ : R)) = (↑a : R) * (y₂ * (↑s₁ : R))
⊢ (↑1 : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑a : R) * (y₁ * (↑s₂ : R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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₂
a : ↥N
e : (↑a : R) * (y₁ * (↑s₂ : R)) = (↑a : R) * (y₂ * (↑s₁ : R))
⊢ (↑1 : R) * ((↑a : R) * (y₂ * (↑s₁ : R))) = (↑a : R) * (y₂ * (↑s₁ : R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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₂
a : ↥N
e : (↑a : R) * (y₁ * (↑s₂ : R)) = (↑a : R) * (y₂ * (↑s₁ : R))
⊢ ∃ (a : ↥N) (c : ↥M), (↑c : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑c : R) * ((↑a : R) * (y₂ * (↑s₁ : R)))

Tactic:
exact ⟨a, 1, by convert! e using 1 <;> simp⟩
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
y : ↥N
obtain : ∀ (m : R) (hm : m * (↑y : R) ∈ M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)

Tactic:
obtain ⟨m, hm⟩ := h' y
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
y : ↥N
m : R
hm : m * (↑y : R) ∈ M
⊢ IsUnit.{u_2} (M := S)
    ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) (m * (↑y : R)) hm) : R) : S)

Tactic:
have := IsLocalization.map_units S ⟨_, hm⟩
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
y : ↥N
m : R
hm : m * (↑y : R) ∈ M
this :
  IsUnit.{u_2} (M := S)
    ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) (m * (↑y : R)) hm) : R) : S)
⊢ IsUnit
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) m : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S))

Tactic:
rw [map_mul] at this

Premises used: map_mul