case intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
hJ : x ∈ J
r : R
s : { x // x ∈ M }
hx : mk' S r s = x
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
hJ : x ∈ J
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
obtain ⟨r, s, hx⟩ := mk'_surjective M x
case intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
r : R
s : { x // x ∈ M }
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ mk' S r s ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
case intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
hJ : x ∈ J
r : R
s : { x // x ∈ M }
hx : mk' S r s = x
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
rw [← hx] at hJ⊢
no goals
case intro.intro
R : Type u_2
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
r : R
s : { x // x ∈ M }
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ mk' S r s ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
exact
  Ideal.mul_mem_right _ _
    (Ideal.mem_map_of_mem _
      (show (algebraMap R S) r ∈ J from
        mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))