-- Mathlib/RingTheory/Localization/LocalizationLocalization.lean
theorem isLocalization_of_is_exists_mul_mem (M N : Submonoid R) [IsLocalization M S] (h : M ≤ N)
    (h' : ∀ x : N, ∃ m : R, m * x ∈ M) : IsLocalization N S :=
  { map_units' := fun y => by
      obtain ⟨m, hm⟩ := h' y
      have := IsLocalization.map_units S ⟨_, hm⟩
      rw [map_mul] at this
      exact (IsUnit.mul_iff.mp this).2
    surj' := fun z => by
      obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M z
      exact ⟨⟨y, _, h s.prop⟩, e⟩
    exists_of_eq := fun {_ _} => by
      rw [IsLocalization.eq_iff_exists M]
      exact fun ⟨x, hx⟩ => ⟨⟨_, h x.prop⟩, hx⟩ }

Proof state:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
this : IsUnit ((algebraMap R S) ↑⟨m * ↑y, hm⟩)
⊢ IsUnit ((algebraMap R S) ↑y)

Tactic:
rw [map_mul] at this

Result:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
this : IsUnit ((algebraMap R S) m * (algebraMap R S) ↑y)
⊢ IsUnit ((algebraMap R S) ↑y)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
z : S
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

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

Result:
case intro.mk
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
z : S
y : R
s : ↥M
e : z * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
⊢ IsUnit ((algebraMap R S) ↑y)

Tactic:
obtain ⟨m, hm⟩ := h' y

Result:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
⊢ IsUnit ((algebraMap R S) ↑y)

Proof state:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
⊢ IsUnit ((algebraMap R S) ↑y)

Tactic:
have := IsLocalization.map_units S ⟨_, hm⟩

Result:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
this : IsUnit ((algebraMap R S) ↑⟨m * ↑y, hm⟩)
⊢ IsUnit ((algebraMap R S) ↑y)

Proof state:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
this : IsUnit ((algebraMap R S) m * (algebraMap R S) ↑y)
⊢ IsUnit ((algebraMap R S) ↑y)

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

Result:
no goals

Proof state:
case intro.mk
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
z : S
y : R
s : ↥M
e : z * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

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

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) → ∃ c, ↑c * x✝¹ = ↑c * x✝

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

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (algebraMap R S) x✝¹ = (algebraMap R S) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
rw [IsLocalization.eq_iff_exists M]

Result:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) → ∃ c, ↑c * x✝¹ = ↑c * x✝