-- Mathlib/RingTheory/Localization/Integer.lean
theorem finsetIntegerMultiple_image [DecidableEq R] (s : Finset S) :
    algebraMap R S '' finsetIntegerMultiple M s = commonDenomOfFinset M s • (s : Set S)

Proof state:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach) ↔ x✝ ∈ commonDenomOfFinset M s • ↑s

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach) → x✝ ∈ commonDenomOfFinset M s • ↑s

case h.mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
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) '' ↑s.attach)

Proof state:
case h.mpr.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : S
hx : x ∈ ↑s
⊢ (fun x => ↑(commonDenomOfFinset M s) • x) x ∈ ⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach)

Tactic:
exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple M s id _⟩

Result:
no goals

Proof state:
case h.mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
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) '' ↑s.attach)

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.mpr.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : S
hx : x ∈ ↑s
⊢ (fun x => ↑(commonDenomOfFinset M s) • x) x ∈ ⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach) = commonDenomOfFinset M s • ↑s

Tactic:
ext

Result:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach) ↔ x✝ ∈ commonDenomOfFinset M s • ↑s

Proof state:
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : { x // x ∈ s }
⊢ commonDenom M s id • id ↑x ∈ commonDenomOfFinset M s • ↑s

Tactic:
exact Set.mem_image_of_mem _ x.prop

Result:
no goals

Proof state:
case h.mp
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach) → x✝ ∈ commonDenomOfFinset M s • ↑s

Tactic:
rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
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

Proof state:
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
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

Tactic:
rw [map_integerMultiple]

Result:
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : { x // x ∈ s }
⊢ commonDenom M s id • id ↑x ∈ commonDenomOfFinset M s • ↑s

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ↑(Finset.image (fun t => integerMultiple M s id t) s.attach) = commonDenomOfFinset M s • ↑s

Tactic:
rw [Finset.coe_image]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑s.attach) = commonDenomOfFinset M s • ↑s

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ↑(finsetIntegerMultiple M s) = commonDenomOfFinset M s • ↑s

Tactic:
delta finsetIntegerMultiple commonDenom

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ↑(Finset.image (fun t => integerMultiple M s id t) s.attach) = commonDenomOfFinset M s • ↑s