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)

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 : Type u
inst✝³ : CommRing R
S : Submonoid R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
⊢ (#L) ≤ (#R)
cases fintypeOrInfinite R
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)
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)
erw [← Cardinal.mul_eq_self <| Cardinal.aleph0_le_mk R]
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)
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)
set f : R × R → L := fun aa => IsLocalization.mk' _ aa.1 (if h : aa.2 ∈ S then ⟨aa.2, h⟩ else 1)
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
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)
refine' @Cardinal.mk_le_of_surjective _ _ f fun a => _
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
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
obtain ⟨x, y, h⟩ := IsLocalization.mk'_surjective S a
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
⊢ f (x, ↑y) = a
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
use (x, y)
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
⊢ mk' L x (if h : ↑y ∈ S then { val := ↑y, property := h } else 1) = a
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
⊢ f (x, ↑y) = a
dsimp
no goals
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
⊢ mk' L x (if h : ↑y ∈ S then { val := ↑y, property := h } else 1) = a
rwa [dif_pos <| show ↑y ∈ S from y.2, SetLike.eta]
no goals
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)
exact Cardinal.mk_le_of_surjective (IsArtinianRing.localization_surjective S _)