[GOAL]
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ #L ≤ #R
[PROOFSTEP]
classical
cases fintypeOrInfinite R
· exact Cardinal.mk_le_of_surjective (IsArtinianRing.localization_surjective S _)
erw [← Cardinal.mul_eq_self <| Cardinal.aleph0_le_mk R]
set f : R × R → L := fun aa => IsLocalization.mk' _ aa.1 (if h : aa.2 ∈ S then ⟨aa.2, h⟩ else 1)
refine' @Cardinal.mk_le_of_surjective _ _ f fun a => _
obtain ⟨x, y, h⟩ := IsLocalization.mk'_surjective S a
use(x, y)
dsimp
rwa [dif_pos <| show ↑y ∈ S from y.2, SetLike.eta]
[GOAL]
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ #L ≤ #R
[PROOFSTEP]
cases fintypeOrInfinite R
[GOAL]
case inl
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Fintype R
⊢ #L ≤ #R
[PROOFSTEP]
exact Cardinal.mk_le_of_surjective (IsArtinianRing.localization_surjective S _)
[GOAL]
case inr
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
⊢ #L ≤ #R
[PROOFSTEP]
erw [← Cardinal.mul_eq_self <| Cardinal.aleph0_le_mk R]
[GOAL]
case inr
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
⊢ #L ≤ #R * #R
[PROOFSTEP]
set f : R × R → L := fun aa => IsLocalization.mk' _ aa.1 (if h : aa.2 ∈ S then ⟨aa.2, h⟩ else 1)
[GOAL]
case inr
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
⊢ #L ≤ #R * #R
[PROOFSTEP]
refine' @Cardinal.mk_le_of_surjective _ _ f fun a => _
[GOAL]
case inr
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
a : L
⊢ ∃ a_1, f a_1 = a
[PROOFSTEP]
obtain ⟨x, y, h⟩ := IsLocalization.mk'_surjective S a
[GOAL]
case inr.intro.intro
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
a : L
x : R
y : { x // x ∈ S }
h : mk' L x y = a
⊢ ∃ a_1, f a_1 = a
[PROOFSTEP]
use(x, y)
[GOAL]
case h
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
a : L
x : R
y : { x // x ∈ S }
h : mk' L x y = a
⊢ f (x, ↑y) = a
[PROOFSTEP]
dsimp
[GOAL]
case h
R : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
val✝ : Infinite R
f : R × R → L := fun aa => mk' L aa.fst (if h : aa.snd ∈ S then { val := aa.snd, property := h } else 1)
a : L
x : R
y : { x // x ∈ S }
h : mk' L x y = a
⊢ mk' L x (if h : ↑y ∈ S then { val := ↑y, property := h } else 1) = a
[PROOFSTEP]
rwa [dif_pos <| show ↑y ∈ S from y.2, SetLike.eta]
