awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ (↑M₁ : Set R)
hy :
  HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T) =
    (algebraMap S₂ T : (a : S₂) → T)
      ((y,
            Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) m) ⋯) :
          S₂ × ↥(Algebra.algebraMapSubmonoid S₂ M₁)).1
z n : R
hn : n ∈ M₂
hz :
  HMul.hMul (β := S₂) y
      ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) =
    (algebraMap R S₂ : (a : R) → S₂) (z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).1
hunit : IsUnit.{u_4} (M := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁)
⊢ HMul.hMul (β := T)
      (HMul.hMul (β := T)
        (HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T))
        ((algebraMap S₂ T : (a : S₂) → T)
            ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) :
          T))
      ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T) =
    HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T) *
      HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T)
        ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ (↑M₁ : Set R)
hy :
  HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T) =
    (algebraMap S₂ T : (a : S₂) → T)
      ((y,
            Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) m) ⋯) :
          S₂ × ↥(Algebra.algebraMapSubmonoid S₂ M₁)).1
z n : R
hn : n ∈ M₂
hz :
  HMul.hMul (β := S₂) y
      ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) =
    (algebraMap R S₂ : (a : R) → S₂) (z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).1
hunit : IsUnit.{u_4} (M := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁)
⊢ HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T) =
    HMul.hMul (β := T)
      (HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T))
      ((algebraMap S₁ T : (a : S₁) → T)
          (HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) (↑hunit.unit⁻¹ : S₁)) :
        T)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
hxy : Eq.{u_6 + 1} (α := T) ((algebraMap S₁ T : (a : S₁) → T) x : T) ((algebraMap S₁ T : (a : S₁) → T) y : T)
obtain :
  ∀ (r s : R) (d : ↥M₁)
    (hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r)
    (hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s),
    ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y

Tactic:
obtain ⟨r, s, d, hr, hs⟩ := IsLocalization.surj₂ M₁ S₁ x y

Premises used: IsLocalization.surj₂
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
hxy : Eq.{u_6 + 1} (α := T) ((algebraMap S₁ T : (a : S₁) → T) x : T) ((algebraMap S₁ T : (a : S₁) → T) y : T)
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
⊢ HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) x : T)
      ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) : T) =
    HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) y : T)
      ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) : T)

Tactic:
apply_fun (· * algebraMap S₁ T (algebraMap R S₁ d)) at hxy

Premises used: HMul.hMul, Algebra.algebraMap, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) x : T)
      ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) : T) =
    HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) y : T)
      ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) : T)
⊢ Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)

Tactic:
simp_rw [← map_mul, hr, hs, ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R S₂ T] at hxy

Premises used: map_mul, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
obtain :
  ∀ (c : R) (hmc : c ∈ (↑M₁ : Set R))
    (hc :
      HMul.hMul (α := S₂) (β := S₂)
          ((↑(Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
                  ((algebraMap R S₂ : (a : R) → S₂) c) ⋯) :
              S₂) :
            S₂)
          ((algebraMap R S₂ : (a : R) → S₂) r : S₂) =
        HMul.hMul (α := S₂) (β := S₂)
          ((↑(Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
                  ((algebraMap R S₂ : (a : R) → S₂) c) ⋯) :
              S₂) :
            S₂)
          ((algebraMap R S₂ : (a : R) → S₂) s : S₂)),
    ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y

Tactic:
obtain ⟨⟨-, c, hmc, rfl⟩, hc⟩ := exists_of_eq (M := Algebra.algebraMapSubmonoid S₂ M₁) hxy

Premises used: IsLocalization.exists_of_eq, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  HMul.hMul (α := S₂) (β := S₂)
      ((↑(Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) c) ⋯) :
          S₂) :
        S₂)
      ((algebraMap R S₂ : (a : R) → S₂) r : S₂) =
    HMul.hMul (α := S₂) (β := S₂)
      ((↑(Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) c) ⋯) :
          S₂) :
        S₂)
      ((algebraMap R S₂ : (a : R) → S₂) s : S₂)
⊢ Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)

Tactic:
simp_rw [← map_mul] at hc

Premises used: map_mul
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
obtain :
  ∀ (a : ↥M₂) (ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)),
    ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y

Tactic:
obtain ⟨a, ha⟩ := IsLocalization.exists_of_eq (M := M₂) hc

Premises used: IsLocalization.exists_of_eq
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
a : ↥M₂
ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)
h :
  HMul.hMul (α := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      x =
    HMul.hMul (α := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      y
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y

Tactic:
use ⟨algebraMap R S₁ a, a, a.property, rfl⟩
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
a : ↥M₂
ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)
h :
  HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        x)
      ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) =
    HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        y)
      ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁)
⊢ HMul.hMul (α := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      x =
    HMul.hMul (α := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      y

Tactic:
apply (map_units S₁ d).mul_right_cancel

Premises used: IsLocalization.map_units, IsUnit.mul_right_cancel
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
a : ↥M₂
ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)
h :
  HMul.hMul (α := S₁) (β := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      ((algebraMap R S₁ : (a : R) → S₁) r : S₁) =
    HMul.hMul (α := S₁) (β := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      ((algebraMap R S₁ : (a : R) → S₁) s : S₁)
⊢ HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        x)
      ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) =
    HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        y)
      ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁)

Tactic:
rw [mul_assoc, hr, mul_assoc, hs]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
a : ↥M₂
ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)
h :
  HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁) (β := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        ((algebraMap R S₁ : (a : R) → S₁) r : S₁))
      ((algebraMap R S₁ : (a : R) → S₁) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M₁) c hmc) : R) : S₁) =
    HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁) (β := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        ((algebraMap R S₁ : (a : R) → S₁) s : S₁))
      ((algebraMap R S₁ : (a : R) → S₁) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M₁) c hmc) : R) : S₁)
⊢ HMul.hMul (α := S₁) (β := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      ((algebraMap R S₁ : (a : R) → S₁) r : S₁) =
    HMul.hMul (α := S₁) (β := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      ((algebraMap R S₁ : (a : R) → S₁) s : S₁)

Tactic:
apply (map_units S₁ ⟨c, hmc⟩).mul_right_cancel

Premises used: Subtype.mk, IsLocalization.map_units, IsUnit.mul_right_cancel