-- Mathlib/RingTheory/Localization/LocalizationLocalization.lean
theorem mem_localizationLocalizationSubmodule {x : R} :
    x ∈ localizationLocalizationSubmodule M N ↔
      ∃ (y : N) (z : M), algebraMap R S x = y * algebraMap R S z

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
y : ↥N
z : ↥M
e : (algebraMap R S) x = ↑y * (algebraMap R S) ↑z
⊢ ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x

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

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) →
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

Tactic:
rintro ⟨y, hy, _, ⟨z, hz, rfl⟩, e⟩

Result:
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
y : S
hy : y ∈ N
z : R
hz : z ∈ ↑M
e : y * (algebraMap R S) z = (algebraMap R S) x
⊢ ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ x ∈ localizationLocalizationSubmodule M N ↔ ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

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

Result:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) ↔
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

Proof state:
case mpr
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z) →
    ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x

Tactic:
rintro ⟨y, z, e⟩

Result:
case mpr.intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
y : ↥N
z : ↥M
e : (algebraMap R S) x = ↑y * (algebraMap R S) ↑z
⊢ ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) ↔
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) →
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

case mpr
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z) →
    ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x

Proof state:
case mp.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
y : S
hy : y ∈ N
z : R
hz : z ∈ ↑M
e : y * (algebraMap R S) z = (algebraMap R S) x
⊢ ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

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

Result:
no goals