R : Type u_6
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_5
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
hy : M ≤ Submonoid.comap g T
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
A : Type u_1
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_2
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ ↑(map W l hl) (↑(map Q g hy) x) = ↑(RingHom.comp (map W l hl) (map Q g hy)) x
R : Type u_6
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_5
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
hy : M ≤ Submonoid.comap g T
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
A : Type u_1
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_2
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ ↑(map W l hl) (↑(map Q g hy) x) = ↑(map W (RingHom.comp l g) (_ : ∀ (x : R), x ∈ M → ↑g x ∈ Submonoid.comap l U)) x
rw [← map_comp_map (Q := Q) hy hl]
no goals
R : Type u_6
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_5
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
hy : M ≤ Submonoid.comap g T
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
A : Type u_1
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_2
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ ↑(map W l hl) (↑(map Q g hy) x) = ↑(RingHom.comp (map W l hl) (map Q g hy)) x
rfl