A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ (∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }) ↔
    ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ x ∈ AlgHom.range (mapToFractionRing K S B hS) ↔ ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹
rw [mem_range_mapToFractionRing_iff]
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ↑(algebraMap A K) x✝² * (↑(algebraMap A K) x✝¹)⁻¹ =
    IsLocalization.mk' K x✝² { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) }
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
⊢ (∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }) ↔
    ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹
convert Iff.rfl
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (↑(algebraMap A K) x✝¹)⁻¹ =
    ↑(↑(IsUnit.liftRight
              (MonoidHom.restrict (Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
              (_ :
                ∀ (y : { x // x ∈ A⁰ }),
                  IsUnit (↑(Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) ↑y)))
          { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) })⁻¹
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ ↑(algebraMap A K) x✝² * (↑(algebraMap A K) x✝¹)⁻¹ =
    IsLocalization.mk' K x✝² { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) }
congr
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (↑(algebraMap A K) x✝¹)⁻¹ =
    (↑(↑(IsUnit.liftRight
              (MonoidHom.restrict (Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
              (_ :
                ∀ (y : { x // x ∈ A⁰ }),
                  IsUnit (↑(Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) ↑y)))
          { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) }))⁻¹
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (↑(algebraMap A K) x✝¹)⁻¹ =
    ↑(↑(IsUnit.liftRight
              (MonoidHom.restrict (Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
              (_ :
                ∀ (y : { x // x ∈ A⁰ }),
                  IsUnit (↑(Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) ↑y)))
          { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) })⁻¹
rw [Units.val_inv_eq_inv_val]
no goals
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
x : K
x✝² x✝¹ : A
x✝ : x✝¹ ∈ S
⊢ (↑(algebraMap A K) x✝¹)⁻¹ =
    (↑(↑(IsUnit.liftRight
              (MonoidHom.restrict (Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
              (_ :
                ∀ (y : { x // x ∈ A⁰ }),
                  IsUnit (↑(Submonoid.LocalizationMap.toMap (IsLocalization.toLocalizationMap A⁰ K)) ↑y)))
          { val := x✝¹, property := (_ : x✝¹ ∈ A⁰) }))⁻¹
rfl