awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
y : ↥N
m : R
hm : m * (↑y : R) ∈ M
this :
  IsUnit
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) m : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S))
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)

Tactic:
(IsUnit.mul_iff.mp this).2

Premises used: IsUnit.mul_iff, And.right, Iff.mp
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
y : ↥N
m : R
hm : m * (↑y : R) ∈ M
this :
  IsUnit
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) m : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S))
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)

Tactic:
exact (IsUnit.mul_iff.mp this).2

Premises used: IsUnit.mul_iff, And.right, Iff.mp
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
z : S
obtain :
  ∀ (y : R) (s : ↥M)
    (e :
      HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (y, s).1),
    ∃ (x : R × ↥N),
      HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1
⊢ ∃ (x : R × ↥N),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1

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

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
z : S
y : R
s : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
⊢ ∃ (x : R × ↥N),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1

Tactic:
⟨⟨y, _, h s.prop⟩, e⟩

Premises used: Prod.mk, Subtype.mk, Subtype.prop, Exists.intro
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
z : S
y : R
s : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
⊢ ∃ (x : R × ↥N),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1

Tactic:
exact ⟨⟨y, _, h s.prop⟩, e⟩
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
x x_1 : R
rw : (∃ (c : ↥M), (↑c : R) * x = (↑c : R) * x_1) → ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * x_1
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) x_1 : S) →
    ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * x_1

Tactic:
rw [IsLocalization.eq_iff_exists M]

Premises used: IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
x x_1 : R
⊢ (∃ (c : ↥M), (↑c : R) * x = (↑c : R) * x_1) → ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * x_1

Tactic:
fun ⟨x, hx⟩ => ⟨⟨_, h x.prop⟩, hx⟩

Premises used: HMul.hMul, Exists, Subtype.mk, _private.0.IsLocalization.isLocalization_of_is_exists_mul_mem.match_1, Subtype.prop, Exists.intro, Subtype.val, Eq
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
x x_1 : R
⊢ (∃ (c : ↥M), (↑c : R) * x = (↑c : R) * x_1) → ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * x_1

Tactic:
exact fun ⟨x, hx⟩ => ⟨⟨_, h x.prop⟩, hx⟩
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x : R
y : ↥M
⊢ (algebraMap R T : (a : R) → T) x =
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) (mk' S x y) : T)
      ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑y : R) ⋯) : R) : T)

Tactic:
simp only [IsScalarTower.algebraMap_apply R S T, ← map_mul, mk'_spec]

Premises used: map_mul, IsScalarTower.algebraMap_apply, IsLocalization.mk'_spec
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
⊢ IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T

Tactic:
have := isLocalization_of_submonoid_le S T M (nonZeroDivisors R) hM
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
⊢ IsFractionRing S T

Tactic:
@isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_

Premises used: IsLocalization.isLocalization_of_is_exists_mul_mem
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
refine_1 :
  LE.le (α := Submonoid S)
    (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R) : Submonoid S)
    (nonZeroDivisors S : Submonoid S)
refine_2 :
  ∀ (x : ↥(nonZeroDivisors S : Submonoid S)),
    ∃ (m : S),
      Membership.mem (γ := Submonoid S)
        (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) (m * (↑x : S))
⊢ IsFractionRing S T

Tactic:
refine @isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_

Premises used: IsLocalization.isLocalization_of_is_exists_mul_mem
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
⊢ LE.le (α := Submonoid S)
    (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R) : Submonoid S)
    (nonZeroDivisors S : Submonoid S)

Tactic:
map_nonZeroDivisors_le M S

Premises used: Set.Mem, IsLocalization.map_nonZeroDivisors_le
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
⊢ LE.le (α := Submonoid S)
    (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R) : Submonoid S)
    (nonZeroDivisors S : Submonoid S)

Tactic:
exact map_nonZeroDivisors_le M S

Premises used: IsLocalization.map_nonZeroDivisors_le
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
refine_2 :
  ∀ (y : R) (s : ↥M)
    (e :
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (y, s).1),
    ∃ (m : S),
      Membership.mem (γ := Submonoid S)
        (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
        (m *
          (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x
                ⋯) :
            S))
⊢ ∃ (m : S),
    Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
      (m *
        (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x ⋯) :
          S))

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

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
y : R
s : ↥M
e : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
h :
  Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
      (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x ⋯) :
        S))
⊢ ∃ (m : S),
    Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
      (m *
        (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x ⋯) :
          S))

Tactic:
use algebraMap R S s

Premises used: Algebra.algebraMap, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
y : R
s : ↥M
e : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
h :
  Membership.mem (α := S) (γ := Submonoid S)
    (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
    ((algebraMap R S : (a : R) → S) (y, s).1 : S)
⊢ Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
      (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x ⋯) :
        S))

Tactic:
rw [mul_comm, Subtype.coe_mk, e]

Premises used: Subtype.coe_mk, mul_comm
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
y : R
s : ↥M
e : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
⊢ Membership.mem (α := S) (γ := Submonoid S)
    (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
    ((algebraMap R S : (a : R) → S) (y, s).1 : S)

Tactic:
Set.mem_image_of_mem (algebraMap R S) (mem_nonZeroDivisors_iff_right.mpr ?_)

Premises used: Iff.mpr, Algebra.algebraMap, Set.Mem, setOf, mem_nonZeroDivisors_iff_right, Set.mem_image_of_mem, Set.image, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
y : R
s : ↥M
e : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
h : ∀ (x : R), x * (y, s).1 = 0 → x = 0
⊢ Membership.mem (α := S) (γ := Submonoid S)
    (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
    ((algebraMap R S : (a : R) → S) (y, s).1 : S)

Tactic:
refine Set.mem_image_of_mem (algebraMap R S) (mem_nonZeroDivisors_iff_right.mpr ?_)

Premises used: Iff.mpr, Algebra.algebraMap, mem_nonZeroDivisors_iff_right, Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
y : R
s : ↥M
e : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
z : R
hz : z * (y, s).1 = 0
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) 0 : S)
⊢ z = 0

Tactic:
apply IsLocalization.injective S hM

Premises used: IsLocalization.injective
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
y : R
s : ↥M
e : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
z : R
hz : z * (y, s).1 = 0
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) z : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) 0 : S)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
y : R
s : ↥M
e : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
z : R
hz : z * (y, s).1 = 0
h : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) z : S) (0 : S)

Tactic:
apply hx
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
y : R
s : ↥M
e : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (y, s).1
z : R
hz : z * (y, s).1 = 0
h :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x)
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₁ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S)
      (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₂ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (y, s).1 : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₃ :
  (algebraMap R S : (a : R) → S) (z * (y, s).1) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₄ :
  (algebraMap R S : (a : R) → S) 0 = HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₅ : 0 = HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₆ h₇ : Eq.{u_2 + 1} (α := S) 0 0
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0

Tactic:
rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]

Premises used: MulZeroClass.zero_mul, mul_assoc, map_zero, map_mul, IsLocalization.map_units, IsUnit.mul_left_inj
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
⊢ Nontrivial T

Tactic:
haveI := IsFractionRing.nontrivial R T
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this : Nontrivial T
⊢ Nontrivial S

Tactic:
haveI := (algebraMap S T).domain_nontrivial
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
apply : M ≤ nonZeroDivisors R
⊢ IsFractionRing S T

Tactic:
apply isFractionRing_of_isLocalization M S T

Premises used: IsFractionRing.isFractionRing_of_isLocalization
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
rw : x ≠ 0
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero]

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
a : Eq.{u_2 + 1} (α := S) 0 1
⊢ False

Tactic:
apply @zero_ne_one S

Premises used: zero_ne_one
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
a : ∃ (m : ↥M), (↑m : R) * 1 = 0
⊢ Eq.{u_2 + 1} (α := S) 0 1

Tactic:
rw [← (algebraMap R S).map_one, ← @mk'_one R _ M, @comm _ Eq, mk'_eq_zero_iff]

Premises used: comm, Algebra.algebraMap, RingHom.map_one, IsLocalization.mk'_one, IsLocalization.mk'_eq_zero_iff
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) x hx) : R) * 1 = 0

Tactic:
simp [hx']