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
x : R
⊢ x ∈ localizationLocalizationSubmodule M N ↔
    ∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
have rw : (∃ y ∈ N,
    ∃ (z : S),
      Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
        y * z = (algebraMap R S : (a : R) → S) x) ↔
  ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
Tactic: rw [localizationLocalizationSubmodule, Submonoid.mem_comap, Submonoid.mem_sup]
-- 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
x : R
⊢ (∃ y ∈ N,
      ∃ (z : S),
        Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
          y * z = (algebraMap R S : (a : R) → S) x) ↔
    ∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
have mp : (∃ y ∈ N,
    ∃ (z : S),
      Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
        y * z = (algebraMap R S : (a : R) → S) x) →
  ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
Tactic: constructor
-- 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
x : R
mp :
  (∃ y ∈ N,
      ∃ (z : S),
        Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
          y * z = (algebraMap R S : (a : R) → S) x) →
    ∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ (∃ y ∈ N,
      ∃ (z : S),
        Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
          y * z = (algebraMap R S : (a : R) → S) x) ↔
    ∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
have mpr : (∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)) →
  ∃ y ∈ N,
    ∃ (z : S),
      Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
        y * z = (algebraMap R S : (a : R) → S) x
Tactic: constructor
-- 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
y : ↥(localizationLocalizationSubmodule M N)
⊢ IsUnit.{u_3} (M := T) ((algebraMap R T : (a : R) → T) (↑y : R) : T)
have obtain : ∀ (y' : ↥N) (z : ↥M)
  (eq :
    (algebraMap R S : (a : R) → S) (↑y : R) =
      HMul.hMul (β := S) (↑y' : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)),
  IsUnit.{u_3} (M := T) ((algebraMap R T : (a : R) → T) (↑y : R) : T)
Tactic: obtain ⟨y', z, eq⟩ := mem_localizationLocalizationSubmodule.mp y.prop
-- 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
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq :
  (algebraMap R S : (a : R) → S) (↑y : R) = HMul.hMul (β := S) (↑y' : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ IsUnit.{u_3} (M := T) ((algebraMap R T : (a : R) → T) (↑y : R) : T)
have rw : IsUnit.{u_3} (M := T) ((algebraMap S T : (a : S) → T) (↑y' : S) : T) ∧
  IsUnit.{u_3} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑z : R) : S) : T)
Tactic: rw [IsScalarTower.algebraMap_apply R S T, eq, map_mul, IsUnit.mul_iff]
-- 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 : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
have rcases : ∀ (y : S) (s : ↥N)
  (eq₁ :
    HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑(y, s).2 : S) : T) =
      (algebraMap S T : (a : S) → T) (y, s).1),
  ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
Tactic: rcases IsLocalization.surj N x with ⟨⟨y, 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 : T
y : S
s : ↥N
eq₁ :
  HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑(y, s).2 : S) : T) = (algebraMap S T : (a : S) → T) (y, s).1
⊢ ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
have rcases : ∀ (z : R) (t : ↥M)
  (eq₂ :
    HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(z, t).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (z, t).1),
  ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
Tactic: rcases IsLocalization.surj M y with ⟨⟨z, t⟩, 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 : T
y : S
s : ↥N
eq₁ :
  HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑(y, s).2 : S) : T) = (algebraMap S T : (a : S) → T) (y, s).1
z : R
t : ↥M
eq₂ :
  HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(z, t).2 : R) : S) = (algebraMap R S : (a : R) → S) (z, t).1
⊢ ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
have rcases : ∀ (z' : R) (t' : ↥M)
  (eq₃ :
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(z', t').2 : R) : S) =
      (algebraMap R S : (a : R) → S) (z', t').1),
  ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
Tactic: rcases IsLocalization.surj M (s : S) with ⟨⟨z', t'⟩, 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 : 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 : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
have refine_1 : z' * (↑t : R) ∈ localizationLocalizationSubmodule M N
Tactic: refine ⟨⟨z * t', z' * 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 : 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 : z' * (↑t : R) ∈ localizationLocalizationSubmodule M N
⊢ ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
have refine_2 : 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)) sorry).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)) sorry).1
Tactic: refine ⟨⟨z * t', z' * 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 : 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'
⊢ z' * (↑t : R) ∈ localizationLocalizationSubmodule M N
have 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)
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 : 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)
have 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)
Tactic: refine ⟨s, t * 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 : 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'
⊢ (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]
-- 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'
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)
⊢ (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]
-- 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'
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)
⊢ (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]
-- 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'
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)
⊢ (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]
-- 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'
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)
⊢ (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]
-- 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'
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)
⊢ (algebraMap R S : (a : R) → S) (z' * (↑t : R)) =
    HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(t * t') : R) : S)
have 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)
Tactic: rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]