R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y) ↔ ∃ c, ↑c * x = ↑c * y
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ ↑(algebraMap R T) x = ↑(algebraMap R T) y ↔ ∃ c, ↑c * x = ↑c * y
rw [IsScalarTower.algebraMap_apply R S T, IsScalarTower.algebraMap_apply R S T,
  IsLocalization.eq_iff_exists N T]
case mp
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y) → ∃ c, ↑c * x = ↑c * y

case mpr
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y) ↔ ∃ c, ↑c * x = ↑c * y
constructor
case mp.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
⊢ ∃ c, ↑c * x = ↑c * y
case mp
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y) → ∃ c, ↑c * x = ↑c * y
rintro ⟨z, eq₁⟩
case mp.intro.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑(z', s).snd = ↑(algebraMap R S) (z', s).fst
⊢ ∃ c, ↑c * x = ↑c * y
case mp.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
⊢ ∃ c, ↑c * x = ↑c * y
rcases IsLocalization.surj M (z : S) with ⟨⟨z', s⟩, eq₂⟩
case mp.intro.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
⊢ ∃ c, ↑c * x = ↑c * y
case mp.intro.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑(z', s).snd = ↑(algebraMap R S) (z', s).fst
⊢ ∃ c, ↑c * x = ↑c * y
dsimp only at eq₂
case mp.intro.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
⊢ ∃ c, ↑c * x = ↑c * y

case this
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
⊢ ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
case mp.intro.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
⊢ ∃ c, ↑c * x = ↑c * y
suffices : (algebraMap R S) (x * z' : R) = (algebraMap R S) (y * z')
case mp.intro.intro.mk.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ∃ c, ↑c * x = ↑c * y
case mp.intro.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
⊢ ∃ c, ↑c * x = ↑c * y
obtain ⟨c, eq₃ : ↑c * (x * z') = ↑c * (y * z')⟩ := (IsLocalization.eq_iff_exists M S).mp this
case mp.intro.intro.mk.intro.refine_1
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑c * z' ∈ localizationLocalizationSubmodule M N

case mp.intro.intro.mk.intro.refine_2
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑{ val := ↑c * z', property := ?mp.intro.intro.mk.intro.refine_1 } * x =
    ↑{ val := ↑c * z', property := ?mp.intro.intro.mk.intro.refine_1 } * y
case mp.intro.intro.mk.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ∃ c, ↑c * x = ↑c * y
refine ⟨⟨c * z', ?_⟩, ?_⟩
case mp.intro.intro.mk.intro.refine_1
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ∃ y z, ↑(algebraMap R S) (↑c * z') = ↑y * ↑(algebraMap R S) ↑z
case mp.intro.intro.mk.intro.refine_1
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑c * z' ∈ localizationLocalizationSubmodule M N
rw [mem_localizationLocalizationSubmodule]
case mp.intro.intro.mk.intro.refine_1
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑(algebraMap R S) (↑c * z') = ↑z * ↑(algebraMap R S) ↑(c * s)
case mp.intro.intro.mk.intro.refine_1
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ∃ y z, ↑(algebraMap R S) (↑c * z') = ↑y * ↑(algebraMap R S) ↑z
refine ⟨z, c * s, ?_⟩
no goals
case mp.intro.intro.mk.intro.refine_1
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑(algebraMap R S) (↑c * z') = ↑z * ↑(algebraMap R S) ↑(c * s)
rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]
no goals
case mp.intro.intro.mk.intro.refine_2
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
this : ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
c : { x // x ∈ M }
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑{ val := ↑c * z', property := (_ : ↑c * z' ∈ localizationLocalizationSubmodule M N) } * x =
    ↑{ val := ↑c * z', property := (_ : ↑c * z' ∈ localizationLocalizationSubmodule M N) } * y
rwa [mul_comm _ z', mul_comm _ z', ← mul_assoc, ← mul_assoc] at eq₃
no goals
case this
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : { x // x ∈ N }
eq₁ : ↑z * ↑(algebraMap R S) x = ↑z * ↑(algebraMap R S) y
z' : R
s : { x // x ∈ M }
eq₂ : ↑z * ↑(algebraMap R S) ↑s = ↑(algebraMap R S) z'
⊢ ↑(algebraMap R S) (x * z') = ↑(algebraMap R S) (y * z')
rw [map_mul, map_mul, ← eq₂, ← mul_assoc, ← mul_assoc, mul_comm _ (z : S), eq₁,
mul_comm _ (z : S)]
case mpr.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
hc : c ∈ localizationLocalizationSubmodule M N
eq₁ : c * x = c * y
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
case mpr
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
rintro ⟨⟨c, hc⟩, eq₁ : c * x = c * y⟩
case mpr.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
hc : ∃ y z, ↑(algebraMap R S) c = ↑y * ↑(algebraMap R S) ↑z
eq₁ : c * x = c * y
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
case mpr.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
hc : c ∈ localizationLocalizationSubmodule M N
eq₁ : c * x = c * y
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
rw [mem_localizationLocalizationSubmodule] at hc
case mpr.intro.mk.intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
case mpr.intro.mk
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
hc : ∃ y z, ↑(algebraMap R S) c = ↑y * ↑(algebraMap R S) ↑z
eq₁ : c * x = c * y
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
rcases hc with ⟨z₁, z, eq₂⟩
case mpr.intro.mk.intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ↑z₁ * ↑(algebraMap R S) x = ↑z₁ * ↑(algebraMap R S) y
case mpr.intro.mk.intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ∃ c, ↑c * ↑(algebraMap R S) x = ↑c * ↑(algebraMap R S) y
use z₁
case mpr.intro.mk.intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ↑(algebraMap R S) ↑z * (↑z₁ * ↑(algebraMap R S) x) = ↑(algebraMap R S) ↑z * (↑z₁ * ↑(algebraMap R S) y)
case mpr.intro.mk.intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ↑z₁ * ↑(algebraMap R S) x = ↑z₁ * ↑(algebraMap R S) y
refine (IsLocalization.map_units S z).mul_right_inj.mp ?_
no goals
case mpr.intro.mk.intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.134353
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y c : R
eq₁ : c * x = c * y
z₁ : { x // x ∈ N }
z : { x // x ∈ M }
eq₂ : ↑(algebraMap R S) c = ↑z₁ * ↑(algebraMap R S) ↑z
⊢ ↑(algebraMap R S) ↑z * (↑z₁ * ↑(algebraMap R S) x) = ↑(algebraMap R S) ↑z * (↑z₁ * ↑(algebraMap R S) y)
rw [← mul_assoc, mul_comm _ (z₁ : S), ← eq₂, ← map_mul, eq₁, map_mul, eq₂, ← mul_assoc,
  mul_comm _ (z₁ : S)]