-- Mathlib/RingTheory/Localization/Ideal.lean
theorem mem_map_algebraMap_iff {I : Ideal R} {z} : z ∈ Ideal.map (algebraMap R S) I ↔
    ∃ x : I × M, z * algebraMap R S x.2 = algebraMap R S x.1

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
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I → z ∈ IsLocalization.map_ideal M S I

Tactic:
refine fun h => Ideal.mem_sInf.1 h fun z hz => ?_

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
hz : z ∈ ⇑(algebraMap R S) '' ↑I
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)

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
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1) → z ∈ Ideal.map (algebraMap R S) I

Tactic:
rintro ⟨⟨a, s⟩, h⟩

Result:
case mpr.intro.mk
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
a : ↥I
s : ↥M
h : z * (algebraMap R S) ↑(a, s).2 = (algebraMap R S) ↑(a, s).1
⊢ z ∈ Ideal.map (algebraMap R S) I

Proof state:
case h
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ (algebraMap R S) y = z
Z : ↥I := ⟨y, ⋯⟩
⊢ z * (algebraMap R S) ↑(Z, 1).2 = (algebraMap R S) ↑(Z, 1).1

Tactic:
simp [Z, hy.right]

Result:
no goals

Proof state:
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ (algebraMap R S) y = z
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)

Tactic:
let Z : { x // x ∈ I } := ⟨y, hy.left⟩

Result:
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ (algebraMap R S) y = z
Z : ↥I := ⟨y, ⋯⟩
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)

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
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I → ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

Tactic:
change _ → z ∈ map_ideal M S I

Result:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I → z ∈ IsLocalization.map_ideal M S I

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
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
hz : z ∈ ⇑(algebraMap R S) '' ↑I
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)

Tactic:
obtain ⟨y, hy⟩ := hz

Result:
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ (algebraMap R S) y = z
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I ↔ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

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
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ z ∈ Ideal.map (algebraMap R S) I → ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
⊢ (∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1) → z ∈ Ideal.map (algebraMap R S) I

Proof state:
case mpr.intro.mk
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
a : ↥I
s : ↥M
h : z * (algebraMap R S) ↑(a, s).2 = (algebraMap R S) ↑(a, s).1
⊢ z * (algebraMap R S) ↑s ∈ Ideal.map (algebraMap R S) I

Tactic:
exact h.symm ▸ Ideal.mem_map_of_mem _ a.2

Result:
no goals

Proof state:
case mpr.intro.mk
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
a : ↥I
s : ↥M
h : z * (algebraMap R S) ↑(a, s).2 = (algebraMap R S) ↑(a, s).1
⊢ z ∈ Ideal.map (algebraMap R S) I

Tactic:
rw [← Ideal.unit_mul_mem_iff_mem _ (map_units S s), mul_comm]

Result:
case mpr.intro.mk
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z : S
a : ↥I
s : ↥M
h : z * (algebraMap R S) ↑(a, s).2 = (algebraMap R S) ↑(a, s).1
⊢ z * (algebraMap R S) ↑s ∈ Ideal.map (algebraMap R S) I

Proof state:
case mp.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ (algebraMap R S) y = z
Z : ↥I := ⟨y, ⋯⟩
⊢ z ∈ ↑(IsLocalization.map_ideal M S I)

Tactic:
use ⟨Z, 1⟩

Result:
case h
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
z✝ : S
h : z✝ ∈ Ideal.map (algebraMap R S) I
z : S
y : R
hy : y ∈ ↑I ∧ (algebraMap R S) y = z
Z : ↥I := ⟨y, ⋯⟩
⊢ z * (algebraMap R S) ↑(Z, 1).2 = (algebraMap R S) ↑(Z, 1).1