R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
⊢ ∀ (x_1 : P'),
    x_1 ∈ ↑(canonicalEquiv S P P') (spanSingleton S x) ↔
      x_1 ∈ spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
⊢ ↑(canonicalEquiv S P P') (spanSingleton S x) =
    spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
apply SetLike.ext_iff.mpr
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
⊢ y ∈ ↑(canonicalEquiv S P P') (spanSingleton S x) ↔
    y ∈ spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
⊢ ∀ (x_1 : P'),
    x_1 ∈ ↑(canonicalEquiv S P P') (spanSingleton S x) ↔
      x_1 ∈ spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
intro y
case mp
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)

case mpr
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ y ∈ ↑(canonicalEquiv S P P') (spanSingleton S x)
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
⊢ y ∈ ↑(canonicalEquiv S P P') (spanSingleton S x) ↔
    y ∈ spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
constructor <;> intro h
case mp
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x = y
case mp
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
rw [mem_spanSingleton]
case mp.intro.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x' ∈
    ↑(canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z,
    z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x =
      ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x'
case mp
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x = y
obtain ⟨x', hx', rfl⟩ := (mem_canonicalEquiv_apply _ _ _).mp h
case mp.intro.intro.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) ∈
    ↑(canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z_1,
    z_1 • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x =
      ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x)
case mp.intro.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x' ∈
    ↑(canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z,
    z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x =
      ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x'
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp hx'
case mp.intro.intro.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) ∈
    ↑(canonicalEquiv S P P') (spanSingleton S x)
⊢ z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x =
    ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x)
case mp.intro.intro.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) ∈
    ↑(canonicalEquiv S P P') (spanSingleton S x)
⊢ ∃ z_1,
    z_1 • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x =
      ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x)
use z
case mp.intro.intro.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) ∈
    ↑(canonicalEquiv S P P') (spanSingleton S x)
⊢ z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x =
    ↑(RingHom.id R) z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x
case mp.intro.intro.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) ∈
    ↑(canonicalEquiv S P P') (spanSingleton S x)
⊢ z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x =
    ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x)
rw [IsLocalization.map_smul]
no goals
case mp.intro.intro.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) ∈
    ↑(canonicalEquiv S P P') (spanSingleton S x)
⊢ z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x =
    ↑(RingHom.id R) z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x
rfl
case mpr
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ ∃ y_1,
    y_1 ∈ spanSingleton S x ∧
      ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) y_1 = y
case mpr
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ y ∈ ↑(canonicalEquiv S P P') (spanSingleton S x)
rw [mem_canonicalEquiv_apply]
case mpr.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h :
  z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x ∈
    spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ ∃ y,
    y ∈ spanSingleton S x ∧
      ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) y =
        z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x
case mpr
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
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) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ ∃ y_1,
    y_1 ∈ spanSingleton S x ∧
      ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) y_1 = y
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp h
case mpr.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h :
  z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x ∈
    spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ z • x ∈ spanSingleton S x ∧
    ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) =
      z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x
case mpr.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h :
  z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x ∈
    spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ ∃ y,
    y ∈ spanSingleton S x ∧
      ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) y =
        z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x
use z • x
case mpr.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h :
  z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x ∈
    spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) =
    z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x
case mpr.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h :
  z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x ∈
    spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ z • x ∈ spanSingleton S x ∧
    ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) =
      z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x
use (mem_spanSingleton _).mpr ⟨z, rfl⟩
no goals
case mpr.intro
R : Type u_2
inst✝⁹ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type ?u.1366656
inst✝⁶ : CommRing R₁
K : Type ?u.1366662
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
P' : Type u_1
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
h :
  z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x ∈
    spanSingleton S (↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x)
⊢ ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) (z • x) =
    z • ↑(IsLocalization.map P' (RingHom.id R) (_ : ∀ (y : R), y ∈ S → ↑(RingHom.id R) y ∈ S)) x
simp [IsLocalization.map_smul]