-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem canonicalEquiv_spanSingleton {P'} [CommRing P'] [Algebra R P'] [IsLocalization S P']
    (x : P) :
    canonicalEquiv S P P' (spanSingleton S x) =
      spanSingleton S
        (IsLocalization.map P' (RingHom.id R)
          (fun y (hy : y ∈ S) => show RingHom.id R y ∈ S from hy) x)

Proof state:
case mp
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z, z • (IsLocalization.map P' (RingHom.id R) ⋯) x = y

Tactic:
obtain ⟨x', hx', rfl⟩ := (mem_canonicalEquiv_apply _ _ _).mp h

Result:
case mp.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x x' : P
hx' : x' ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) x' ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z, z • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) x'

Proof state:
case mp.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
hx' : z • x ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z_1, z_1 • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) (z • x)

Tactic:
use z

Result:
case h
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
hx' : z • x ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ z • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) (z • x)

Proof state:
case mp.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x x' : P
hx' : x' ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) x' ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z, z • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) x'

Tactic:
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp hx'

Result:
case mp.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
hx' : z • x ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z_1, z_1 • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) (z • x)

Proof state:
case h
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h : z • (IsLocalization.map P' (RingHom.id R) ⋯) x ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ z • x ∈ spanSingleton S x ∧
    (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) = z • (IsLocalization.map P' (RingHom.id R) ⋯) x

Tactic:
use (mem_spanSingleton _).mpr ⟨z, rfl⟩

Result:
case right
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h : z • (IsLocalization.map P' (RingHom.id R) ⋯) x ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) = z • (IsLocalization.map P' (RingHom.id R) ⋯) x

Proof state:
case mpr
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ ∃ y_1 ∈ spanSingleton S x, (IsLocalization.map P' (RingHom.id R) ⋯) y_1 = y

Tactic:
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp h

Result:
case mpr.intro
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h : z • (IsLocalization.map P' (RingHom.id R) ⋯) x ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ ∃ y ∈ spanSingleton S x, (IsLocalization.map P' (RingHom.id R) ⋯) y = z • (IsLocalization.map P' (RingHom.id R) ⋯) x

Proof state:
case mpr.intro
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h : z • (IsLocalization.map P' (RingHom.id R) ⋯) x ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ ∃ y ∈ spanSingleton S x, (IsLocalization.map P' (RingHom.id R) ⋯) y = z • (IsLocalization.map P' (RingHom.id R) ⋯) x

Tactic:
use z • x

Result:
case h
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h : z • (IsLocalization.map P' (RingHom.id R) ⋯) x ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ z • x ∈ spanSingleton S x ∧
    (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) = z • (IsLocalization.map P' (RingHom.id R) ⋯) x

Proof state:
case mpr
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ y ∈ (canonicalEquiv S P P') (spanSingleton S x)

Tactic:
rw [mem_canonicalEquiv_apply]

Result:
case mpr
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ ∃ y_1 ∈ spanSingleton S x, (IsLocalization.map P' (RingHom.id R) ⋯) y_1 = y

Proof state:
case mp
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)

Tactic:
rw [mem_spanSingleton]

Result:
case mp
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z, z • (IsLocalization.map P' (RingHom.id R) ⋯) x = y