awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : A
rw :
  Eq.{u_8 + 1} (α := Q)
    ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q)
        ((algebraMap R S : (a : R) → S) ((algebraMap A R : (a : A) → R) x : R) : S) :
      Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₁ :
  Eq.{u_8 + 1} (α := Q)
    ((algebraMap P Q : (a : P) → Q) (((↑h : R →+* P) : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
⊢ Eq.{u_8 + 1} (α := Q) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((algebraMap A S : (a : A) → S) x : S) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
have rw₂ : Eq.{u_8 + 1} (α := Q)
  ((algebraMap P Q : (a : P) → Q) ((h : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
  ((algebraMap A Q : (a : A) → Q) x : Q)
Tactic: rw [IsScalarTower.algebraMap_apply A R S, map_eq,
    RingHom.coe_coe, AlgEquiv.commutes, IsScalarTower.algebraMap_apply A P Q]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : A
rw :
  Eq.{u_8 + 1} (α := Q)
    ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q)
        ((algebraMap R S : (a : R) → S) ((algebraMap A R : (a : A) → R) x : R) : S) :
      Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₁ :
  Eq.{u_8 + 1} (α := Q)
    ((algebraMap P Q : (a : P) → Q) (((↑h : R →+* P) : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₂ :
  Eq.{u_8 + 1} (α := Q)
    ((algebraMap P Q : (a : P) → Q) ((h : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
⊢ Eq.{u_8 + 1} (α := Q) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((algebraMap A S : (a : A) → S) x : S) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
have rw₃ : Eq.{u_8 + 1} (α := Q) ((algebraMap P Q : (a : P) → Q) ((algebraMap A P : (a : A) → P) x : P) : Q)
  ((algebraMap A Q : (a : A) → Q) x : Q)
Tactic: rw [IsScalarTower.algebraMap_apply A R S, map_eq,
    RingHom.coe_coe, AlgEquiv.commutes, IsScalarTower.algebraMap_apply A P Q]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : A
rw :
  Eq.{u_8 + 1} (α := Q)
    ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q)
        ((algebraMap R S : (a : R) → S) ((algebraMap A R : (a : A) → R) x : R) : S) :
      Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₁ :
  Eq.{u_8 + 1} (α := Q)
    ((algebraMap P Q : (a : P) → Q) (((↑h : R →+* P) : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₂ :
  Eq.{u_8 + 1} (α := Q)
    ((algebraMap P Q : (a : P) → Q) ((h : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₃ :
  Eq.{u_8 + 1} (α := Q) ((algebraMap P Q : (a : P) → Q) ((algebraMap A P : (a : A) → P) x : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
⊢ Eq.{u_8 + 1} (α := Q) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((algebraMap A S : (a : A) → S) x : S) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
have rw₄ : Eq.{u_8 + 1} (α := Q) ((algebraMap P Q : (a : P) → Q) ((algebraMap A P : (a : A) → P) x : P) : Q)
  ((algebraMap P Q : (a : P) → Q) ((algebraMap A P : (a : A) → P) x : P) : Q)
Tactic: rw [IsScalarTower.algebraMap_apply A R S, map_eq,
    RingHom.coe_coe, AlgEquiv.commutes, IsScalarTower.algebraMap_apply A P Q]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
⊢ Submonoid.map h.symm T = M
have rw : Submonoid.map h.symm (Submonoid.map h M) = M
Tactic: rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv,
        ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
        Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
rw : Submonoid.map h.symm (Submonoid.map h M) = M
⊢ Submonoid.map h.symm T = M
have rw₁ : Submonoid.map (F := P ≃* R) (↑h.symm : P ≃* R) (Submonoid.map h M) = M
Tactic: rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv,
        ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
        Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
rw : Submonoid.map h.symm (Submonoid.map h M) = M
rw₁ : Submonoid.map (F := P ≃* R) (↑h.symm : P ≃* R) (Submonoid.map h M) = M
⊢ Submonoid.map h.symm T = M
have rw₂ : Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑h : R ≃* P)) (Submonoid.map h M) = M
Tactic: rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv,
        ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
        Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
rw : Submonoid.map h.symm (Submonoid.map h M) = M
rw₁ : Submonoid.map (F := P ≃* R) (↑h.symm : P ≃* R) (Submonoid.map h M) = M
rw₂ : Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑h : R ≃* P)) (Submonoid.map h M) = M
⊢ Submonoid.map h.symm T = M
have rw₃ : Submonoid.comap (F := R ≃* P) (↑h : R ≃* P) (Submonoid.map h M) = M
Tactic: rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv,
        ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
        Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
rw : Submonoid.map h.symm (Submonoid.map h M) = M
rw₁ : Submonoid.map (F := P ≃* R) (↑h.symm : P ≃* R) (Submonoid.map h M) = M
rw₂ : Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑h : R ≃* P)) (Submonoid.map h M) = M
rw₃ : Submonoid.comap (F := R ≃* P) (↑h : R ≃* P) (Submonoid.map h M) = M
⊢ Submonoid.map h.symm T = M
have rw₄ : Submonoid.comap (F := R ≃* P) (↑h : R ≃* P) (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) = M
Tactic: rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv,
        ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
        Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
rw : Submonoid.map h.symm (Submonoid.map h M) = M
rw₁ : Submonoid.map (F := P ≃* R) (↑h.symm : P ≃* R) (Submonoid.map h M) = M
rw₂ : Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑h : R ≃* P)) (Submonoid.map h M) = M
rw₃ : Submonoid.comap (F := R ≃* P) (↑h : R ≃* P) (Submonoid.map h M) = M
rw₄ : Submonoid.comap (F := R ≃* P) (↑h : R ≃* P) (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) = M
⊢ Submonoid.map h.symm T = M
have rw₅ : M = M
Tactic: rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv,
        ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
        Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
inst : CommSemiring R
S : Submonoid R
R' : Type u_5
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
inst_3 : IsLocalization S R'
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
inst_6 : Module R M'
inst_7 : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
⊢ s • x ∈ N' ↔ x ∈ N'
have refine : ∀ (h : s • x ∈ N'), x ∈ N'
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Submodule.smul_of_tower_mem N' s h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
inst : CommSemiring R
S : Submonoid R
R' : Type u_5
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
inst_3 : IsLocalization S R'
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
inst_6 : Module R M'
inst_7 : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
h : s • x ∈ N'
⊢ x ∈ N'
have rwa : HSMul.hSMul.{u_5, u_6, u_6} (α := R') ((algebraMap R R' : (a : R) → R') (↑s : R) : R') x ∈ N'
Tactic: rwa [← Submodule.smul_mem_iff_of_isUnit (r := algebraMap R R' s) N' (map_units R' s),
    algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
inst : CommSemiring R
S : Submonoid R
R' : Type u_5
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
inst_3 : IsLocalization S R'
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
inst_6 : Module R M'
inst_7 : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
h : s • x ∈ N'
rwa : HSMul.hSMul.{u_5, u_6, u_6} (α := R') ((algebraMap R R' : (a : R) → R') (↑s : R) : R') x ∈ N'
⊢ x ∈ N'
have rwa₁ : (↑s : R) • x ∈ N'
Tactic: rwa [← Submodule.smul_mem_iff_of_isUnit (r := algebraMap R R' s) N' (map_units R' s),
    algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
hM : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) (IsUnit.submonoid S)
h : Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
y : S
⊢ ∃ (x : R × ↥M),
    HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1
have obtain : ∀ (x : R),
  ∃ (x_1 : R × ↥M),
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
        ((algebraMap R S : (a : R) → S) (↑x_1.2 : R) : S) =
      (algebraMap R S : (a : R) → S) x_1.1
Tactic: obtain ⟨x, rfl⟩ := h.surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Submonoid R
hM : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) (IsUnit.submonoid S)
h : Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : R
⊢ ∃ (x_1 : R × ↥M),
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
        ((algebraMap R S : (a : R) → S) (↑x_1.2 : R) : S) =
      (algebraMap R S : (a : R) → S) x_1.1
have h₁ : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
    ((algebraMap R S : (a : R) → S) (↑(x, 1).2 : R) : S) =
  (algebraMap R S : (a : R) → S) (x, 1).1
Tactic: use ⟨x, 1⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
⊢ R ≃ₐ[R] S
have refine_1 : Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(Algebra.ofId R S) : (a : R) → S)
Tactic: refine AlgEquiv.ofBijective (Algebra.ofId R S) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
refine_1 : Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(Algebra.ofId R S) : (a : R) → S)
⊢ R ≃ₐ[R] S
have refine_2 : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(Algebra.ofId R S) : (a : R) → S)
Tactic: refine AlgEquiv.ofBijective (Algebra.ofId R S) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((Algebra.ofId R S : (a : R) → S) x : S) ((Algebra.ofId R S : (a : R) → S) y : S)
⊢ x = y
have refine_1 : ∀ (c : ↥M) (eq : (↑c : R) * x = (↑c : R) * y), x = y
Tactic: obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((Algebra.ofId R S : (a : R) → S) x : S) ((Algebra.ofId R S : (a : R) → S) y : S)
c : ↥M
eq : (↑c : R) * x = (↑c : R) * y
⊢ x = y
have refine_1 : ∀ (u : Rˣ) (hu : (↑u : R) = (↑c : R)), x = y
Tactic: obtain ⟨u, hu⟩ := H c.prop
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((Algebra.ofId R S : (a : R) → S) x : S) ((Algebra.ofId R S : (a : R) → S) y : S)
c : ↥M
eq : (↑c : R) * x = (↑c : R) * y
u : Rˣ
hu : (↑u : R) = (↑c : R)
⊢ x = y
have refine_1 : ∀ (eq : (↑u : R) * x = (↑u : R) * y) (hu : (↑u : R) = (↑c : R)), x = y
Tactic: rwa [← hu, Units.mul_right_inj] at eq
Cleared hypotheses: eq, hu
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((Algebra.ofId R S : (a : R) → S) x : S) ((Algebra.ofId R S : (a : R) → S) y : S)
c : ↥M
eq : (↑c : R) * x = (↑c : R) * y
u : Rˣ
hu : (↑u : R) = (↑c : R)
refine_1 : ∀ (eq : (↑u : R) * x = (↑u : R) * y) (hu : (↑u : R) = (↑c : R)), x = y
⊢ x = y
have refine_1₁ : ∀ (eq : x = y) (hu : (↑u : R) = (↑c : R)), x = y
Tactic: rwa [← hu, Units.mul_right_inj] at eq
Cleared hypotheses: eq, hu
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
⊢ ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y
have refine_2 : ∀ (x : R) (s : ↥M)
  (eq :
    HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (x, s).1),
  ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y
Tactic: obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
⊢ ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y
have refine_2 : ∀ (u : Rˣ) (hu : (↑u : R) = (↑s : R)), ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y
Tactic: obtain ⟨u, hu⟩ := H s.prop
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
u : Rˣ
hu : (↑u : R) = (↑s : R)
⊢ ∃ (a : R), (Algebra.ofId R S : (a : R) → S) a = y
have h : (Algebra.ofId R S : (a : R) → S) (x * u.inv) = y
Tactic: use x * u.inv
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
u : Rˣ
hu : (↑u : R) = (↑s : R)
⊢ (Algebra.ofId R S : (a : R) → S) (x * u.inv) = y
have h : (algebraMap R S : (a : R) → S) (x * (↑u⁻¹ : R)) = y
Tactic: dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]