awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
x : ↥M
rw :
  HMul.hMul (α := S) (β := S)
      ((↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) x) :
          S) :
        S)
      ((algebraMap R S : (a : R) → S) (↑x : R) : S) =
    HMul.hMul (β := S) (mk' S 1 x) ((algebraMap R S : (a : R) → S) (↑x : R) : S)
⊢ (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) x) : S) =
    mk' S 1 x

Tactic:
rw [← (IsLocalization.map_units S x).mul_left_inj]

Premises used: IsLocalization.map_units, IsUnit.mul_left_inj
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
x : ↥M
⊢ HMul.hMul (α := S) (β := S)
      ((↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) x) :
          S) :
        S)
      ((algebraMap R S : (a : R) → S) (↑x : R) : S) =
    HMul.hMul (β := S) (mk' S 1 x) ((algebraMap R S : (a : R) → S) (↑x : R) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
x : S
simp_rw :
  Membership.mem (γ := Submonoid S) (invSubmonoid M S) x ↔
    ∃ (m : ↥M),
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S) =
        x
⊢ Membership.mem (γ := Submonoid S) (invSubmonoid M S) x ↔ ∃ (m : ↥M), mk' S 1 m = x

Tactic:
simp_rw [← toInvSubmonoid_eq_mk']

Premises used: IsLocalization.toInvSubmonoid_eq_mk'
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
x : S
⊢ Membership.mem (γ := Submonoid S) (invSubmonoid M S) x ↔
    ∃ (m : ↥M),
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S) =
        x

Tactic:
⟨fun h => ⟨_, congr_arg Subtype.val (toInvSubmonoid_surjective M S ⟨x, h⟩).choose_spec⟩,
    fun h => h.choose_spec ▸ (toInvSubmonoid M S h.choose).prop⟩

Premises used: Exists.choose_spec, Eq.rec, Subtype.mk, congr_arg, IsLocalization.toInvSubmonoid_surjective, Subtype.prop, Iff.intro, Exists.intro, IsLocalization.toInvSubmonoid, Exists.choose, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
x : S
⊢ Membership.mem (γ := Submonoid S) (invSubmonoid M S) x ↔
    ∃ (m : ↥M),
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S) =
        x

Tactic:
exact ⟨fun h => ⟨_, congr_arg Subtype.val (toInvSubmonoid_surjective M S ⟨x, h⟩).choose_spec⟩,
    fun h => h.choose_spec ▸ (toInvSubmonoid M S h.choose).prop⟩
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
rw : LE.le (α := Submodule R S) ⊤ (Submodule.span R (↑(invSubmonoid M S) : Set S))
⊢ Eq (α := Submodule R S) (Submodule.span R (↑(invSubmonoid M S) : Set S)) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
x : S
rcases :
  ∀ (r : R) (m : ↥M),
    Membership.mem (γ := Submodule R S) (Submodule.span R (↑(invSubmonoid M S) : Set S))
      (HSMul.hSMul (β := S) r
        (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) :
          S))
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (↑(invSubmonoid M S) : Set S)) x

Tactic:
rcases IsLocalization.surj'' M x with ⟨r, m, rfl⟩

Premises used: IsLocalization.surj'', rfl
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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 : R
m : ↥M
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (↑(invSubmonoid M S) : Set S))
    (HSMul.hSMul (β := S) r
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S))

Tactic:
Submodule.smul_mem _ _ (Submodule.subset_span (toInvSubmonoid M S m).prop)

Premises used: Set.Mem, Subtype.prop, IsLocalization.toInvSubmonoid, Submodule.subset_span, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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 : R
m : ↥M
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (↑(invSubmonoid M S) : Set S))
    (HSMul.hSMul (β := S) r
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S))

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (toInvSubmonoid M S m).prop)

Premises used: Subtype.prop, IsLocalization.toInvSubmonoid, Submodule.subset_span, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
inst_4 : Monoid.FG.{u_1} ↥M
⊢ Monoid.FG.{u_2} ↥(invSubmonoid M S)

Tactic:
have := Monoid.fg_of_surjective _ (toInvSubmonoid_surjective M S)
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
inst_4 : Monoid.FG.{u_1} ↥M
this : Monoid.FG.{u_2} ↥(invSubmonoid M S)
⊢ Submonoid.FG (invSubmonoid M S)

Tactic:
rw [Monoid.fg_iff_submonoid_fg] at this

Premises used: Monoid.fg_iff_submonoid_fg
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
inst_4 : Monoid.FG.{u_1} ↥M
this : Submonoid.FG (invSubmonoid M S)
rcases :
  ∀ (s : Finset S) (hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)),
    Algebra.FiniteType R S
⊢ Algebra.FiniteType R S

Tactic:
rcases this with ⟨s, hs⟩
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
inst_4 : Monoid.FG.{u_1} ↥M
s : Finset S
hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)
⊢ Algebra.FiniteType R S

Tactic:
⟨⟨s, ?_⟩⟩

Premises used: Algebra.FiniteType.mk, Exists.intro
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
inst_4 : Monoid.FG.{u_1} ↥M
s : Finset S
hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)
refine : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
⊢ Algebra.FiniteType R S

Tactic:
refine ⟨⟨s, ?_⟩⟩
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
inst_4 : Monoid.FG.{u_1} ↥M
s : Finset S
hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)
rw : LE.le (α := Subalgebra R S) ⊤ (Algebra.adjoin R (↑s : Set S))
⊢ Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
inst_4 : Monoid.FG.{u_1} ↥M
s : Finset S
hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)
x : S
rw : x ∈ (↑⊤ : Set S)
⊢ x ∈
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S)) :
          Submodule R S) :
      Set S)

Tactic:
rw [Algebra.adjoin_eq_span, hs, span_invSubmonoid]

Premises used: Algebra.adjoin_eq_span, IsLocalization.span_invSubmonoid
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
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
inst_4 : Monoid.FG.{u_1} ↥M
s : Finset S
hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)
x : S
⊢ x ∈ (↑⊤ : Set S)

Tactic:
trivial
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R_1 : Type u_1
inst : CommRing R_1
M_1 : Submonoid R_1
S_1 : Type u_2
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
inst_3 : IsLocalization M_1 S_1
R : Type u_3
S : Type u_4
inst_4 : CommRing R
inst_5 : CommRing S
inst_6 : Algebra R S
inst_7 : Algebra.FiniteType R S
M : Submonoid S
inst_8 : Monoid.FG.{u_4} ↥M
⊢ Algebra.FiniteType.{u_3, u_4} R (Localization (M := S) M)

Tactic:
.trans ‹_› (IsLocalization.finiteType_of_monoid_fg M _)

Premises used: IsLocalization.finiteType_of_monoid_fg, Algebra.FiniteType.trans
-- 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
x : R
rw :
  (∃ y ∈ N,
      ∃ (z : S),
        Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
          y * z = (algebraMap R S : (a : R) → S) x) ↔
    ∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ x ∈ localizationLocalizationSubmodule M N ↔
    ∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)

Tactic:
rw [localizationLocalizationSubmodule, Submonoid.mem_comap, Submonoid.mem_sup]

Premises used: Submonoid.mem_sup, Submonoid.mem_comap, IsLocalization.localizationLocalizationSubmodule
-- 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
x : R
mp :
  (∃ y ∈ N,
      ∃ (z : S),
        Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
          y * z = (algebraMap R S : (a : R) → S) x) →
    ∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
mpr :
  (∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)) →
    ∃ y ∈ N,
      ∃ (z : S),
        Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
          y * z = (algebraMap R S : (a : R) → S) x
⊢ (∃ y ∈ N,
      ∃ (z : S),
        Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
          y * z = (algebraMap R S : (a : R) → S) x) ↔
    ∃ (y : ↥N) (z : ↥M),
      (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)

Tactic:
constructor
-- 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
x : R
y : S
hy : y ∈ N
z : R
hz : z ∈ (↑M : Set R)
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) z : S) = (algebraMap R S : (a : R) → S) x
⊢ ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)

Tactic:
⟨⟨y, hy⟩, ⟨z, hz⟩, e.symm⟩

Premises used: Subtype.mk, Exists.intro, 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
x : R
y : S
hy : y ∈ N
z : R
hz : z ∈ (↑M : Set R)
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) z : S) = (algebraMap R S : (a : R) → S) x
⊢ ∃ (y : ↥N) (z : ↥M),
    (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)

Tactic:
exact ⟨⟨y, hy⟩, ⟨z, hz⟩, e.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
x : R
y : ↥N
z : ↥M
e : (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ ∃ y ∈ N,
    ∃ (z : S),
      Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
        y * z = (algebraMap R S : (a : R) → S) x

Tactic:
⟨y, y.prop, _, ⟨z, z.prop, rfl⟩, e.symm⟩

Premises used: Subtype.prop, And.intro, Exists.intro, Eq.symm, Subtype.val, 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
x : R
y : ↥N
z : ↥M
e : (algebraMap R S : (a : R) → S) x = HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ ∃ y ∈ N,
    ∃ (z : S),
      Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) z ∧
        y * z = (algebraMap R S : (a : R) → S) x

Tactic:
exact ⟨y, y.prop, _, ⟨z, z.prop, rfl⟩, e.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
y : ↥(localizationLocalizationSubmodule M N)
obtain :
  ∀ (y' : ↥N) (z : ↥M)
    (eq :
      (algebraMap R S : (a : R) → S) (↑y : R) =
        HMul.hMul (β := S) (↑y' : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)),
    IsUnit.{u_3} (M := T) ((algebraMap R T : (a : R) → T) (↑y : R) : T)
⊢ IsUnit.{u_3} (M := T) ((algebraMap R T : (a : R) → T) (↑y : R) : T)

Tactic:
obtain ⟨y', z, eq⟩ := mem_localizationLocalizationSubmodule.mp y.prop

Premises used: IsLocalization.mem_localizationLocalizationSubmodule, Subtype.prop, Iff.mp
-- 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
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq :
  (algebraMap R S : (a : R) → S) (↑y : R) = HMul.hMul (β := S) (↑y' : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
rw :
  IsUnit.{u_3} (M := T) ((algebraMap S T : (a : S) → T) (↑y' : S) : T) ∧
    IsUnit.{u_3} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑z : R) : S) : T)
⊢ IsUnit.{u_3} (M := T) ((algebraMap R T : (a : R) → T) (↑y : R) : T)

Tactic:
rw [IsScalarTower.algebraMap_apply R S T, eq, map_mul, IsUnit.mul_iff]

Premises used: IsUnit.mul_iff, map_mul, IsScalarTower.algebraMap_apply
-- 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
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq :
  (algebraMap R S : (a : R) → S) (↑y : R) = HMul.hMul (β := S) (↑y' : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ IsUnit.{u_3} (M := T) ((algebraMap S T : (a : S) → T) (↑y' : S) : T) ∧
    IsUnit.{u_3} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑z : R) : S) : T)

Tactic:
⟨IsLocalization.map_units T y', (IsLocalization.map_units _ z).map (algebraMap S T)⟩

Premises used: Algebra.algebraMap, And.intro, IsLocalization.map_units, IsUnit.map
-- 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
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq :
  (algebraMap R S : (a : R) → S) (↑y : R) = HMul.hMul (β := S) (↑y' : S) ((algebraMap R S : (a : R) → S) (↑z : R) : S)
⊢ IsUnit.{u_3} (M := T) ((algebraMap S T : (a : S) → T) (↑y' : S) : T) ∧
    IsUnit.{u_3} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑z : R) : S) : T)

Tactic:
exact ⟨IsLocalization.map_units T y', (IsLocalization.map_units _ z).map (algebraMap S T)⟩
-- 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 : T
rcases :
  ∀ (y : S) (s : ↥N)
    (eq₁ :
      HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑(y, s).2 : S) : T) =
        (algebraMap S T : (a : S) → T) (y, s).1),
    ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
      HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
⊢ ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1

Tactic:
rcases IsLocalization.surj N x with ⟨⟨y, s⟩, eq₁⟩

Premises used: IsLocalization.surj
-- 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 : T
y : S
s : ↥N
eq₁ :
  HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑(y, s).2 : S) : T) = (algebraMap S T : (a : S) → T) (y, s).1
rcases :
  ∀ (z : R) (t : ↥M)
    (eq₂ :
      HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(z, t).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (z, t).1),
    ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
      HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
⊢ ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1

Tactic:
rcases IsLocalization.surj M y with ⟨⟨z, t⟩, eq₂⟩

Premises used: IsLocalization.surj
-- 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 : T
y : S
s : ↥N
eq₁ :
  HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑(y, s).2 : S) : T) = (algebraMap S T : (a : S) → T) (y, s).1
z : R
t : ↥M
eq₂ :
  HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(z, t).2 : R) : S) = (algebraMap R S : (a : R) → S) (z, t).1
rcases :
  ∀ (z' : R) (t' : ↥M)
    (eq₃ :
      HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑(z', t').2 : R) : S) =
        (algebraMap R S : (a : R) → S) (z', t').1),
    ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
      HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1
⊢ ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1

Tactic:
rcases IsLocalization.surj M (s : S) with ⟨⟨z', t'⟩, eq₃⟩

Premises used: IsLocalization.surj, 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
x : T
y : S
s : ↥N
eq₁ : HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T) = (algebraMap S T : (a : S) → T) y
z : R
t : ↥M
eq₂ : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑t : R) : S) = (algebraMap R S : (a : R) → S) z
z' : R
t' : ↥M
eq₃ : HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) = (algebraMap R S : (a : R) → S) z'
⊢ ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1

Tactic:
⟨⟨z * t', z' * t, ?_⟩, ?_⟩

Premises used: HMul.hMul, Prod.mk, Subtype.mk, Exists.intro, 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
x : T
y : S
s : ↥N
eq₁ : HMul.hMul (β := T) x ((algebraMap S T : (a : S) → T) (↑s : S) : T) = (algebraMap S T : (a : S) → T) y
z : R
t : ↥M
eq₂ : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑t : R) : S) = (algebraMap R S : (a : R) → S) z
z' : R
t' : ↥M
eq₃ : HMul.hMul (β := S) (↑s : S) ((algebraMap R S : (a : R) → S) (↑t' : R) : S) = (algebraMap R S : (a : R) → S) z'
refine_1 : z' * (↑t : R) ∈ localizationLocalizationSubmodule M N
refine_2 :
  HMul.hMul (β := T) x
      ((algebraMap R T : (a : R) → T)
          (↑(z * (↑t' : R),
                  Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) (z' * (↑t : R)) ⋯).2 :
            R) :
        T) =
    (algebraMap R T : (a : R) → T)
      (z * (↑t' : R), Subtype.mk (p := fun (x : R) ↦ x ∈ localizationLocalizationSubmodule M N) (z' * (↑t : R)) ⋯).1
⊢ ∃ (y : R × ↥(localizationLocalizationSubmodule M N)),
    HMul.hMul (β := T) x ((algebraMap R T : (a : R) → T) (↑y.2 : R) : T) = (algebraMap R T : (a : R) → T) y.1

Tactic:
refine ⟨⟨z * t', z' * t, ?_⟩, ?_⟩