awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T) = (algebraMap S T : (a : S) → T) y
z : R
t : ↥M
eq₂ : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑t : R) : S) = (algebraMap R S : (a : R) → S) z
z' : R
t' : ↥M
eq₃ : HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) = (algebraMap R S : (a : R) → S) z'
refine_1 :
  ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
      HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ z' * (↑t : R) ∈ localizationLocalizationSubmodule M N

Tactic:
rw [mem_localizationLocalizationSubmodule]

Premises used: IsLocalization.mem_localizationLocalizationSubmodule
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T) = (algebraMap S T : (a : S) → T) y
z : R
t : ↥M
eq₂ : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑t : R) : S) = (algebraMap R S : (a : R) → S) z
z' : R
t' : ↥M
eq₃ : HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) = (algebraMap R S : (a : R) → S) z'
⊢ ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
      HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)

Tactic:
⟨s, t * t', ?_⟩

Premises used: HMul.hMul, Exists.intro
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T) = (algebraMap S T : (a : S) → T) y
z : R
t : ↥M
eq₂ : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑t : R) : S) = (algebraMap R S : (a : R) → S) z
z' : R
t' : ↥M
eq₃ : HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) = (algebraMap R S : (a : R) → S) z'
refine_1 :
  (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
⊢ ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
      HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)

Tactic:
refine ⟨s, t * t', ?_⟩
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T) = (algebraMap S T : (a : S) → T) y
z : R
t : ↥M
eq₂ : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑t : R) : S) = (algebraMap R S : (a : R) → S) z
z' : R
t' : ↥M
eq₃ : HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) = (algebraMap R S : (a : R) → S) z'
refine_1 :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z' : S) ((algebraMap R S : (a : R) → S) (↑t : R) : S) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
refine_1₁ :
  HMul.hMul (β := S) (HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S))
      ((algebraMap R S : (a : R) → S) (↑t : R) : S) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
refine_1₂ :
  (↑s : S) *
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S)
        ((algebraMap R S : (a : R) → S) (↑t : R) : S) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
refine_1₃ :
  HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) ((↑t' : R) * (↑t : R)) : S) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
refine_1₄ :
  HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) ((↑t' : R) * (↑t : R)) : S) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t' * t) : R) : S)
refine_1₅ refine_1₆ :
  HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) ((↑t' : R) * (↑t : R)) : S) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) ((↑t' : R) * (↑t : R)) : S)
⊢ (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)

Tactic:
rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]

Premises used: mul_assoc, map_mul, mul_comm, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T) = (algebraMap S T : (a : S) → T) y
z : R
t : ↥M
eq₂ : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑t : R) : S) = (algebraMap R S : (a : R) → S) z
z' : R
t' : ↥M
eq₃ : HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) = (algebraMap R S : (a : R) → S) z'
refine_2 :
  x *
      HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) (↑s : S) : T)
          ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) : T))
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑t : R) : S) : T) =
    HMul.hMul (β := T)
      (HMul.hMul (β := T) (HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T))
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑t : R) : S) : T))
      ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) : T)
⊢ HMul.hMul (β := T) x
      ((algebraMap R T : (a : R) → T)
          (↑(z * (↑t' : R),
                  Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) (z' * (↑t : R)) ⋯).2 :
            R) :
        T) =
    (algebraMap R T : (a : R) → T)
      (z * (↑t' : R), Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) (z' * (↑t : R)) ⋯).1

Tactic:
simp only [map_mul, IsScalarTower.algebraMap_apply R S T, ← eq₃, ← eq₂, ← eq₁]

Premises used: map_mul, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T) = (algebraMap S T : (a : S) → T) y
z : R
t : ↥M
eq₂ : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑t : R) : S) = (algebraMap R S : (a : R) → S) z
z' : R
t' : ↥M
eq₃ : HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) = (algebraMap R S : (a : R) → S) z'
⊢ x *
      HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) (↑s : S) : T)
          ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) : T))
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑t : R) : S) : T) =
    HMul.hMul (β := T)
      (HMul.hMul (β := T) (HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T))
        ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑t : R) : S) : T))
      ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) : T)

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
rw :
  (∃ (c : ↥N),
      HMul.hMul (β := S) (↑c : S) ((algebraMap R S : (a : R) → S) x : S) =
        HMul.hMul (β := S) (↑c : S) ((algebraMap R S : (a : R) → S) y : S)) →
    ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap R T : (a : R) → T) x : T) ((algebraMap R T : (a : R) → T) y : T) →
    ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y

Tactic:
rw [IsScalarTower.algebraMap_apply R S T, IsScalarTower.algebraMap_apply R S T,
    IsLocalization.eq_iff_exists N T]

Premises used: IsScalarTower.algebraMap_apply, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
rcases :
  ∀ (z' : R) (s : ↥M)
    (eq₂ :
      HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(z', s).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (z', s).1),
    ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y
⊢ ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y

Tactic:
rcases IsLocalization.surj M (z : S) with ⟨⟨z', s⟩, eq₂⟩

Premises used: IsLocalization.surj, Subtype.val
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
obtain :
  ∀ (c : ↥M) (eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')),
    ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y
⊢ ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y

Tactic:
obtain ⟨c, eq₃ : ↑c * (x * z') = ↑c * (y * z')⟩ := (IsLocalization.eq_iff_exists M S).mp this

Premises used: HMul.hMul, Iff.mp, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
c : ↥M
eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')
⊢ ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y

Tactic:
⟨⟨c * z', ?_⟩, ?_⟩

Premises used: HMul.hMul, Subtype.mk, Exists.intro, Subtype.val
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
c : ↥M
eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')
refine_1 : (↑c : R) * z' ∈ localizationLocalizationSubmodule M N
refine_2 :
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
⊢ ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y

Tactic:
refine ⟨⟨c * z', ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
c : ↥M
eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')
refine_1 :
  ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
      HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ (↑c : R) * z' ∈ localizationLocalizationSubmodule M N

Tactic:
rw [mem_localizationLocalizationSubmodule]

Premises used: IsLocalization.mem_localizationLocalizationSubmodule
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
c : ↥M
eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')
⊢ ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
      HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)

Tactic:
⟨z, c * s, ?_⟩

Premises used: HMul.hMul, Exists.intro
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
c : ↥M
eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')
refine_1 :
  (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)
⊢ ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
      HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)

Tactic:
refine ⟨z, c * s, ?_⟩
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
c : ↥M
eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')
refine_1 :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑c : R) : S) ((algebraMap R S : (a : R) → S) z' : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)
refine_1₁ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑c : R) : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)
refine_1₂ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑c : R) : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) ((↑c : R) * (↑s : R)) : S)
refine_1₃ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑c : R) : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    (↑z : S) *
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑c : R) : S)
        ((algebraMap R S : (a : R) → S) (↑s : R) : S)
refine_1₄ refine_1₅ :
  (↑z : S) *
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑c : R) : S)
        ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    (↑z : S) *
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑c : R) : S)
        ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)

Tactic:
rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]

Premises used: mul_left_comm, map_mul, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
this : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
c : ↥M
eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')
refine_2 :
  ∀ (eq₃ : (↑c : R) * (z' * x) = (↑c : R) * (y * z')),
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
refine_2₁ :
  ∀ (eq₃ : (↑c : R) * (z' * x) = (↑c : R) * (z' * y)),
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
refine_2₂ :
  ∀ (eq₃ : (↑c : R) * z' * x = (↑c : R) * (z' * y)),
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
refine_2₃ refine_2₄ refine_2₅ refine_2₆ :
  ∀ (eq₃ : (↑c : R) * z' * x = (↑c : R) * z' * y),
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') ⋯) : R) * y

Tactic:
rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
suffices :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)
⊢ ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y

Tactic:
suffices (algebraMap R S) (x * z' : R) = (algebraMap R S) (y * z') by
    obtain ⟨c, eq₃ : ↑c * (x * z') = ↑c * (y * z')⟩ := (IsLocalization.eq_iff_exists M S).mp this
    refine ⟨⟨c * z', ?_⟩, ?_⟩
    · rw [mem_localizationLocalizationSubmodule]
      refine ⟨z, c * s, ?_⟩
      rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
    · rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃