case intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
rintro ⟨x, rfl⟩
case intro.intro.intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
case intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
obtain ⟨a, s, rfl⟩ := IsLocalization.mk'_surjective S x
case intro.intro.intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
case intro.intro.intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
use a, s, s.2
no goals
case intro.intro.intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
apply IsLocalization.lift_mk'
case intro.intro.intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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)
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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)
rintro ⟨a, s, hs, rfl⟩
case intro.intro.intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
case intro.intro.intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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)
use IsLocalization.mk' _ a ⟨s, hs⟩
no goals
case intro.intro.intro
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_1
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⁰) }
apply IsLocalization.lift_mk'