case intro
R : Type u_2
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.28129
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
ι : Type u_1
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
R : Type u_2
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.28129
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
ι : Type u_1
inst✝ : Finite ι
f : ι → S
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
cases nonempty_fintype ι
case intro.intro
R : Type u_2
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.28129
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
ι : Type u_1
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
b : { x // x ∈ M }
hb : ∀ (i : ι), i ∈ Finset.univ → IsInteger R (↑b • f i)
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
case intro
R : Type u_2
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.28129
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
ι : Type u_1
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
obtain ⟨b, hb⟩ := exist_integer_multiples M Finset.univ f
no goals
case intro.intro
R : Type u_2
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.28129
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
ι : Type u_1
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
b : { x // x ∈ M }
hb : ∀ (i : ι), i ∈ Finset.univ → IsInteger R (↑b • f i)
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩