awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_7
S : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_9
inst_3 : CommSemiring A
inst_4 : Algebra R A
M : Submonoid A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
inst_10 : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst_11 : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
this_1 : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this_2 : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
this_3 : IsScalarTower R A (S ⊗[R] B)
this_4 : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)
this : IsScalarTower A B (S ⊗[R] B)
⊢ IsLocalization (R := S ⊗[R] A) (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)
have rw : Algebra.IsPushout R B S (S ⊗[R] B)
Tactic: rw [Algebra.isLocalization_iff_isPushout _ B, Algebra.IsPushout.comm,
    ← Algebra.IsPushout.comp_iff R _ S]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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_1 : Type u_3
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
M'_1 : Type u_4
inst_6 : AddCommMonoid M'_1
inst_7 : Module R_1 M'_1
inst_8 : Module A_1 M'_1
inst_9 : IsScalarTower R_1 A_1 M'_1
f : M_1 →ₗ[R_1] M'_1
T : Type u_5
B_1 : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B_1
inst_12 : Algebra R_1 T
inst_13 : Algebra T B_1
inst_14 : Algebra R_1 B_1
inst_15 : Algebra A_1 B_1
inst_16 : IsScalarTower R_1 T B_1
inst_17 : IsScalarTower R_1 A_1 B_1
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
M : Submonoid A
B : Type u_10
inst_23 : CommSemiring B
inst_24 : Algebra R B
inst_25 : Algebra A B
inst_26 : IsScalarTower R A B
inst_27 : IsLocalization M B
C : Type u_11
inst_28 : CommSemiring C
inst_29 : Algebra S C
inst_30 : Algebra (S ⊗[R] A) C
inst_31 : IsScalarTower S (S ⊗[R] A) C
inst_32 : IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M
this_1 : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B) : S ⊗[R] A →ₐ[R] S ⊗[R] B))
this : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
⊢ Eq (α := A →+* S ⊗[R] B)
    (@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
      (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B))
have a : ∀ (x : A),
  Eq (α := S ⊗[R] B)
    ((@RingHom.comp _ (S ⊗[R] A) _ _ Semiring.toNonAssocSemiring _ (algebraMap (S ⊗[R] A) (S ⊗[R] B))
            (AlgHom.toRingHom Algebra.TensorProduct.includeRight) :
          (a : A) → S ⊗[R] B)
        x :
      S ⊗[R] B)
    ((RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap A B) : (a : A) → S ⊗[R] B) x :
      S ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (hypothesis)
Goal:
R : Type u_7
S : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_9
inst_3 : CommSemiring A
inst_4 : Algebra R A
M : Submonoid A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : IsLocalization M B
C : Type u_11
inst_10 : CommSemiring C
inst_11 : Algebra S C
inst_12 : Algebra (S ⊗[R] A) C
inst_13 : IsScalarTower S (S ⊗[R] A) C
inst_14 : IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight M) C
x : S
a : A
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B) : S ⊗[R] A →ₐ[R] S ⊗[R] B))
⊢ Eq.{u_11 + 1} (α := C)
    ((tensorProductEquivOfMapIncludeRight R S M B C : (a : S ⊗[R] B) → C)
        (x ⊗ₜ[R] (algebraMap A B : (a : A) → B) a : S ⊗[R] B) :
      C)
    ((algebraMap (S ⊗[R] A) C : (a : S ⊗[R] A) → C) (x ⊗ₜ[R] a) : C)
have heq : Eq (α := S ⊗[R] B) (x ⊗ₜ[R] (algebraMap A B : (a : A) → B) a : S ⊗[R] B)
  ((algebraMap (S ⊗[R] A) (S ⊗[R] B) : (a : S ⊗[R] A) → S ⊗[R] B) (x ⊗ₜ[R] a) : S ⊗[R] B)
Tactic: have heq : x ⊗ₜ[R] (algebraMap A B) a = algebraMap _ _ (x ⊗ₜ[R] a) := rfl
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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_1 : Type u_6
inst_10 : CommSemiring T
inst_11 : CommSemiring B_1
inst_12 : Algebra R_1 T
inst_13 : Algebra T B_1
inst_14 : Algebra R_1 B_1
inst_15 : Algebra A_1 B_1
inst_16 : IsScalarTower R_1 T B_1
inst_17 : IsScalarTower R_1 A_1 B_1
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
g : A
B : Type u_10
inst_23 : CommSemiring B
inst_24 : Algebra R B
inst_25 : Algebra A B
inst_26 : IsScalarTower R A B
inst_27 : Away g B
⊢ IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight (Submonoid.powers g))
    (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))
have simp : IsLocalization (R := S ⊗[R] A) (Submonoid.powers (1 ⊗ₜ[R] g)) (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))
Tactic: simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
Goal:
R : Type u_7
S : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A : Type u_9
inst_3 : CommSemiring A
inst_4 : Algebra R A
g : A
B : Type u_10
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
inst_9 : Away g B
x : S
a : A
⊢ IsLocalization (Submonoid.map (F := A →ₐ[R] S ⊗[R] A) Algebra.TensorProduct.includeRight (Submonoid.powers g))
    (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))
have simp : IsLocalization (R := S ⊗[R] A) (Submonoid.powers (1 ⊗ₜ[R] g)) (Localization.Away (M := S ⊗[R] A) (1 ⊗ₜ[R] g))
Tactic: simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ Away (R := S) ((algebraMap R S : (a : R) → S) r : S) (S ⊗[R] A)
have simp : IsLocalization (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (S ⊗[R] A)
Tactic: simp only [IsLocalization.Away, ← Algebra.algebraMapSubmonoid_powers]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.BaseChange (goal)
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
⊢ Away (R := S) ((algebraMap R S : (a : R) → S) r : S) (A ⊗[R] S)
have simp : IsLocalization (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (A ⊗[R] S)
Tactic: simp only [IsLocalization.Away, ← Algebra.algebraMapSubmonoid_powers]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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)
have 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₂
Tactic: refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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₂
⊢ 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)
have 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
Tactic: refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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)
⊢ x₁ = x₂
have 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₂
Tactic: obtain ⟨r₁, s₁, rfl⟩ := exists_mk'_eq T x₁
Cleared hypotheses: x₁, eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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)
⊢ mk' (M := T) (Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) r₁ s₁ = x₂
have 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₂)
Tactic: obtain ⟨r₂, s₂, rfl⟩ := exists_mk'_eq T x₂
Cleared hypotheses: x₂, eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (hypothesis)
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 (α := 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₂)
have 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)) sorry :
      ↥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)) sorry :
      ↥S))
Tactic: simp_rw [map_mk'] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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))
⊢ 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₂)
have 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))
                    sorry) :
                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))
                    sorry) :
                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₂)
Tactic: rw [IsLocalization.eq] at eq ⊢
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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)
⊢ ∃ (c : ↥T), (↑c : (i : ι) → R i) * ((↑s₂ : (i : ι) → R i) * r₁) = (↑c : (i : ι) → R i) * ((↑s₁ : (i : ι) → R i) * r₂)
have 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))
                  sorry) :
              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))
                  sorry) :
              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₂)
Tactic: obtain ⟨s, hs⟩ := eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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)
⊢ ∃ (c : ↥T), (↑c : (i : ι) → R i) * ((↑s₂ : (i : ι) → R i) * r₁) = (↑c : (i : ι) → R i) * ((↑s₁ : (i : ι) → R i) * r₂)
have refine_1 : ∀ (j : ι),
  ((↑(Subtype.mk (p := fun (x : (i : ι) → R i) ↦ x ∈ T) (update (β := R) 0 i (↑s : R i)) sorry) : (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)) sorry) : (i : ι) → R i) *
        ((↑s₁ : (i : ι) → R i) * r₂))
      j
Tactic: refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩