-- Mathlib/RingTheory/Localization/Basic.lean
theorem mapPiEvalRingHom_bijective : Bijective (mapPiEvalRingHom S)

Proof state:
case refine_1.intro.intro.intro.intro
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  mk' (Localization S) ((Pi.evalRingHom R i) r₁) ⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ =
    mk' (Localization S) ((Pi.evalRingHom R i) r₂) ⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ =
    mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂

Tactic:
rw [IsLocalization.eq] at eq ⊢

Result:
case refine_1.intro.intro.intro.intro
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  ∃ c,
    ↑c * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
      ↑c * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
⊢ ∃ c, ↑c * (↑s₂ * r₁) = ↑c * (↑s₁ * r₂)

Proof state:
case refine_1.intro.intro.intro.intro
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁) =
    (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂)
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ =
    mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂

Tactic:
simp_rw [map_mk'] at eq

Result:
case refine_1.intro.intro.intro.intro
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  mk' (Localization S) ((Pi.evalRingHom R i) r₁) ⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ =
    mk' (Localization S) ((Pi.evalRingHom R i) r₂) ⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ =
    mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂

Proof state:
case refine_2
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x : Localization S
⊢ ∃ a, (mapPiEvalRingHom S) a = x

Tactic:
obtain ⟨r, s, rfl⟩ := mk'_surjective S x

Result:
case refine_2.intro.intro
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r : R i
s : ↥S
⊢ ∃ a, (mapPiEvalRingHom S) a = mk' (Localization S) r s

Proof state:
case refine_1.intro.intro.intro.intro.intro
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
j : ι
⊢ (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₁ * r₂)) j

Tactic:
obtain rfl | ne := eq_or_ne j i

Result:
case refine_1.intro.intro.intro.intro.intro.inl
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
r₁ r₂ : (i : ι) → R i
j : ι
S : Submonoid (R j)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R j) S
s₁ s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R j) ↑s₂, ⋯⟩ * (Pi.evalRingHom R j) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R j) ↑s₁, ⋯⟩ * (Pi.evalRingHom R j) r₂)
⊢ (↑⟨update 0 j ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 j ↑s, ⋯⟩ * (↑s₁ * r₂)) j

case refine_1.intro.intro.intro.intro.intro.inr
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
j : ι
ne : j ≠ i
⊢ (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₁ * r₂)) j

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
⊢ update 0 i ↑s ∈ T

Tactic:
apply update_self i s.1 0 ▸ s.2

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro.inl
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
r₁ r₂ : (i : ι) → R i
j : ι
S : Submonoid (R j)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R j) S
s₁ s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R j) ↑s₂, ⋯⟩ * (Pi.evalRingHom R j) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R j) ↑s₁, ⋯⟩ * (Pi.evalRingHom R j) r₂)
⊢ (↑⟨update 0 j ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 j ↑s, ⋯⟩ * (↑s₁ * r₂)) j

Tactic:
simpa using hs

Result:
no goals

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
⊢ Bijective ⇑(mapPiEvalRingHom S)

Tactic:
refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩

Result:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x₁ x₂ : Localization (Submonoid.comap (Pi.evalRingHom R i) S)
eq : (mapPiEvalRingHom S) x₁ = (mapPiEvalRingHom S) x₂
⊢ x₁ = x₂

case refine_2
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x : Localization S
⊢ ∃ a, (mapPiEvalRingHom S) a = x

Proof state:
case refine_1.intro.intro.intro.intro.intro.inr
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
j : ι
ne : j ≠ i
⊢ (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₁ * r₂)) j

Tactic:
simp [update_of_ne ne]

Result:
no goals

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r : R i
s : ↥S
⊢ (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) (update 0 i r) ⟨update 0 i ↑s, ⋯⟩) =
    mk' (Localization S) r s

Tactic:
simp [map_mk']

Result:
no goals