R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
⊢ ∃ b, ∀ (i : ι), i ∈ s → IsInteger R (↑b • f i)
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
⊢ ∃ b, ∀ (i : ι), i ∈ s → IsInteger R (↑b • f i)
haveI := Classical.propDecidable
case refine'_1
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ R

case refine'_2
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(algebraMap R S) ?refine'_1 = ↑(∏ i in s, (sec M (f i)).snd) • f i
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
⊢ ∃ b, ∀ (i : ι), i ∈ s → IsInteger R (↑b • f i)
refine' ⟨∏ i in s, (sec M (f i)).2, fun i hi => ⟨_, _⟩⟩
case refine'_2
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd) • f i = ↑(∏ i in s, (sec M (f i)).snd) • f i
case refine'_2
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(algebraMap R S) (↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * (sec M (f i)).fst) =
    ↑(∏ i in s, (sec M (f i)).snd) • f i
rw [RingHom.map_mul, sec_spec', ← mul_assoc, ← (algebraMap R S).map_mul, ← Algebra.smul_def]
case refine'_2.e_a
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd = ↑(∏ i in s, (sec M (f i)).snd)
case refine'_2
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd) • f i = ↑(∏ i in s, (sec M (f i)).snd) • f i
congr 2
case refine'_2.e_a
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd =
    ∏ x in s, ↑(Submonoid.subtype M) (sec M (f x)).snd
case refine'_2.e_a
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd = ↑(∏ i in s, (sec M (f i)).snd)
refine' _root_.trans _ ((Submonoid.subtype M).map_prod _ _).symm
case refine'_2.e_a
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ∏ x in s, ↑(sec M (f x)).snd = ∏ x in s, ↑(Submonoid.subtype M) (sec M (f x)).snd
case refine'_2.e_a
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd =
    ∏ x in s, ↑(Submonoid.subtype M) (sec M (f x)).snd
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]
no goals
case refine'_2.e_a
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ∏ x in s, ↑(sec M (f x)).snd = ∏ x in s, ↑(Submonoid.subtype M) (sec M (f x)).snd
rfl
no goals
case refine'_1
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.23842
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_1
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ R
exact (∏ j in s.erase i, (sec M (f j)).2) * (sec M (f i)).1