-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem map_coeIdeal (I : Ideal R) : (I : FractionalIdeal S P).map g = I

Proof state:
case a.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ x ∈ map g ↑I → ∃ x' ∈ I, (algebraMap R P') x' = x

Tactic:
rintro ⟨_, ⟨y, hy, rfl⟩, rfl⟩

Result:
case a.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
y : R
hy : y ∈ ↑I
⊢ ∃ x' ∈ I, (algebraMap R P') x' = g.toLinearMap ((Algebra.linearMap R P) y)

Proof state:
case a
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ x ∈ map g ↑I ↔ x ∈ ↑I

Tactic:
simp only [mem_coeIdeal]

Result:
case a
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ x ∈ map g ↑I ↔ ∃ x' ∈ I, (algebraMap R P') x' = x

Proof state:
case a
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ x ∈ map g ↑I ↔ ∃ x' ∈ I, (algebraMap R P') x' = x

Tactic:
constructor

Result:
case a.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ x ∈ map g ↑I → ∃ x' ∈ I, (algebraMap R P') x' = x

case a.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ (∃ x' ∈ I, (algebraMap R P') x' = x) → x ∈ map g ↑I

Proof state:
case a.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ (∃ x' ∈ I, (algebraMap R P') x' = x) → x ∈ map g ↑I

Tactic:
rintro ⟨y, hy, rfl⟩

Result:
case a.mpr.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
y : R
hy : y ∈ I
⊢ (algebraMap R P') y ∈ map g ↑I

Proof state:
case a.mpr.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
y : R
hy : y ∈ I
⊢ (algebraMap R P') y ∈ map g ↑I

Tactic:
exact ⟨_, ⟨y, hy, rfl⟩, g.commutes y⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
⊢ map g ↑I = ↑I

Tactic:
ext x

Result:
case a
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
x : P'
⊢ x ∈ map g ↑I ↔ x ∈ ↑I

Proof state:
case a.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
g : P →ₐ[R] P'
I : Ideal R
y : R
hy : y ∈ ↑I
⊢ ∃ x' ∈ I, (algebraMap R P') x' = g.toLinearMap ((Algebra.linearMap R P) y)

Tactic:
exact ⟨y, hy, (g.commutes y).symm⟩

Result:
no goals