-- Mathlib/RingTheory/Localization/Integer.lean
theorem exist_integer_multiples {ι : Type*} (s : Finset ι) (f : ι → S) :
    ∃ b : M, ∀ i ∈ s, IsLocalization.IsInteger R ((b : R) • f i)

Proof state:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2

Tactic:
rw [mul_comm,Submonoid.coe_finset_prod,
  ← Finset.prod_insert (f := fun i => ((sec M (f i)).snd : R)) (s.not_mem_erase i),
  Finset.insert_erase hi]

Result:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ∏ x ∈ s, ↑(sec M (f x)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2

Proof state:
case refine_2
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2) • f i = ↑(∏ i ∈ s, (sec M (f i)).2) • f i

Tactic:
congr 2

Result:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2 = ↑(∏ i ∈ s, (sec M (f i)).2)

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

Tactic:
haveI := Classical.propDecidable

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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
⊢ ∃ b, ∀ i ∈ s, IsInteger R (↑b • f i)

Proof state:
case refine_1
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ R

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

Result:
no goals

Proof state:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2 = ↑(∏ i ∈ s, (sec M (f i)).2)

Tactic:
refine _root_.trans ?_ (map_prod (Submonoid.subtype M) _ _).symm

Result:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2

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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
⊢ ∃ b, ∀ i ∈ s, IsInteger R (↑b • f i)

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

Result:
case refine_1
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ R

case refine_2
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (algebraMap R S) ?refine_1 = ↑(∏ i ∈ s, (sec M (f i)).2) • f i

Proof state:
case refine_2
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (algebraMap R S) (↑(∏ j ∈ s.erase i, (sec M (f j)).2) * (sec M (f i)).1) = ↑(∏ i ∈ s, (sec M (f i)).2) • f i

Tactic:
rw [RingHom.map_mul, sec_spec', ← mul_assoc, ← (algebraMap R S).map_mul, ← Algebra.smul_def]

Result:
case refine_2
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j ∈ s.erase i, (sec M (f j)).2) * ↑(sec M (f i)).2) • f i = ↑(∏ i ∈ s, (sec M (f i)).2) • f i

Proof state:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ∏ x ∈ s, ↑(sec M (f x)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2

Tactic:
rfl

Result:
no goals