-- Mathlib/RingTheory/Localization/Basic.lean
theorem mapPiEvalRingHom_bijective : Bijective (mapPiEvalRingHom 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₂)
⊢ ∃ c, ↑c * (↑s₂ * r₁) = ↑c * (↑s₁ * r₂)

Tactic:
refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩

Result:
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

Proof state:
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₂

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

Result:
case refine_1.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
x₂ : Localization (Submonoid.comap (Pi.evalRingHom R i) S)
r₁ : (i : ι) → R i
s₁ : ↥T
eq : (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁) = (mapPiEvalRingHom S) x₂
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ = x₂

Proof state:
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

Tactic:
exact ⟨mk' (M := T) _ (update 0 i r) ⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩,
  by simp [map_mk']⟩

Result:
no goals

Proof state:
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
⊢ Bijective ⇑(mapPiEvalRingHom S)

Tactic:
let T := S.comap (Pi.evalRingHom R i)

Result:
ι : 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)

Proof state:
case refine_1.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
x₂ : Localization (Submonoid.comap (Pi.evalRingHom R i) S)
r₁ : (i : ι) → R i
s₁ : ↥T
eq : (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁) = (mapPiEvalRingHom S) x₂
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ = x₂

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

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 :
  (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₂

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 :
  ∃ 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₂)

Tactic:
obtain ⟨s, hs⟩ := eq

Result:
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₂)
⊢ ∃ c, ↑c * (↑s₂ * r₁) = ↑c * (↑s₁ * r₂)

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
⊢ update 0 i ↑s ∈ T

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

Result:
no goals