no goals
R : Type ?u.339407
inst✝⁴ : CommSemiring R
M : Submonoid R
S✝ : Type ?u.339596
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type ?u.339776
inst✝¹ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
S : Type ?u.339916
inst✝ : CommSemiring S
J : Ideal S
hJ : Ideal.IsPrime J
K : Ideal P
hK : Ideal.IsPrime K
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ I = Ideal.comap (RingHom.comp g f) K
rw [hIJ, hJK, Ideal.comap_comap f g]
no goals
R : Type u_3
inst✝⁴ : CommSemiring R
M : Submonoid R
S✝ : Type ?u.339596
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
P : Type u_2
inst✝¹ : CommSemiring P
I : Ideal R
hI : Ideal.IsPrime I
S : Type u_1
inst✝ : CommSemiring S
J : Ideal S
hJ : Ideal.IsPrime J
K : Ideal P
hK : Ideal.IsPrime K
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
r : R
⊢ ↑(RingHom.comp (localRingHom J K g hJK) (localRingHom I J f hIJ)) (↑(algebraMap R (Localization.AtPrime I)) r) =
    ↑(algebraMap ((fun x => P) r) (Localization.AtPrime K)) (↑(RingHom.comp g f) r)
simp only [Function.comp_apply, RingHom.coe_comp, localRingHom_to_map]