R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.1037421
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.1037874
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ RingEquiv.trans (canonicalEquiv S P P) (canonicalEquiv S P P) = RingEquiv.refl (FractionalIdeal S P)
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.1037421
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.1037874
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ canonicalEquiv S P P = RingEquiv.refl (FractionalIdeal S P)
rw [← canonicalEquiv_trans_canonicalEquiv S P P]
case h.e'_2.h.e'_10
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.1037421
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.1037874
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ canonicalEquiv S P P = RingEquiv.symm (canonicalEquiv S P P)
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.1037421
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.1037874
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ RingEquiv.trans (canonicalEquiv S P P) (canonicalEquiv S P P) = RingEquiv.refl (FractionalIdeal S P)
convert(canonicalEquiv S P P).symm_trans_self
no goals
case h.e'_2.h.e'_10
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.1037421
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.1037874
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ canonicalEquiv S P P = RingEquiv.symm (canonicalEquiv S P P)
exact (canonicalEquiv_symm S P P).symm