[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
s : { x // x ∈ S }
⊢ IsUnit (↑(algebraMap A K) ↑s)
[PROOFSTEP]
apply IsLocalization.map_units K (⟨s.1, hS s.2⟩ : A⁰)
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
src✝ : B →+* K := IsLocalization.lift (_ : ∀ (s : { x // x ∈ S }), IsUnit (↑(algebraMap A K) ↑s))
a : A
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : B), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap A B) a) =
    ↑(algebraMap A K) a
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : K
⊢ x ∈ AlgHom.range (mapToFractionRing K S B hS) →
    ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : B
⊢ ∃ a s hs, ↑↑(mapToFractionRing K S B hS) x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }
[PROOFSTEP]
obtain ⟨a, s, rfl⟩ := IsLocalization.mk'_surjective S x
[GOAL]
case intro.intro.intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
s : { x // x ∈ S }
⊢ ∃ a_1 s_1 hs,
    ↑↑(mapToFractionRing K S B hS) (IsLocalization.mk' B a s) =
      IsLocalization.mk' K a_1 { val := s_1, property := (_ : s_1 ∈ A⁰) }
[PROOFSTEP]
use a, s, s.2
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a : A
s : { x // x ∈ S }
⊢ ↑↑(mapToFractionRing K S B hS) (IsLocalization.mk' B a s) =
    IsLocalization.mk' K a { val := ↑s, property := (_ : ↑s ∈ A⁰) }
[PROOFSTEP]
apply IsLocalization.lift_mk'
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
x : K
⊢ (∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }) →
    x ∈ AlgHom.range (mapToFractionRing K S B hS)
[PROOFSTEP]
rintro ⟨a, s, hs, rfl⟩
[GOAL]
case intro.intro.intro
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) } ∈ AlgHom.range (mapToFractionRing K S B hS)
[PROOFSTEP]
use IsLocalization.mk' _ a ⟨s, hs⟩
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ ↑↑(mapToFractionRing K S B hS) (IsLocalization.mk' B a { val := s, property := hs }) =
    IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }
[PROOFSTEP]
apply IsLocalization.lift_mk'
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
⊢ Function.Bijective ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS))
[PROOFSTEP]
refine' ⟨fun a b h => _, Set.surjective_onto_range⟩
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a b : B
h : ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) a = ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) b
⊢ a = b
[PROOFSTEP]
refine' (IsLocalization.lift_injective_iff _).2 (fun a b => _) (Subtype.ext_iff.1 h)
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
a✝ b✝ : B
h : ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) a✝ = ↑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) b✝
a b : A
⊢ ↑(algebraMap A B) a = ↑(algebraMap A B) b ↔ ↑(algebraMap A K) a = ↑(algebraMap A K) b
[PROOFSTEP]
exact ⟨fun h => congr_arg _ (IsLocalization.injective _ hS h), fun h => congr_arg _ (IsFractionRing.injective A K h)⟩
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
⊢ {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }} =
    ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
x✝ : K
⊢ x✝ ∈ {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }} ↔
    x✝ ∈ ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))
[PROOFSTEP]
symm
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
x✝ : K
⊢ x✝ ∈ ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS)) ↔
    x✝ ∈ {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }}
[PROOFSTEP]
apply mem_range_mapToFractionRing_iff
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S { x // x ∈ subalgebra K S hS }
[PROOFSTEP]
dsimp only [Localization.subalgebra]
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S
    { x //
      x ∈
        Subalgebra.copy (AlgHom.range (mapToFractionRing K S (Localization S) hS))
          {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }}
          (_ :
            {x | ∃ a s hs, x = IsLocalization.mk' K a { val := s, property := (_ : s ∈ A⁰) }} =
              ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))) }
[PROOFSTEP]
rw [Subalgebra.copy_eq]
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S { x // x ∈ AlgHom.range (mapToFractionRing K S (Localization S) hS) }
[PROOFSTEP]
infer_instance
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
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)⁻¹
[PROOFSTEP]
rw [mem_range_mapToFractionRing_iff]
[GOAL]
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
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)⁻¹
[PROOFSTEP]
convert Iff.rfl
[GOAL]
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
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⁰) }
[PROOFSTEP]
congr
[GOAL]
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
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⁰) })⁻¹
[PROOFSTEP]
rw [Units.val_inv_eq_inv_val]
[GOAL]
case h.e'_2.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_3.e_a
A : Type u_1
K : Type u_2
inst✝⁶ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝⁵ : Field K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
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⁰) }))⁻¹
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹} =
    ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹} ↔
    x✝ ∈ ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))
[PROOFSTEP]
symm
[GOAL]
case h
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS)) ↔
    x✝ ∈ {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹}
[PROOFSTEP]
apply mem_range_mapToFractionRing_iff_ofField
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S { x // x ∈ ofField K S hS }
[PROOFSTEP]
dsimp only [Localization.subalgebra.ofField]
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S
    { x //
      x ∈
        Subalgebra.copy (AlgHom.range (mapToFractionRing K S (Localization S) hS))
          {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹}
          (_ :
            {x | ∃ a s x_1, x = ↑(algebraMap A K) a * (↑(algebraMap A K) s)⁻¹} =
              ↑(AlgHom.range (mapToFractionRing K S (Localization S) hS))) }
[PROOFSTEP]
rw [Subalgebra.copy_eq]
[GOAL]
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S { x // x ∈ AlgHom.range (mapToFractionRing K S (Localization S) hS) }
[PROOFSTEP]
infer_instance
