awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
x y : R
z : ↥N
eq₁ :
  HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S) =
    HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S)
z' : R
s : ↥M
eq₂ : HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) z'
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    (algebraMap R S : (a : R) → S) (y * z')
rw₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) z' : S) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) y : S) ((algebraMap R S : (a : R) → S) z' : S)
rw₂ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₃ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S)
      (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S))
rw₄ :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
rw₅ :
  HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) x : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
rw₆ :
  HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (↑z : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
rw₇ rw₈ :
  HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (β := S) (HMul.hMul (β := S) (↑z : S) ((algebraMap R S : (a : R) → S) y : S))
      ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x * z') : S) ((algebraMap R S : (a : R) → S) (y * z') : S)

Tactic:
rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
    mul_comm _ (z : S)]

Premises used: mul_assoc, map_mul, mul_comm, Subtype.val
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ IsLocalization (localizationLocalizationSubmodule M N) T

Tactic:
localization_localization_isLocalization M N T

Premises used: IsLocalization.localization_localization_isLocalization
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
h : Submonoid.comap (F := R →+* S) (algebraMap R S) N = localizationLocalizationSubmodule M N
⊢ IsLocalization (Submonoid.comap (F := R →+* S) (algebraMap R S) N) T

Tactic:
convert! localization_localization_isLocalization M N T using 1

Premises used: IsLocalization.localization_localization_isLocalization
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
h : N = N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M
⊢ Eq (α := Submonoid R) (Submonoid.comap (F := R →+* S) (algebraMap R S) N)
    (Submonoid.comap (F := R →+* S) (algebraMap R S) (N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M))

Tactic:
congr
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
h : N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M = N
⊢ N = N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M

Tactic:
symm
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
h : Submonoid.map (F := R →+* S) (algebraMap R S) M ≤ N
⊢ N ⊔ Submonoid.map (F := R →+* S) (algebraMap R S) M = N

Tactic:
rw [sup_eq_left]

Premises used: sup_eq_left
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
x : R
hx : x ∈ (↑M : Set R)
⊢ Membership.mem (α := S) N ((algebraMap R S : (a : R) → S) x : S)

Tactic:
H _ (IsLocalization.map_units _ ⟨x, hx⟩)

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
x : R
hx : x ∈ (↑M : Set R)
⊢ Membership.mem (α := S) N ((algebraMap R S : (a : R) → S) x : S)

Tactic:
exact H _ (IsLocalization.map_units _ ⟨x, hx⟩)

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst_8 : IsLocalization.AtPrime T p
apply : ∀ (x : S), IsUnit x → x ∈ p.primeCompl
⊢ IsLocalization.AtPrime T (Ideal.comap (F := R →+* S) (algebraMap R S) p)

Tactic:
apply localization_localization_isLocalization_of_has_all_units M p.primeCompl T

Premises used: IsLocalization.localization_localization_isLocalization_of_has_all_units, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst_8 : IsLocalization.AtPrime T p
x : S
hx : IsUnit x
hx' : x ∈ (↑p : Set S)
⊢ False

Tactic:
(Hp.1 : ¬_) (p.eq_top_of_isUnit_mem hx' hx)

Premises used: Ideal.eq_top_of_isUnit_mem, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid 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
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst_8 : IsLocalization.AtPrime T p
x : S
hx : IsUnit x
hx' : x ∈ (↑p : Set S)
⊢ False

Tactic:
exact (Hp.1 : ¬_) (p.eq_top_of_isUnit_mem hx' hx)

Premises used: Ideal.eq_top_of_isUnit_mem, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
p : Ideal (Localization (M := R) M)
inst_8 : p.IsPrime
⊢ IsScalarTower R (Localization (M := R) M) (Localization.AtPrime p)

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
p : Ideal (Localization (M := R) M)
inst_8 : p.IsPrime
⊢ IsLocalization.AtPrime (Localization.AtPrime p)
    (Ideal.comap (F := R →+* Localization (M := R) M) (algebraMap R (Localization (M := R) M)) p)

Tactic:
isLocalization_isLocalization_atPrime_isLocalization M _ _

Premises used: IsLocalization.isLocalization_isLocalization_atPrime_isLocalization
-- 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
⊢ IsScalarTower R S T

Tactic:
letI := localizationAlgebraOfSubmonoidLe S T M N h
  IsScalarTower.of_algebraMap_eq' (IsLocalization.lift_comp _).symm

Premises used: IsLocalization.lift_comp, IsScalarTower.of_algebraMap_eq', IsLocalization.localizationAlgebraOfSubmonoidLe._proof_2, Eq.symm
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
x : Ideal R
H : x.IsPrime
inst_5 : IsDomain R
a : R
ha : a ∈ x.primeCompl
rw : a ≠ 0
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) a

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 : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
x : Ideal R
H : x.IsPrime
inst_5 : IsDomain R
a : R
ha : a ∈ x.primeCompl
⊢ a ≠ 0

Tactic:
fun h => ha (h.symm ▸ x.zero_mem)

Premises used: Eq.rec, Ideal.zero_mem, Eq.symm, Not
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
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 S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
x : Ideal R
H : x.IsPrime
inst_5 : IsDomain R
a : R
ha : a ∈ x.primeCompl
⊢ a ≠ 0

Tactic:
exact fun h => ha (h.symm ▸ x.zero_mem)
-- Module: Mathlib.RingTheory.Localization.LocalizationLocalization
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R_1 S
N : Submonoid S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R_1 T
R : Type u_4
inst_5 : CommRing R
inst_6 : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
⊢ IsScalarTower R (Localization.AtPrime p) (FractionRing R)

Tactic:
localization_isScalarTower_of_submonoid_le (Localization.AtPrime p) (FractionRing R)
    p.primeCompl (nonZeroDivisors R) p.primeCompl_le_nonZeroDivisors

Premises used: Localization.AtPrime, FractionRing, nonZeroDivisors, Ideal.primeCompl_le_nonZeroDivisors, Ideal.primeCompl, IsLocalization.localization_isScalarTower_of_submonoid_le
-- 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
y : R
hy : y ∈ (↑N : Set R)
⊢ IsUnit.{u_3} (M := T) ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) y hy) : R) : T)

Tactic:
IsLocalization.map_units T ⟨y, hy⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- 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
y : R
hy : y ∈ (↑N : Set R)
h₁ :
  Eq.{u_3 + 1} (α := T)
    ((algebraMap S T : (a : S) → T)
        ((↑(Subtype.mk (p := fun (x : S) ↦
                Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
                ((algebraMap R S : (a : R) → S) y) ⋯) :
            S) :
          S) :
      T)
    ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) y hy) : R) : T)
⊢ IsUnit.{u_3} (M := T)
    ((algebraMap S T : (a : S) → T)
        ((↑(Subtype.mk (p := fun (x : S) ↦
                Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
                ((algebraMap R S : (a : R) → S) y) ⋯) :
            S) :
          S) :
      T)

Tactic:
convert! IsLocalization.map_units T ⟨y, hy⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- 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
y : R
hy : y ∈ (↑N : Set R)
⊢ Eq.{u_3 + 1} (α := T)
    ((algebraMap S T : (a : S) → T)
        ((↑(Subtype.mk (p := fun (x : S) ↦
                Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
                ((algebraMap R S : (a : R) → S) y) ⋯) :
            S) :
          S) :
      T)
    ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) y hy) : R) : T)

Tactic:
(IsScalarTower.algebraMap_apply _ _ _ _).symm

Premises used: Eq.symm, IsScalarTower.algebraMap_apply
-- 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
y : R
hy : y ∈ (↑N : Set R)
⊢ Eq.{u_3 + 1} (α := T)
    ((algebraMap S T : (a : S) → T)
        ((↑(Subtype.mk (p := fun (x : S) ↦
                Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
                ((algebraMap R S : (a : R) → S) y) ⋯) :
            S) :
          S) :
      T)
    ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) y hy) : R) : T)

Tactic:
exact (IsScalarTower.algebraMap_apply _ _ _ _).symm

Premises used: Eq.symm, IsScalarTower.algebraMap_apply
-- 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
y : T
obtain :
  ∀ (x : R) (s : ↥N)
    (e :
      HMul.hMul (β := T) y ((algebraMap R T : (a : R) → T) (↑(x, s).2 : R) : T) =
        (algebraMap R T : (a : R) → T) (x, s).1),
    ∃ (x : S × ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)),
      HMul.hMul (β := T) y ((algebraMap S T : (a : S) → T) (↑x.2 : S) : T) = (algebraMap S T : (a : S) → T) x.1
⊢ ∃ (x : S × ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)),
    HMul.hMul (β := T) y ((algebraMap S T : (a : S) → T) (↑x.2 : S) : T) = (algebraMap S T : (a : S) → T) x.1

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

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
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
y : T
x : R
s : ↥N
e : HMul.hMul (β := T) y ((algebraMap R T : (a : R) → T) (↑(x, s).2 : R) : T) = (algebraMap R T : (a : R) → T) (x, s).1
⊢ ∃ (x : S × ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)),
    HMul.hMul (β := T) y ((algebraMap S T : (a : S) → T) (↑x.2 : S) : T) = (algebraMap S T : (a : S) → T) x.1

Tactic:
⟨⟨algebraMap R S x, _, _, s.prop, rfl⟩, ?_⟩

Premises used: Algebra.algebraMap, Prod.mk, Subtype.mk, Subtype.prop, And.intro, Exists.intro, DFunLike.coe, rfl
-- 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
y : T
x : R
s : ↥N
e : HMul.hMul (β := T) y ((algebraMap R T : (a : R) → T) (↑(x, s).2 : R) : T) = (algebraMap R T : (a : R) → T) (x, s).1
refine :
  HMul.hMul (β := T) y
      ((algebraMap S T : (a : S) → T)
          ((↑((algebraMap R S : (a : R) → S) x,
                    Subtype.mk (p := fun (x : S) ↦
                      Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
                      ((algebraMap R S : (a : R) → S) (↑s : R)) ⋯).2 :
              S) :
            S) :
        T) =
    (algebraMap S T : (a : S) → T)
      (((algebraMap R S : (a : R) → S) x,
            Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
              ((algebraMap R S : (a : R) → S) (↑s : R)) ⋯).1 :
        S)
⊢ ∃ (x : S × ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)),
    HMul.hMul (β := T) y ((algebraMap S T : (a : S) → T) (↑x.2 : S) : T) = (algebraMap S T : (a : S) → T) x.1

Tactic:
refine ⟨⟨algebraMap R S x, _, _, s.prop, rfl⟩, ?_⟩
-- 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
y : T
x : R
s : ↥N
e : HMul.hMul (β := T) y ((algebraMap R T : (a : R) → T) (↑(x, s).2 : R) : T) = (algebraMap R T : (a : R) → T) (x, s).1
⊢ HMul.hMul (β := T) y
      ((algebraMap S T : (a : S) → T)
          ((↑((algebraMap R S : (a : R) → S) x,
                    Subtype.mk (p := fun (x : S) ↦
                      Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
                      ((algebraMap R S : (a : R) → S) (↑s : R)) ⋯).2 :
              S) :
            S) :
        T) =
    (algebraMap S T : (a : S) → T)
      (((algebraMap R S : (a : R) → S) x,
            Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
              ((algebraMap R S : (a : R) → S) (↑s : R)) ⋯).1 :
        S)

Tactic:
simpa [← IsScalarTower.algebraMap_apply] using e

Premises used: IsScalarTower.algebraMap_apply
-- 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₁ x₂ : S
obtain :
  ∀ (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),
    Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
      ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂

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

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
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₁ x₂ : 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
obtain :
  ∀ (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),
    Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
      ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂

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

Premises used: IsLocalization.surj