R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ↑(algebraMap R S) '' ↑(Finset.image (fun t => integerMultiple M s id t) (Finset.attach s)) =
    commonDenomOfFinset M s • ↑s
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ↑(algebraMap R S) '' ↑(finsetIntegerMultiple M s) = commonDenomOfFinset M s • ↑s
delta finsetIntegerMultiple commonDenom
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) = commonDenomOfFinset M s • ↑s
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ↑(algebraMap R S) '' ↑(Finset.image (fun t => integerMultiple M s id t) (Finset.attach s)) =
    commonDenomOfFinset M s • ↑s
rw [Finset.coe_image]
case h
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) ↔
    x✝ ∈ commonDenomOfFinset M s • ↑s
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) = commonDenomOfFinset M s • ↑s
ext
case h.mp
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) →
    x✝ ∈ commonDenomOfFinset M s • ↑s

case h.mpr
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ commonDenomOfFinset M s • ↑s →
    x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s))
case h
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) ↔
    x✝ ∈ commonDenomOfFinset M s • ↑s
constructor
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : { x // x ∈ s }
⊢ ↑(algebraMap R S) ((fun t => integerMultiple M s id t) x) ∈ commonDenomOfFinset M s • ↑s
case h.mp
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) →
    x✝ ∈ commonDenomOfFinset M s • ↑s
rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : { x // x ∈ s }
⊢ commonDenom M s id • id ↑x ∈ commonDenomOfFinset M s • ↑s
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : { x // x ∈ s }
⊢ ↑(algebraMap R S) ((fun t => integerMultiple M s id t) x) ∈ commonDenomOfFinset M s • ↑s
rw [map_integerMultiple]
no goals
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : { x // x ∈ s }
⊢ commonDenom M s id • id ↑x ∈ commonDenomOfFinset M s • ↑s
exact Set.mem_image_of_mem _ x.prop
case h.mpr.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : S
hx : x ∈ ↑s
⊢ (fun x => ↑(Submonoid.subtype M) (commonDenomOfFinset M s) • x) x ∈
    ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s))
case h.mpr
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ commonDenomOfFinset M s • ↑s →
    x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s))
rintro ⟨x, hx, rfl⟩
no goals
case h.mpr.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47772
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : S
hx : x ∈ ↑s
⊢ (fun x => ↑(Submonoid.subtype M) (commonDenomOfFinset M s) • x) x ∈
    ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s))
exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple M s id _⟩