awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
hM : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) (IsUnit.submonoid S)
h : Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
y : S
obtain :
  ∀ (x : R),
    ∃ (x_1 : R × ↥M),
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
          ((algebraMap R S : (a : R) → S) (↑x_1.2 : R) : S) =
        (algebraMap R S : (a : R) → S) x_1.1
⊢ ∃ (x : R × ↥M),
    HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1

Tactic:
obtain ⟨x, rfl⟩ := h.surjective y

Premises used: Function.Bijective.surjective, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
hM : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) (IsUnit.submonoid S)
h : Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : R
h₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
      ((algebraMap R S : (a : R) → S) (↑(x, 1).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (x, 1).1
⊢ ∃ (x_1 : R × ↥M),
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
        ((algebraMap R S : (a : R) → S) (↑x_1.2 : R) : S) =
      (algebraMap R S : (a : R) → S) x_1.1

Tactic:
use ⟨x, 1⟩
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
hM : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) (IsUnit.submonoid S)
h : Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : R
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
      ((algebraMap R S : (a : R) → S) (↑(x, 1).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (x, 1).1

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
hM : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) (IsUnit.submonoid S)
h : Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
⊢ (↑1 : R) * x = (↑1 : R) * y

Tactic:
simp [h.injective hxy]

Premises used: Function.Bijective.injective
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
hS : S ≤ IsUnit.submonoid R
⊢ LE.le (α := Submonoid R) (Algebra.algebraMapSubmonoid R S) (IsUnit.submonoid R)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
⊢ IsLocalization (IsUnit.submonoid R) R

Tactic:
of_le_isUnit le_rfl

Premises used: le_rfl, IsLocalization.of_le_isUnit
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
⊢ IsLocalization (Algebra.algebraMapSubmonoid S (IsUnit.submonoid R)) S

Tactic:
IsLocalization.of_le_isUnit Algebra.algebraMapSubmonoid_isUnit_le

Premises used: Algebra.algebraMapSubmonoid_isUnit_le, IsLocalization.of_le_isUnit
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
refine_1 : Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(Algebra.ofId R S) : (a : R) → S)
refine_2 : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(Algebra.ofId R S) : (a : R) → S)
⊢ R ≃ₐ[R] S

Tactic:
refine AlgEquiv.ofBijective (Algebra.ofId R S) ⟨?_, ?_⟩

Premises used: AlgEquiv.ofBijective, Algebra.ofId, And.intro
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((Algebra.ofId R S : (a : R) → S) x : S) ((Algebra.ofId R S : (a : R) → S) y : S)
refine_1 : ∀ (c : ↥M) (eq : (↑c : R) * x = (↑c : R) * y), x = y
⊢ x = y

Tactic:
obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy

Premises used: Iff.mp, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((Algebra.ofId R S : (a : R) → S) x : S) ((Algebra.ofId R S : (a : R) → S) y : S)
c : ↥M
eq : (↑c : R) * x = (↑c : R) * y
refine_1 : ∀ (u : Rˣ) (hu : (↑u : R) = (↑c : R)), x = y
⊢ x = y

Tactic:
obtain ⟨u, hu⟩ := H c.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((Algebra.ofId R S : (a : R) → S) x : S) ((Algebra.ofId R S : (a : R) → S) y : S)
c : ↥M
eq : (↑c : R) * x = (↑c : R) * y
u : Rˣ
hu : (↑u : R) = (↑c : R)
refine_1 : ∀ (eq : (↑u : R) * x = (↑u : R) * y) (hu : (↑u : R) = (↑c : R)), x = y
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (eq : x = y) (hu : (↑u : R) = (↑c : R)), x = y
⊢ x = y

Tactic:
rwa [← hu, Units.mul_right_inj] at eq

Premises used: Units.mul_right_inj
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
refine_2 :
  ∀ (x : R) (s : ↥M)
    (eq :
      HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (x, s).1),
    ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y
⊢ ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y

Tactic:
obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
refine_2 : ∀ (u : Rˣ) (hu : (↑u : R) = (↑s : R)), ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y
⊢ ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y

Tactic:
obtain ⟨u, hu⟩ := H s.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
u : Rˣ
hu : (↑u : R) = (↑s : R)
h : (Algebra.ofId R S : (a : R) → S) (x * u.inv) = y
⊢ ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y

Tactic:
use x * u.inv

Premises used: Units.inv
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
u : Rˣ
hu : (↑u : R) = (↑s : R)
h : (algebraMap R S : (a : R) → S) (x * (↑u⁻¹ : R)) = y
⊢ (Algebra.ofId R S : (a : R) → S) (x * u.inv) = y

Tactic:
dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]

Premises used: RingHom.toFun_eq_coe, Algebra.ofId, AlgHom.coe_mks
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
u : Rˣ
hu : (↑u : R) = (↑s : R)
h : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) ((↑u : R) * (↑u⁻¹ : R)) : S) = y
⊢ (algebraMap R S : (a : R) → S) (x * (↑u⁻¹ : R)) = y

Tactic:
rw [map_mul, ← eq, ← hu, mul_assoc, ← map_mul]

Premises used: mul_assoc, map_mul
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
u : Rˣ
hu : (↑u : R) = (↑s : R)
⊢ HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) ((↑u : R) * (↑u⁻¹ : R)) : S) = y

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
toIsLocalizationMap : Submonoid.IsLocalizationMap.{u_1, u_3} (M := R) (N := P) M (⇑(algebraMap R P) : (a : R) → P)
⊢ IsLocalization M P

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
toIsLocalizationMap : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
toIsLocalizationMap₁ :
  ∀ (z : P),
    ∃ (x : R × ↥M),
      HMul.hMul (β := P) z ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1
toIsLocalizationMap₂ :
  ∀ {x y : R},
    Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) x : P) ((algebraMap R P : (a : R) → P) y : P) →
      ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y
⊢ Submonoid.IsLocalizationMap.{u_1, u_3} (M := R) (N := P) M (⇑(algebraMap R P) : (a : R) → P)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
⊢ IsUnit.{u_3} (M := P)
    (((↑(↑h : S →ₐ[R] P).toRingHom : S →* P) : (a : S) → P) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : P)

Tactic:
(IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom

Premises used: AlgEquiv.toAlgHom, AlgHom.toRingHom, IsLocalization.map_units, IsUnit.map, RingHom.toMonoidHom
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
h₁ :
  Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
    (((↑(↑h : S →ₐ[R] P).toRingHom : S →* P) : (a : S) → P) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : P)
⊢ IsUnit.{u_3} (M := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)

Tactic:
convert! (IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom

Premises used: AlgEquiv.toAlgHom, AlgHom.toRingHom, IsLocalization.map_units, IsUnit.map, RingHom.toMonoidHom
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
⊢ Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
    (((↑(↑h : S →ₐ[R] P).toRingHom : S →* P) : (a : S) → P) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : P)

Tactic:
(h.commutes y).symm

Premises used: AlgEquiv.commutes, Eq.symm, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
⊢ Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
    (((↑(↑h : S →ₐ[R] P).toRingHom : S →* P) : (a : S) → P) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : P)

Tactic:
exact (h.commutes y).symm

Premises used: AlgEquiv.commutes, Eq.symm, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : P
toIsLocalizationMap :
  ∀ (x : R) (s : ↥M)
    (e :
      HMul.hMul (α := S) (β := S) ((h.symm : (a : P) → S) y : S) ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (x, s).1),
    ∃ (x : R × ↥M),
      HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1
⊢ ∃ (x : R × ↥M),
    HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1

Tactic:
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)

Premises used: IsLocalization.surj, AlgEquiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e :
  HMul.hMul (α := S) (β := S) ((h.symm : (a : P) → S) y : S) ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (x, s).1
⊢ Eq.{u_3 + 1} (α := P)
    ((have this : S → P := (⇑h : (a : S) → P);
      this)
      (HMul.hMul (α := S) (β := S) ((h.symm : (a : P) → S) y : S) ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S)))
    ((have this : S → P := (⇑h : (a : S) → P);
      this)
      ((algebraMap R S : (a : R) → S) (x, s).1))

Tactic:
apply_fun (show S → P from h) at e

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e :
  Eq.{u_3 + 1} (α := P)
    ((have this : S → P := (⇑h : (a : S) → P);
      this)
      (HMul.hMul (α := S) (β := S) ((h.symm : (a : P) → S) y : S) ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S)))
    ((have this : S → P := (⇑h : (a : S) → P);
      this)
      ((algebraMap R S : (a : R) → S) (x, s).1))
⊢ HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑s : R) : P) = (algebraMap R P : (a : R) → P) x

Tactic:
simp only [map_mul, h.apply_symm_apply, h.commutes] at e

Premises used: AlgEquiv.commutes, AlgEquiv.apply_symm_apply, map_mul
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e : HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑s : R) : P) = (algebraMap R P : (a : R) → P) x
⊢ ∃ (x : R × ↥M),
    HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1

Tactic:
⟨⟨x, s⟩, e⟩

Premises used: Prod.mk, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e : HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑s : R) : P) = (algebraMap R P : (a : R) → P) x
⊢ ∃ (x : R × ↥M),
    HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1

Tactic:
exact ⟨⟨x, s⟩, e⟩
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
toIsLocalizationMap :
  Eq.{u_2 + 1} (α := S) ((h.symm.toEquiv : (a : P) → S) ((algebraMap R P : (a : R) → P) x : P) : S)
      ((h.symm.toEquiv : (a : P) → S) ((algebraMap R P : (a : R) → P) y : P) : S) →
    Eq.{u_2 + 1} (α := S) ((h.symm : (a : P) → S) ((algebraMap R P : (a : R) → P) x : P) : S)
      ((h.symm : (a : P) → S) ((algebraMap R P : (a : R) → P) y : P) : S)
⊢ Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) x : P) ((algebraMap R P : (a : R) → P) y : P) →
    ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y

Tactic:
rw [← h.symm.toEquiv.injective.eq_iff, ← IsLocalization.eq_iff_exists M S, ← h.symm.commutes, ←
      h.symm.commutes]

Premises used: AlgEquiv.symm, Function.Injective.eq_iff, AlgEquiv.commutes, Equiv.injective, AlgEquiv.toEquiv, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ Eq.{u_2 + 1} (α := S) ((h.symm.toEquiv : (a : P) → S) ((algebraMap R P : (a : R) → P) x : P) : S)
      ((h.symm.toEquiv : (a : P) → S) ((algebraMap R P : (a : R) → P) y : P) : S) →
    Eq.{u_2 + 1} (α := S) ((h.symm : (a : P) → S) ((algebraMap R P : (a : R) → P) x : P) : S)
      ((h.symm : (a : P) → S) ((algebraMap R P : (a : R) → P) y : P) : S)

Tactic:
id

Premises used: id
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ Eq.{u_2 + 1} (α := S) ((h.symm.toEquiv : (a : P) → S) ((algebraMap R P : (a : R) → P) x : P) : S)
      ((h.symm.toEquiv : (a : P) → S) ((algebraMap R P : (a : R) → P) y : P) : S) →
    Eq.{u_2 + 1} (α := S) ((h.symm : (a : P) → S) ((algebraMap R P : (a : R) → P) x : P) : S)
      ((h.symm : (a : P) → S) ((algebraMap R P : (a : R) → P) y : P) : S)

Tactic:
exact id

Premises used: id
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
H : M ≤ IsUnit.submonoid R
⊢ IsLocalization M R

Tactic:
isLocalization_of_algEquiv _ (atUnits _ _ (S := Localization M) H).symm

Premises used: AlgEquiv.symm, IsLocalization.atUnits, IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
h : S ≃ₐ[R] P
⊢ IsLocalization M S ↔ IsLocalization M P

Tactic:
⟨fun _ => isLocalization_of_algEquiv M h, fun _ => isLocalization_of_algEquiv M h.symm⟩

Premises used: AlgEquiv.symm, Iff.intro, IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
h : S ≃+* P
⊢ IsLocalization M S ↔ IsLocalization M P

Tactic:
letI := (h.toRingHom.comp <| algebraMap R S).toAlgebra
  isLocalization_iff_of_algEquiv M { h with commutes' := fun _ => rfl }

Premises used: RingEquiv.toEquiv, RingEquiv.map_add', RingEquiv.map_mul', AlgEquiv.mk, IsLocalization.isLocalization_iff_of_algEquiv, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
inst_5 : IsLocalization N S
inst_6 : Algebra R P
⊢ IsLocalization M P ↔ IsLocalization N P

Tactic:
⟨fun _ ↦ isLocalization_of_algEquiv N (algEquiv M S P),
    fun _ ↦ isLocalization_of_algEquiv M (algEquiv N S P)⟩

Premises used: IsLocalization.algEquiv, Iff.intro, IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.Localization.Basic
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 R
h₁ : M ≤ N
h₂ : ∀ n ∈ N, ∃ m ∈ M, n ∣ m
⊢ IsLocalization M S ↔ IsLocalization N S

Tactic:
have : IsLocalization N (Localization M) := of_le_of_exists_dvd _ _ h₁ h₂
  isLocalization_iff_of_isLocalization _ _ (Localization M)

Premises used: IsLocalization.isLocalization_iff_of_isLocalization, IsLocalization.of_le_of_exists_dvd, Localization
-- 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 : R
ha : a ∈ (↑M₂ : Set R)
rw : IsUnit.{u_6} (M := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) a : S₂) : T)
⊢ IsUnit.{u_6} (M := T)
    ((algebraMap S₁ T : (a : S₁) → T)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) a) ⋯) :
            S₁) :
          S₁) :
      T)

Tactic:
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T]

Premises used: IsScalarTower.algebraMap_apply