-- Mathlib/Algebra/Module/LocalizedModule/Int.lean
theorem finsetIntegerMultiple_image [DecidableEq M] (s : Finset M') :
    f '' finsetIntegerMultiple S f s = commonDenomOfFinset S f s • (s : Set M')

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' ↑(finsetIntegerMultiple S f s) = commonDenomOfFinset S f s • ↑s

Tactic:
delta finsetIntegerMultiple commonDenom

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' ↑(Finset.image (fun t => integerMultiple S f s id t) s.attach) = commonDenomOfFinset S f s • ↑s

Proof state:
case h.mpr
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ commonDenomOfFinset S f s • ↑s → x✝ ∈ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach)

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.mpr.intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x : M'
hx : x ∈ ↑s
⊢ (fun x => ↑(commonDenomOfFinset S f s) • x) x ∈ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach)

Proof state:
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x : { x // x ∈ s }
⊢ f ((fun t => integerMultiple S f s id t) x) ∈ commonDenomOfFinset S f s • ↑s

Tactic:
rw [map_integerMultiple]

Result:
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x : { x // x ∈ s }
⊢ commonDenom S f s id • id ↑x ∈ commonDenomOfFinset S f s • ↑s

Proof state:
case h.mpr.intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x : M'
hx : x ∈ ↑s
⊢ (fun x => ↑(commonDenomOfFinset S f s) • x) x ∈ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach)

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

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach) = commonDenomOfFinset S f s • ↑s

Tactic:
ext

Result:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach) ↔ x✝ ∈ commonDenomOfFinset S f s • ↑s

Proof state:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach) ↔ x✝ ∈ commonDenomOfFinset S f s • ↑s

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach) → x✝ ∈ commonDenomOfFinset S f s • ↑s

case h.mpr
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ commonDenomOfFinset S f s • ↑s → x✝ ∈ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' ↑(Finset.image (fun t => integerMultiple S f s id t) s.attach) = commonDenomOfFinset S f s • ↑s

Tactic:
rw [Finset.coe_image]

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach) = commonDenomOfFinset S f s • ↑s

Proof state:
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x : { x // x ∈ s }
⊢ commonDenom S f s id • id ↑x ∈ commonDenomOfFinset S f 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
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' ((fun t => integerMultiple S f s id t) '' ↑s.attach) → x✝ ∈ commonDenomOfFinset S f s • ↑s

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

Result:
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x : { x // x ∈ s }
⊢ f ((fun t => integerMultiple S f s id t) x) ∈ commonDenomOfFinset S f s • ↑s