awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Submonoid R_1
A_1 : Type u_2
inst_1 : CommSemiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : IsLocalization S_1 A_1
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R_1 M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R_1 M'
inst_8 : Module A_1 M'
inst_9 : IsScalarTower R_1 A_1 M'
f : M →ₗ[R_1] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R_1 T
inst_13 : Algebra T B
inst_14 : Algebra R_1 B
inst_15 : Algebra A_1 B
inst_16 : IsScalarTower R_1 T B
inst_17 : IsScalarTower R_1 A_1 B
R : Type u_7
S : Type u_8
inst_18 : CommSemiring R
inst_19 : CommSemiring S
inst_20 : Algebra R S
r : R
A : Type u_9
inst_21 : CommSemiring A
inst_22 : Algebra R A
inst_23 : Away r A
⊢ IsLocalization (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (S ⊗[R] A)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Submonoid R_1
A_1 : Type u_2
inst_1 : CommSemiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : IsLocalization S_1 A_1
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R_1 M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R_1 M'
inst_8 : Module A_1 M'
inst_9 : IsScalarTower R_1 A_1 M'
f : M →ₗ[R_1] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R_1 T
inst_13 : Algebra T B
inst_14 : Algebra R_1 B
inst_15 : Algebra A_1 B
inst_16 : IsScalarTower R_1 T B
inst_17 : IsScalarTower R_1 A_1 B
R : Type u_7
S : Type u_8
inst_18 : CommSemiring R
inst_19 : CommSemiring S
inst_20 : Algebra R S
r : R
A : Type u_9
inst_21 : CommSemiring A
inst_22 : Algebra R A
inst_23 : Away r A
simp : IsLocalization (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (A ⊗[R] S)
⊢ Away (R := S) ((algebraMap R S : (a : R) → S) r : S) (A ⊗[R] S)

Tactic:
simp only [IsLocalization.Away, ← Algebra.algebraMapSubmonoid_powers]

Premises used: IsLocalization.Away, Algebra.algebraMapSubmonoid_powers
-- Module: Mathlib.RingTheory.Localization.BaseChange
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
S_1 : Submonoid R_1
A_1 : Type u_2
inst_1 : CommSemiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : IsLocalization S_1 A_1
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R_1 M
M' : Type u_4
inst_6 : AddCommMonoid M'
inst_7 : Module R_1 M'
inst_8 : Module A_1 M'
inst_9 : IsScalarTower R_1 A_1 M'
f : M →ₗ[R_1] M'
T : Type u_5
B : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B
inst_12 : Algebra R_1 T
inst_13 : Algebra T B
inst_14 : Algebra R_1 B
inst_15 : Algebra A_1 B
inst_16 : IsScalarTower R_1 T B
inst_17 : IsScalarTower R_1 A_1 B
R : Type u_7
S : Type u_8
inst_18 : CommSemiring R
inst_19 : CommSemiring S
inst_20 : Algebra R S
r : R
A : Type u_9
inst_21 : CommSemiring A
inst_22 : Algebra R A
inst_23 : Away r A
⊢ IsLocalization (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (A ⊗[R] S)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
⊢ Bijective (α := Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) (β :=
    Localization (M := R i) S)
    (⇑(mapPiEvalRingHom (R := R) S) : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)

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

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
refine_1 :
  ∀ (x₁ x₂ : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S))
    (eq :
      Eq.{u_2 + 1} (α := Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            x₁ :
          Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            x₂ :
          Localization (M := R i) S)),
    x₁ = x₂
refine_2 :
  ∀ (x : Localization (M := R i) S),
    ∃ (a : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)),
      (mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) a = x
⊢ Bijective (α := Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) (β :=
    Localization (M := R i) S)
    (⇑(mapPiEvalRingHom (R := R) S) : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)

Tactic:
refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
x₁ x₂ : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)
eq :
  Eq.{u_2 + 1} (α := Localization (M := R i) S)
    ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) x₁ :
      Localization (M := R i) S)
    ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) x₂ :
      Localization (M := R i) S)
refine_1 :
  ∀ (r₁ : (i : ι) → R i) (s₁ : ↥T)
    (eq :
      Eq.{u_2 + 1} (α := Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁
              s₁) :
          Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            x₂ :
          Localization (M := R i) S)),
    mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁ s₁ = x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨r₁, s₁, rfl⟩ := exists_mk'_eq T x₁

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
x₂ : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)
r₁ : (i : ι) → R i
s₁ : ↥T
eq :
  Eq.{u_2 + 1} (α := Localization (M := R i) S)
    ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
        (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁ s₁) :
      Localization (M := R i) S)
    ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) x₂ :
      Localization (M := R i) S)
refine_1 :
  ∀ (r₂ : (i : ι) → R i) (s₂ : ↥T)
    (eq :
      Eq.{u_2 + 1} (α := Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
          (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁ s₁))
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
          (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₂ s₂))),
    Eq (α := Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S))
      (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁ s₁)
      (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₂ s₂)
⊢ mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁ s₁ = x₂

Tactic:
obtain ⟨r₂, s₂, rfl⟩ := exists_mk'_eq T x₂

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  Eq.{u_2 + 1} (α := Localization (M := R i) S)
    ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
      (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁ s₁))
    ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
      (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₂ s₂))
⊢ Eq.{u_2 + 1} (α := Localization (M := R i) S)
    (mk' (R := R i) (M := S) (Localization (M := R i) S)
      (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i)
      (Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
          (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i)) ⋯ :
        ↥S))
    (mk' (R := R i) (M := S) (Localization (M := R i) S)
      (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)
      (Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
          (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i)) ⋯ :
        ↥S))

Tactic:
simp_rw [map_mk'] at eq

Premises used: IsLocalization.map_mk'
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  Eq.{u_2 + 1} (α := Localization (M := R i) S)
    (mk' (R := R i) (M := S) (Localization (M := R i) S)
      (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i)
      (Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
          (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i)) ⋯ :
        ↥S))
    (mk' (R := R i) (M := S) (Localization (M := R i) S)
      (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)
      (Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
          (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i)) ⋯ :
        ↥S))
refine_1 :
  ∀
    (eq :
      ∃ (c : ↥S),
        (↑c : R i) *
            HMul.hMul (α := R i) (β := R i)
              ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                      (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i)
                        (↑s₂ : (i : ι) → R i))
                      ⋯) :
                  R i) :
                R i)
              (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i) =
          (↑c : R i) *
            HMul.hMul (α := R i) (β := R i)
              ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                      (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i)
                        (↑s₁ : (i : ι) → R i))
                      ⋯) :
                  R i) :
                R i)
              (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)),
    ∃ (c : ↥T),
      (↑c : (i : ι) → R i) * ((↑s₂ : (i : ι) → R i) * r₁) = (↑c : (i : ι) → R i) * ((↑s₁ : (i : ι) → R i) * r₂)
⊢ Eq (α := Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S))
    (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁ s₁)
    (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₂ s₂)

Tactic:
rw [IsLocalization.eq] at eq ⊢

Premises used: IsLocalization.eq
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  ∃ (c : ↥S),
    (↑c : R i) *
        HMul.hMul (α := R i) (β := R i)
          ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                  (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i))
                  ⋯) :
              R i) :
            R i)
          (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i) =
      (↑c : R i) *
        HMul.hMul (α := R i) (β := R i)
          ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                  (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i))
                  ⋯) :
              R i) :
            R i)
          (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)
refine_1 :
  ∀ (s : ↥S)
    (hs :
      (↑s : R i) *
          HMul.hMul (α := R i) (β := R i)
            ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                    (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i))
                    ⋯) :
                R i) :
              R i)
            (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i) =
        (↑s : R i) *
          HMul.hMul (α := R i) (β := R i)
            ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                    (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i))
                    ⋯) :
                R i) :
              R i)
            (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)),
    ∃ (c : ↥T),
      (↑c : (i : ι) → R i) * ((↑s₂ : (i : ι) → R i) * r₁) = (↑c : (i : ι) → R i) * ((↑s₁ : (i : ι) → R i) * r₂)
⊢ ∃ (c : ↥T), (↑c : (i : ι) → R i) * ((↑s₂ : (i : ι) → R i) * r₁) = (↑c : (i : ι) → R i) * ((↑s₁ : (i : ι) → R i) * r₂)

Tactic:
obtain ⟨s, hs⟩ := eq
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i) =
    (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)
⊢ update (β := R) 0 i (↑s : R i) ∈ T

Tactic:
apply update_self i s.1 0 ▸ s.2
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i) =
    (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)
refine_1 :
  ∀ (j : ι),
    ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯) : (i : ι) → R i) *
          ((↑s₂ : (i : ι) → R i) * r₁))
        j =
      ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯) : (i : ι) → R i) *
          ((↑s₁ : (i : ι) → R i) * r₂))
        j
⊢ ∃ (c : ↥T), (↑c : (i : ι) → R i) * ((↑s₂ : (i : ι) → R i) * r₁) = (↑c : (i : ι) → R i) * ((↑s₁ : (i : ι) → R i) * r₂)

Tactic:
refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : 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 (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) S
s₁ s₂ : ↥T
s : ↥S
hs :
  (↑s : R j) *
      HMul.hMul (α := R j) (β := R j)
        ((↑(Subtype.mk (p := fun (x : R j) ↦ x ∈ S)
                (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) (↑s₂ : (i : ι) → R i))
                ⋯) :
            R j) :
          R j)
        (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) r₁ : R j) =
    (↑s : R j) *
      HMul.hMul (α := R j) (β := R j)
        ((↑(Subtype.mk (p := fun (x : R j) ↦ x ∈ S)
                (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) (↑s₁ : (i : ι) → R i))
                ⋯) :
            R j) :
          R j)
        (((Pi.evalRingHom R j : ((i : ι) → R i) →+* R j) : (a : (i : ι) → R i) → R j) r₂ : R j)
⊢ ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 j (↑s : R j)) ⋯) : (i : ι) → R i) *
        ((↑s₂ : (i : ι) → R i) * r₁))
      j =
    ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 j (↑s : R j)) ⋯) : (i : ι) → R i) *
        ((↑s₁ : (i : ι) → R i) * r₂))
      j

Tactic:
simpa using hs
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₂ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₁ : R i) =
    (↑s : R i) *
      HMul.hMul (α := R i) (β := R i)
        ((↑(Subtype.mk (p := fun (x : R i) ↦ x ∈ S)
                (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) (↑s₁ : (i : ι) → R i))
                ⋯) :
            R i) :
          R i)
        (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) r₂ : R i)
j : ι
ne : j ≠ i
⊢ ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯) : (i : ι) → R i) *
        ((↑s₂ : (i : ι) → R i) * r₁))
      j =
    ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯) : (i : ι) → R i) *
        ((↑s₁ : (i : ι) → R i) * r₂))
      j

Tactic:
simp [update_of_ne ne]

Premises used: Function.update_of_ne
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
x : Localization (M := R i) S
refine_2 :
  ∀ (r : R i) (s : ↥S),
    ∃ (a : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)),
      Eq (α := Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            a :
          Localization (M := R i) S)
        (mk' (Localization (M := R i) S) r s : Localization (M := R i) S)
⊢ ∃ (a : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)),
    (mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) a = x

Tactic:
obtain ⟨r, s, rfl⟩ := exists_mk'_eq S x

Premises used: Localization.r, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r : R i
s : ↥S
⊢ update (β := R) 0 i (↑s : R i) ∈ T

Tactic:
apply update_self i s.1 0 ▸ s.2
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r : R i
s : ↥S
⊢ Eq (α := Localization (M := R i) S)
    ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
      (mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S))
        (update (β := R) 0 i r) (Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) ⋯)))
    (mk' (Localization (M := R i) S) r s)

Tactic:
simp [map_mk']

Premises used: IsLocalization.map_mk'
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
r : R i
s : ↥S
⊢ ∃ (a : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)),
    Eq (α := Localization (M := R i) S)
      ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) a :
        Localization (M := R i) S)
      (mk' (Localization (M := R i) S) r s : Localization (M := R i) 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']⟩