awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this_1 : IsDomain Sₚ
this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
x : R
s : ↥M
hx : Eq.{u_4 + 1} (α := Sₚ) ((algebraMap Rₚ Sₚ : (a : Rₚ) → Sₚ) (mk' Rₚ x s) : Sₚ) (0 : Sₚ)
simp :
  ∀
    (hx :
      ∃ (a : S),
        Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) a ∧
          HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) x : S) = 0),
    ∃ a ∈ M, a * x = 0
⊢ mk' Rₚ x s = 0

Tactic:
simp only [IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
    Subtype.exists, exists_prop, this] at hx ⊢

Premises used: IsLocalization.map_mk', Subtype.exists, exists_prop, IsLocalization.mk'_eq_zero_iff
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this_1 : IsDomain Sₚ
this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
x : R
s : ↥M
hx :
  ∃ (a : S),
    Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) a ∧
      HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) x : S) = 0
obtain :
  ∀ (a : R) (ha : a ∈ (↑M : Set R))
    (H : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) x : S) = 0),
    ∃ a ∈ M, a * x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this_1 : IsDomain Sₚ
this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
x : R
s : ↥M
a : R
ha : a ∈ (↑M : Set R)
H : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) x : S) = 0
⊢ a * x = 0

Tactic:
simp only [← map_mul,
    (injective_iff_map_eq_zero' _).mp (FaithfulSMul.algebraMap_injective R S)] at H

Premises used: injective_iff_map_eq_zero', map_mul, FaithfulSMul.algebraMap_injective, Iff.mp
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this_1 : IsDomain Sₚ
this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
x : R
s : ↥M
a : R
ha : a ∈ (↑M : Set R)
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
⟨a, ha, H⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this_1 : IsDomain Sₚ
this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
x : R
s : ↥M
a : R
ha : a ∈ (↑M : Set R)
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
exact ⟨a, ha, H⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
y : R
hy : y ∈ (↑M : Set R)
⊢ IsUnit.{u_4} (M := S')
    ((algebraMap R' S' : (a : R') → S')
        ((↑(Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
                ((f : (a : R) → R') y) ⋯) :
            R') :
          R') :
      S')

Tactic:
simpa only [← RingHom.comp_apply, H] using (IsLocalization.map_units S ⟨y, hy⟩).map g

Premises used: Subtype.mk, IsLocalization.map_units, RingHom.comp_apply, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
z : S'
obtain :
  ∀ (z : S),
    ∃ (x : R' × ↥(Submonoid.map f M)),
      HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
        (algebraMap R' S' : (a : R') → S') x.1
⊢ ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (β := S') z ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') = (algebraMap R' S' : (a : R') → S') x.1

Tactic:
obtain ⟨z, rfl⟩ := hg z

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
z : S
obtain :
  ∀ (r : R) (s : ↥M)
    (e :
      HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, s).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (r, s).1),
    ∃ (x : R' × ↥(Submonoid.map f M)),
      HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
        (algebraMap R' S' : (a : R') → S') x.1
⊢ ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
      (algebraMap R' S' : (a : R') → S') x.1

Tactic:
obtain ⟨⟨r, s⟩, e⟩ := IsLocalization.surj M z

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
z : S
r : R
s : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, s).1
⊢ ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
      (algebraMap R' S' : (a : R') → S') x.1

Tactic:
⟨⟨f r, _, s.1, s.2, rfl⟩, ?_⟩

Premises used: Prod.mk, Subtype.mk, And.intro, Exists.intro, Subtype.val, DFunLike.coe, rfl, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
z : S
r : R
s : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, s).1
refine :
  HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S')
      ((algebraMap R' S' : (a : R') → S')
          ((↑((f : (a : R) → R') r,
                    Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
                      ((f : (a : R) → R') (↑s : R)) ⋯).2 :
              R') :
            R') :
        S') =
    (algebraMap R' S' : (a : R') → S')
      (((f : (a : R) → R') r,
            Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
              ((f : (a : R) → R') (↑s : R)) ⋯).1 :
        R')
⊢ ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
      (algebraMap R' S' : (a : R') → S') x.1

Tactic:
refine ⟨⟨f r, _, s.1, s.2, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
z : S
r : R
s : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, s).1
⊢ HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S')
      ((algebraMap R' S' : (a : R') → S')
          ((↑((f : (a : R) → R') r,
                    Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
                      ((f : (a : R) → R') (↑s : R)) ⋯).2 :
              R') :
            R') :
        S') =
    (algebraMap R' S' : (a : R') → S')
      (((f : (a : R) → R') r,
            Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
              ((f : (a : R) → R') (↑s : R)) ⋯).1 :
        R')

Tactic:
simpa only [map_mul, ← RingHom.comp_apply, H] using DFunLike.congr_arg g e

Premises used: map_mul, RingHom.comp_apply, DFunLike.congr_arg
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
x y : R'
e : Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') x : S') ((algebraMap R' S' : (a : R') → S') y : S')
obtain :
  ∀ (x : R)
    (e :
      Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') x : R') : S')
        ((algebraMap R' S' : (a : R') → S') y : S')),
    ∃ (c : ↥(Submonoid.map f M)), HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') = (↑c : R') * y
⊢ ∃ (c : ↥(Submonoid.map f M)), (↑c : R') * x = (↑c : R') * y

Tactic:
obtain ⟨x, rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
y : R'
x : R
e :
  Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') x : R') : S')
    ((algebraMap R' S' : (a : R') → S') y : S')
obtain :
  ∀ (y : R)
    (e :
      Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') x : R') : S')
        ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') y : R') : S')),
    ∃ (c : ↥(Submonoid.map f M)),
      HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') =
        HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') y : R')
⊢ ∃ (c : ↥(Submonoid.map f M)), HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') = (↑c : R') * y

Tactic:
obtain ⟨y, rfl⟩ := hf y

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
x y : R
e :
  Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') x : R') : S')
    ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') y : R') : S')
⊢ Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') (mk' (M := M) S (x - y) 1) : S') (0 : S')

Tactic:
rw [← sub_eq_zero, ← map_sub, ← map_sub, ← RingHom.comp_apply, ← H, RingHom.comp_apply,
      ← IsLocalization.mk'_one (M := M)] at e

Premises used: map_sub, sub_eq_zero, IsLocalization.mk'_one, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
x y : R
e : Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') (mk' (M := M) S (x - y) 1) : S') (0 : S')
obtain :
  ∀ (r : R) (hr : r ∈ M) (hr' : Membership.mem (γ := Ideal R) (RingHom.ker f) (r * (x - y))),
    ∃ (c : ↥(Submonoid.map f M)),
      HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') =
        HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') y : R')
⊢ ∃ (c : ↥(Submonoid.map f M)),
    HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') =
      HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') y : R')

Tactic:
obtain ⟨r, hr, hr'⟩ := (IsLocalization.mk'_mem_map_algebraMap_iff M _ _ _ _).mp (H' e)

Premises used: IsLocalization.mk'_mem_map_algebraMap_iff, Iff.mp
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
x y : R
e : Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') (mk' (M := M) S (x - y) 1) : S') (0 : S')
r : R
hr : r ∈ M
hr' : Membership.mem (γ := Ideal R) (RingHom.ker f) (r * (x - y))
⊢ HMul.hMul (α := R') (β := R')
      ((↑(Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
              ((f : (a : R) → R') r) ⋯) :
          R') :
        R')
      ((f : (a : R) → R') x : R') =
    HMul.hMul (α := R') (β := R')
      ((↑(Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
              ((f : (a : R) → R') r) ⋯) :
          R') :
        R')
      ((f : (a : R) → R') y : R')

Tactic:
simpa [sub_eq_zero, mul_sub] using hr'

Premises used: mul_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
x y : R
e : Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') (mk' (M := M) S (x - y) 1) : S') (0 : S')
r : R
hr : r ∈ M
hr' : Membership.mem (γ := Ideal R) (RingHom.ker f) (r * (x - y))
⊢ ∃ (c : ↥(Submonoid.map f M)),
    HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') =
      HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') y : R')

Tactic:
exact ⟨⟨_, r, hr, rfl⟩, by simpa [sub_eq_zero, mul_sub] using hr'⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
⊢ LE.le (α := Ideal S)
    (RingHom.ker (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)))
    (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
P : Ideal R
inst_4 : P.IsPrime
inst_5 : IsDomain R
inst_6 : IsDomain S
inst_7 : FaithfulSMul R S
⊢ IsDomain.{u_2} (Localization (M := S) (algebraMapSubmonoid S P.primeCompl))

Tactic:
isDomain_localization (map_le_nonZeroDivisors_of_injective _
    (FaithfulSMul.algebraMap_injective R S) P.primeCompl_le_nonZeroDivisors)

Premises used: map_le_nonZeroDivisors_of_injective, IsLocalization.isDomain_localization, FaithfulSMul.algebraMap_injective, Ideal.primeCompl_le_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ IsInteger.{u_1, u_2} R (S := S) 0

Tactic:
Subsemiring.zero_mem _

Premises used: IsLocalization.IsInteger, Set.Mem, Subsemiring.zero_mem
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ IsInteger.{u_1, u_2} R (S := S) 1

Tactic:
Subsemiring.one_mem _

Premises used: IsLocalization.IsInteger, Subsemiring.one_mem
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a b : S
ha : IsInteger R a
hb : IsInteger R b
⊢ IsInteger R (a + b)

Tactic:
Subsemiring.add_mem _ ha hb

Premises used: IsLocalization.IsInteger, Set.Mem, Subsemiring.add_mem
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a b : S
ha : IsInteger R a
hb : IsInteger R b
⊢ IsInteger R (a * b)

Tactic:
Subsemiring.mul_mem _ ha hb

Premises used: IsLocalization.IsInteger, Set.Mem, Subsemiring.mul_mem
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a : R
b : S
hb : IsInteger R b
rcases : ∀ (b' : R) (hb : (algebraMap R S : (a : R) → S) b' = b), IsInteger R (a • b)
⊢ IsInteger R (a • b)

Tactic:
rcases hb with ⟨b', hb⟩
-- Module: Mathlib.RingTheory.Localization.Integer
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S : (a : R) → S) b' = b
h : (algebraMap R S : (a : R) → S) (a * b') = a • b
⊢ IsInteger R (a • b)

Tactic:
use a * b'