-- Mathlib/RingTheory/Localization/Pi.lean
theorem iff_map_piEvalRingHom [Finite ι] :
    IsLocalization M S' ↔ IsLocalization (.pi .univ fun i ↦ M.map (Pi.evalRingHom R i)) S' :=
  iff_of_le_of_exists_dvd M _ (fun m hm i _ ↦ ⟨m, hm, rfl⟩) fun n hn ↦ by
    choose m mem eq using hn
    have := Fintype.ofFinite ι
    refine ⟨∏ i, m i ⟨⟩, prod_mem fun i _ ↦ mem i _, pi_dvd_iff.mpr fun i ↦ ?_⟩
    rw [Fintype.prod_apply]
    exact (eq i ⟨⟩).symm.dvd.trans (Finset.dvd_prod_of_mem _ <| Finset.mem_univ _)

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
⊢ ∃ m ∈ M, n ∣ m

Tactic:
have := Fintype.ofFinite ι

Result:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
⊢ ∃ m ∈ M, n ∣ m

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ ∏ c : ι, m c True.intro i

Tactic:
exact (eq i ⟨⟩).symm.dvd.trans (Finset.dvd_prod_of_mem _ <| Finset.mem_univ _)

Result:
no goals

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
hn : n ∈ Submonoid.pi Set.univ fun i => Submonoid.map (Pi.evalRingHom R i) M
⊢ ∃ m ∈ M, n ∣ m

Tactic:
choose m mem eq using hn

Result:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
⊢ ∃ m ∈ M, n ∣ m

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ (∏ i : ι, m i True.intro) i

Tactic:
rw [Fintype.prod_apply]

Result:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ ∏ c : ι, m c True.intro i

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
⊢ ∃ m ∈ M, n ∣ m

Tactic:
refine ⟨∏ i, m i ⟨⟩, prod_mem fun i _ ↦ mem i _, pi_dvd_iff.mpr fun i ↦ ?_⟩

Result:
ι : Type u_1
R : ι → Type u_2
inst✝³ : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst✝² : CommSemiring S'
inst✝¹ : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst✝ : Finite ι
n : (i : ι) → R i
m : (i : ι) → i ∈ Set.univ → (i : ι) → R i
mem : ∀ (i : ι) (a : i ∈ Set.univ), m i a ∈ ↑M
eq : ∀ (i : ι) (a : i ∈ Set.univ), (Pi.evalRingHom R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ (∏ i : ι, m i True.intro) i