case a
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
P' : Type u_4
inst✝⁶ : CommRing P'
inst✝⁵ : Algebra R P'
loc' : IsLocalization S P'
P''✝ : Type ?u.928438
inst✝⁴ : CommRing P''✝
inst✝³ : Algebra R P''✝
loc'' : IsLocalization S P''✝
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
P'' : Type u_1
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
x✝ : P''
⊢ x✝ ∈ ↑(canonicalEquiv S P' P'') (↑(canonicalEquiv S P P') I) ↔ x✝ ∈ ↑(canonicalEquiv S P P'') I
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
P' : Type u_4
inst✝⁶ : CommRing P'
inst✝⁵ : Algebra R P'
loc' : IsLocalization S P'
P''✝ : Type ?u.928438
inst✝⁴ : CommRing P''✝
inst✝³ : Algebra R P''✝
loc'' : IsLocalization S P''✝
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
P'' : Type u_1
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
⊢ ↑(canonicalEquiv S P' P'') (↑(canonicalEquiv S P P') I) = ↑(canonicalEquiv S P P'') I
ext
no goals
case a
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
P' : Type u_4
inst✝⁶ : CommRing P'
inst✝⁵ : Algebra R P'
loc' : IsLocalization S P'
P''✝ : Type ?u.928438
inst✝⁴ : CommRing P''✝
inst✝³ : Algebra R P''✝
loc'' : IsLocalization S P''✝
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
P'' : Type u_1
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
x✝ : P''
⊢ x✝ ∈ ↑(canonicalEquiv S P' P'') (↑(canonicalEquiv S P P') I) ↔ x✝ ∈ ↑(canonicalEquiv S P P'') I
simp only [IsLocalization.map_map, RingHomInvPair.comp_eq₂, mem_canonicalEquiv_apply,
  exists_prop, exists_exists_and_eq_and]