awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
    ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y

Tactic:
IsLocalization'.toIsLocalizationMap.exists_of_eq

Premises used: Set.Mem, Submonoid.IsLocalizationMap.exists_of_eq, IsLocalization'.toIsLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
⊢ Bijective (β := S) fun (s : S) ↦ m • s

Tactic:
simpa only [Submonoid.smul_def, Algebra.smul_def] using (map_units S m).smul_bijective

Premises used: Submonoid.smul_def, IsLocalization.map_units, IsUnit.smul_bijective, Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ Eq (α := R →* S) (Submonoid.LocalizationMap.toMonoidHom (toLocalizationMap M S))
    (↑(↑(algebraMap R S) : R →*₀ S) : R →* S)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ Eq (α := (a : R) → S) (⇑(toLocalizationMap M S) : (a : R) → S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
⊢ Eq.{u_2 + 1} (α := S) ((toLocalizationMap M S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ ∀ (z w : S),
    ∃ (z' : R) (w' : R) (d : ↥M),
      HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑d : R) : S) = (algebraMap R S : (a : R) → S) z' ∧
        HMul.hMul (β := S) w ((algebraMap R S : (a : R) → S) (↑d : R) : S) = (algebraMap R S : (a : R) → S) w'

Tactic:
(toLocalizationMap M S).surj₂

Premises used: Set.Mem, IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.surj₂
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
    ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y

Tactic:
(toLocalizationMap M S).eq_iff_exists

Premises used: Set.Mem, Submonoid.LocalizationMap.eq_iff_exists, IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S) ↔ ∀ (c : ↥M), IsRegular (↑c : R)

Tactic:
(toLocalizationMap M S).injective_iff.trans <| .symm Subtype.forall

Premises used: Submonoid.LocalizationMap.injective_iff, Subtype.forall, IsLocalization.toLocalizationMap, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
x y : R
rw : (∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y) → ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * y
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
    ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * y

Tactic:
rw [IsLocalization.eq_iff_exists M]

Premises used: IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
x y : R
c : ↥M
hc : (↑c : R) * x = (↑c : R) * y
⊢ ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * y

Tactic:
⟨⟨c, h₁ c.2⟩, hc⟩

Premises used: Subtype.mk, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
x y : R
c : ↥M
hc : (↑c : R) * x = (↑c : R) * y
⊢ ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * y

Tactic:
exact ⟨⟨c, h₁ c.2⟩, hc⟩
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m
⊢ IsLocalization N S

Tactic:
of_le M N h₁ fun n hn ↦ have ⟨m, hm, dvd⟩ := h₂ n hn
    isUnit_of_dvd_unit (map_dvd _ dvd) (map_units S ⟨m, hm⟩)

Premises used: Algebra.algebraMap, isUnit_of_dvd_unit, IsUnit, Subtype.mk, map_dvd, _private.0.IsLocalization.of_le_of_exists_dvd.match_1, IsLocalization.map_units, IsLocalization.of_le, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S) ↔ ∃ m ∈ M, x ∣ m

Tactic:
⟨fun h ↦ ?_, fun ⟨m, hm, dvd⟩ ↦ isUnit_of_dvd_unit (map_dvd _ dvd) (map_units S ⟨m, hm⟩)⟩

Premises used: Algebra.algebraMap, isUnit_of_dvd_unit, IsUnit, Subtype.mk, map_dvd, Iff.intro, _private.0.IsLocalization.of_le_of_exists_dvd.match_1, IsLocalization.map_units, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
refine : ∀ (h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)), ∃ m ∈ M, x ∣ m
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S) ↔ ∃ m ∈ M, x ∣ m

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨m, hm, dvd⟩ ↦ isUnit_of_dvd_unit (map_dvd _ dvd) (map_units S ⟨m, hm⟩)⟩
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
have : ∀ (s : S) (hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s), ∃ m ∈ M, x ∣ m
⊢ ∃ m ∈ M, x ∣ m

Tactic:
have ⟨s, hxs⟩ := isUnit_iff_dvd_one.mp h
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
have :
  ∀ (r : R) (m : ↥M)
    (hrm :
      HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (r, m).1),
    ∃ m ∈ M, x ∣ m
⊢ ∃ m ∈ M, x ∣ m

Tactic:
have ⟨⟨r, m⟩, hrm⟩ := surj M s
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
r : R
m : ↥M
hrm :
  HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) (r, m).1 : S)

Tactic:
apply_fun (algebraMap R S x * ·) at hrm

Premises used: HMul.hMul, Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
r : R
m : ↥M
hrm :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) (r, m).1 : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)
    ((algebraMap R S : (a : R) → S) (x * (r, m).1) : S)

Tactic:
rw [← mul_assoc, ← hxs, one_mul, ← map_mul] at hrm

Premises used: mul_assoc, map_mul, one_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
r : R
m : ↥M
hrm :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)
    ((algebraMap R S : (a : R) → S) (x * (r, m).1) : S)
have : ∀ (m' : ↥M) (eq : (↑m' : R) * (↑(r, m).2 : R) = (↑m' : R) * (x * (r, m).1)), ∃ m ∈ M, x ∣ m
⊢ ∃ m ∈ M, x ∣ m

Tactic:
have ⟨m', eq⟩ := (eq_iff_exists M S).mp hrm
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
r : R
m : ↥M
hrm :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)
    ((algebraMap R S : (a : R) → S) (x * (r, m).1) : S)
m' : ↥M
eq : (↑m' : R) * (↑(r, m).2 : R) = (↑m' : R) * (x * (r, m).1)
⊢ ∃ m ∈ M, x ∣ m

Tactic:
⟨m' * m, mul_mem m'.2 m.2, _, mul_left_comm _ x _ ▸ eq⟩

Premises used: HMul.hMul, And.intro, Exists.intro, Subtype.val, Subtype.property, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
r : R
m : ↥M
hrm :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)
    ((algebraMap R S : (a : R) → S) (x * (r, m).1) : S)
m' : ↥M
eq : (↑m' : R) * (↑(r, m).2 : R) = (↑m' : R) * (x * (r, m).1)
⊢ ∃ m ∈ M, x ∣ m

Tactic:
exact ⟨m' * m, mul_mem m'.2 m.2, _, mul_left_comm _ x _ ▸ eq⟩
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ Submonoid.LocalizationMap.sec (toLocalizationMap M S) = sec M

Tactic:
rfl

Premises used: IsLocalization.sec, Set.Mem, rfl
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
⊢ HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(sec M z).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (sec M z).1

Tactic:
Classical.choose_spec <| IsLocalization.surj _ z

Premises used: IsLocalization.surj, Classical.choose_spec
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
rw :
  (algebraMap R S : (a : R) → S) (sec M z).1 =
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(sec M z).2 : R) : S)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (sec M z).1 : S)
    ((algebraMap R S : (a : R) → S) (sec M z).1 : S)
⊢ (algebraMap R S : (a : R) → S) (sec M z).1 =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑(sec M z).2 : R) : S) z

Tactic:
rw [mul_comm, sec_spec]

Premises used: IsLocalization.sec_spec, mul_comm
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
h : 0 ∈ M
⊢ Subsingleton S

Tactic:
(toLocalizationMap M S).subsingleton h

Premises used: IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.subsingleton
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ Subsingleton S ↔ 0 ∈ M

Tactic:
(toLocalizationMap M S).subsingleton_iff

Premises used: Set.Mem, Submonoid.LocalizationMap.subsingleton_iff, IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
c : ↥M
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑c : R) * x) : S)
    ((algebraMap R S : (a : R) → S) ((↑c : R) * y) : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
(toLocalizationMap M S).map_right_cancel h

Premises used: IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.map_right_cancel
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
c : ↥M
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * (↑c : R)) : S)
    ((algebraMap R S : (a : R) → S) (y * (↑c : R)) : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
(toLocalizationMap M S).map_left_cancel h

Premises used: IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.map_left_cancel
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
x : R
y : ↥M
h : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) x
hx : x = 0
⊢ HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = 0

Tactic:
rw [hx, (algebraMap R S).map_zero] at h

Premises used: Algebra.algebraMap, RingHom.map_zero
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
x : R
y : ↥M
h : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) x
hx : x = 0
h₁ : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = 0
⊢ x = 0

Tactic:
rw [hx, (algebraMap R S).map_zero] at h

Premises used: Algebra.algebraMap, RingHom.map_zero
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
x : R
y : ↥M
h : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = 0
hx : x = 0
⊢ z = 0

Tactic:
(IsUnit.mul_left_eq_zero (IsLocalization.map_units S y)).1 h

Premises used: IsUnit.mul_left_eq_zero, Iff.mp, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
x : R
y : ↥M
h : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = 0
hx : x = 0
⊢ z = 0

Tactic:
exact (IsUnit.mul_left_eq_zero (IsLocalization.map_units S y)).1 h

Premises used: IsUnit.mul_left_eq_zero, Iff.mp, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
r : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) (0 : S) ↔ ∃ (m : ↥M), (↑m : R) * r = 0

Tactic:
(toLocalizationMap M S).map_eq_zero_iff

Premises used: Set.Mem, Submonoid.LocalizationMap.map_eq_zero_iff, IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
⊢ mk' S (sec M z).1 (sec M z).2 = z

Tactic:
(toLocalizationMap M S).mk'_sec _

Premises used: Set.Mem, IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.mk'_sec
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (x₁ * x₂) (y₁ * y₂) = mk' S x₁ y₁ * mk' S x₂ y₂

Tactic:
(toLocalizationMap M S).mk'_mul _ _ _ _

Premises used: Set.Mem, IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
⊢ mk' (M := M) S x 1 = (algebraMap R S : (a : R) → S) x

Tactic:
(toLocalizationMap M S).mk'_one _

Premises used: Set.Mem, Submonoid.LocalizationMap.mk'_one, IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
⊢ HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) x

Tactic:
(toLocalizationMap M S).mk'_spec _ _

Premises used: IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.mk'_spec
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) (mk' S x y) = (algebraMap R S : (a : R) → S) x

Tactic:
(toLocalizationMap M S).mk'_spec' _ _

Premises used: IsLocalization.mk', Submonoid.LocalizationMap.mk'_spec', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
hy : y ∈ M
⊢ HMul.hMul (β := S) (mk' S x (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy)) ((algebraMap R S : (a : R) → S) y : S) =
    (algebraMap R S : (a : R) → S) x

Tactic:
mk'_spec S x ⟨y, hy⟩

Premises used: Subtype.mk, IsLocalization.mk'_spec
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
hy : y ∈ M
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S x (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy)) =
    (algebraMap R S : (a : R) → S) x

Tactic:
mk'_spec' S x ⟨y, hy⟩

Premises used: IsLocalization.mk'_spec', Subtype.mk
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z : S
⊢ z = mk' S x y ↔ HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) x

Tactic:
(toLocalizationMap M S).eq_mk'_iff_mul_eq

Premises used: IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.eq_mk'_iff_mul_eq
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z : R
h : z * (↑y : R) = x
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    (algebraMap R S : (a : R) → S) (z * (↑y : R))
rw₁ rw₂ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    (algebraMap R S : (a : R) → S) x

Tactic:
rw [← h, map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z : S
⊢ mk' S x y = z ↔ (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S)

Tactic:
(toLocalizationMap M S).mk'_eq_iff_eq_mul

Premises used: IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.mk'_eq_iff_eq_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z₁ z₂ : S
rw :
  mk' S x y + z₁ = z₂ ↔
    HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
        HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
rw₁ :
  HMul.hMul (β := S) (mk' S x y + z₁) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S) ↔
    HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
        HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
rw₂ rw₃ :
  HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
        HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S) ↔
    HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
        HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
⊢ mk' S x y + z₁ = z₂ ↔
    HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) x : S)
        (HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S)) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)

Tactic:
rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]

Premises used: IsLocalization.map_units, IsUnit.mul_left_inj, right_distrib, IsLocalization.mk'_spec