no goals
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type u_2
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.880849
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
I : FractionalIdeal S P'
⊢ ↑(canonicalEquiv S P P') (↑(canonicalEquiv S P' P) I) = I
rw [← canonicalEquiv_symm, RingEquiv.apply_symm_apply]