awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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'
⊢ 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
have 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)
Tactic: simp only [map_mul, IsScalarTower.algebraMap_apply R S T, ← eq₃, ← eq₂, ← eq₁]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
⊢ 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
have 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
Tactic: rw [IsScalarTower.algebraMap_apply R S T, IsScalarTower.algebraMap_apply R S T,
    IsLocalization.eq_iff_exists N T]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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)
⊢ ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y
have 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
Tactic: rcases IsLocalization.surj M (z : S) with ⟨⟨z', s⟩, eq₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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 : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y
have obtain : ∀ (c : ↥M) (eq₃ : (↑c : R) * (x * z') = (↑c : R) * (y * z')),
  ∃ (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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
have refine_1 : (↑c : R) * z' ∈ localizationLocalizationSubmodule M N
Tactic: refine ⟨⟨c * z', ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
⊢ ∃ (c : ↥(localizationLocalizationSubmodule M N)), (↑c : R) * x = (↑c : R) * y
have refine_2 : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * x =
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * y
Tactic: refine ⟨⟨c * z', ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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 : R) * z' ∈ localizationLocalizationSubmodule M N
have 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)
Tactic: rw [mem_localizationLocalizationSubmodule]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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)
have 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)
Tactic: refine ⟨z, c * s, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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')
⊢ (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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)
⊢ (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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)
⊢ (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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)
⊢ (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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)
⊢ (algebraMap R S : (a : R) → S) ((↑c : R) * z') =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑(c * s) : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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')
⊢ (↑(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
have refine_2 : ∀ (eq₃ : (↑c : R) * (z' * x) = (↑c : R) * (y * z')),
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * y
Tactic: rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃
Cleared hypotheses: eq₃
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
⊢ (↑(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
have refine_2₁ : ∀ (eq₃ : (↑c : R) * (z' * x) = (↑c : R) * (z' * y)),
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * y
Tactic: rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃
Cleared hypotheses: eq₃
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
⊢ (↑(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
have refine_2₂ : ∀ (eq₃ : (↑c : R) * z' * x = (↑c : R) * (z' * y)),
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) ((↑c : R) * z') sorry) : R) * y
Tactic: rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃
Cleared hypotheses: eq₃