-- Mathlib/Algebra/Module/LocalizedModule/Int.lean
theorem exist_integer_multiples {ι : Type*} (s : Finset ι) (g : ι → M') :
    ∃ b : S, ∀ i ∈ s, IsInteger f (b.val • g i)

Proof state:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ ↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) = ∏ i ∈ s, ↑(sec i).2

Tactic:
simp only [Submonoid.coe_mul, Submonoid.coe_finset_prod, mul_comm]

Result:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ ↑(sec i).2 * ∏ i ∈ s.erase i, ↑(sec i).2 = ∏ i ∈ s, ↑(sec i).2

Proof state:
case refine_2
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ ↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) • g i = (∏ i ∈ s, ↑(sec i).2) • g i

Tactic:
congr

Result:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ ↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) = ∏ i ∈ s, ↑(sec i).2

Proof state:
case refine_2
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ f ((∏ j ∈ s.erase i, (sec j).2) • (sec i).1) = ↑(∏ i ∈ s, (sec i).2) • g i

Tactic:
simp only [LinearMap.map_smul_of_tower, Submonoid.coe_finset_prod]

Result:
case refine_2
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ (∏ j ∈ s.erase i, (sec j).2) • f (sec i).1 = (∏ i ∈ s, ↑(sec i).2) • g i

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
ι : Type u_4
s : Finset ι
g : ι → M'
⊢ ∃ b, ∀ i ∈ s, IsInteger f (↑b • g i)

Tactic:
choose sec hsec using (fun i ↦ IsLocalizedModule.surj S f (g i))

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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
⊢ ∃ b, ∀ i ∈ s, IsInteger f (↑b • g i)

Proof state:
case refine_1
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ M

Tactic:
exact (∏ j ∈ s.erase i, (sec j).2) • (sec i).1

Result:
no goals

Proof state:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ ↑(sec i).2 * ∏ i ∈ s.erase i, ↑(sec i).2 = ∏ i ∈ s, ↑(sec i).2

Tactic:
rw [← Finset.prod_insert (f := fun i ↦ ((sec i).snd).val) (s.not_mem_erase i),
  Finset.insert_erase hi]

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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
⊢ ∃ b, ∀ i ∈ s, IsInteger f (↑b • g i)

Tactic:
refine ⟨∏ i ∈ s, (sec i).2, fun i hi => ⟨?_, ?_⟩⟩

Result:
case refine_1
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ M

case refine_2
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ f ?refine_1 = ↑(∏ i ∈ s, (sec i).2) • g i

Proof state:
case refine_2
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ (∏ j ∈ s.erase i, (sec j).2) • f (sec i).1 = (∏ i ∈ s, ↑(sec i).2) • g i

Tactic:
rw [← hsec, ← mul_smul, Submonoid.smul_def]

Result:
case refine_2
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ ↑((∏ j ∈ s.erase i, (sec j).2) * (sec i).2) • g i = (∏ i ∈ s, ↑(sec i).2) • g i