awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
y : R
hy : y ∈ (↑N : Set R)
⊢ IsUnit.{u_3} (M := T)
    ((algebraMap S T : (a : S) → T)
        ((↑(Subtype.mk (p := fun (x : S) ↦
                Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
                ((algebraMap R S : (a : R) → S) y) ⋯) :
            S) :
          S) :
      T)
have h₁ : Eq.{u_3 + 1} (α := T)
  ((algebraMap S T : (a : S) → T)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
              ((algebraMap R S : (a : R) → S) y) sorry) :
          S) :
        S) :
    T)
  ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) y hy) : R) : T)
Tactic: convert! IsLocalization.map_units T ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
y : T
⊢ ∃ (x : S × ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)),
    HMul.hMul (β := T) y ((algebraMap S T : (a : S) → T) (↑x.2 : S) : T) = (algebraMap S T : (a : S) → T) x.1
have obtain : ∀ (x : R) (s : ↥N)
  (e :
    HMul.hMul (β := T) y ((algebraMap R T : (a : R) → T) (↑(x, s).2 : R) : T) =
      (algebraMap R T : (a : R) → T) (x, s).1),
  ∃ (x : S × ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)),
    HMul.hMul (β := T) y ((algebraMap S T : (a : S) → T) (↑x.2 : S) : T) = (algebraMap S T : (a : S) → T) x.1
Tactic: obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj N y
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
y : T
x : R
s : ↥N
e : HMul.hMul (β := T) y ((algebraMap R T : (a : R) → T) (↑(x, s).2 : R) : T) = (algebraMap R T : (a : R) → T) (x, s).1
⊢ ∃ (x : S × ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)),
    HMul.hMul (β := T) y ((algebraMap S T : (a : S) → T) (↑x.2 : S) : T) = (algebraMap S T : (a : S) → T) x.1
have refine : HMul.hMul (β := T) y
    ((algebraMap S T : (a : S) → T)
        ((↑((algebraMap R S : (a : R) → S) x,
                  Subtype.mk (p := fun (x : S) ↦
                    Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
                    ((algebraMap R S : (a : R) → S) (↑s : R)) sorry).2 :
            S) :
          S) :
      T) =
  (algebraMap S T : (a : S) → T)
    (((algebraMap R S : (a : R) → S) x,
          Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) N) x)
            ((algebraMap R S : (a : R) → S) (↑s : R)) sorry).1 :
      S)
Tactic: refine ⟨⟨algebraMap R S x, _, _, s.prop, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂
have obtain : ∀ (y₁ : R) (s₁ : ↥M)
  (e₁ :
    HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑(y₁, s₁).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (y₁, s₁).1),
  Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂
Tactic: obtain ⟨⟨y₁, s₁⟩, e₁⟩ := IsLocalization.surj M x₁
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ :
  HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑(y₁, s₁).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (y₁, s₁).1
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂
have obtain : ∀ (y₂ : R) (s₂ : ↥M)
  (e₂ :
    HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑(y₂, s₂).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (y₂, s₂).1),
  Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂
Tactic: obtain ⟨⟨y₂, s₂⟩, e₂⟩ := IsLocalization.surj M x₂
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ :
  HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑(y₁, s₁).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (y₁, s₁).1
y₂ : R
s₂ : ↥M
e₂ :
  HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑(y₂, s₂).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (y₂, s₂).1
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (c : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) N)), (↑c : S) * x₁ = (↑c : S) * x₂
have refine : Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
  ∃ (a : (↑(↑N : Set R) : Type u_1)),
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₁ =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₂
Tactic: refine (Set.exists_image_iff (algebraMap R S) N fun c => c * x₁ = c * x₂).mpr.comp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) = (algebraMap R S : (a : R) → S) y₁
y₂ : R
s₂ : ↥M
e₂ : HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) = (algebraMap R S : (a : R) → S) y₂
this :
  Eq.{u_3 + 1} (α := T) ((algebraMap R T : (a : R) → T) (y₁ * (↑s₂ : R)) : T)
      ((algebraMap R T : (a : R) → T) (y₂ * (↑s₁ : R)) : T) →
    ∃ (a : ↥N),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₁ * (↑s₂ : R))) : S)
        ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₂ * (↑s₁ : R))) : S)
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (a : (↑(↑N : Set R) : Type u_1)),
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₁ =
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₂
have h₁ : HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
      ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) sorry) : R) : T) =
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
      ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) sorry) : R) : T) ↔
  Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T)
Tactic: have h₁ := @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂)
        (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) = (algebraMap R S : (a : R) → S) y₁
y₂ : R
s₂ : ↥M
e₂ : HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) = (algebraMap R S : (a : R) → S) y₂
this :
  Eq.{u_3 + 1} (α := T) ((algebraMap R T : (a : R) → T) (y₁ * (↑s₂ : R)) : T)
      ((algebraMap R T : (a : R) → T) (y₂ * (↑s₁ : R)) : T) →
    ∃ (a : ↥N),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₁ * (↑s₂ : R))) : S)
        ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₂ * (↑s₁ : R))) : S)
h₁ :
  HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) ↔
    Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T)
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (a : (↑(↑N : Set R) : Type u_1)),
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₁ =
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₂
have h₂ : HMul.hMul (β := T)
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
        ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T))
      ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₂ : R) sorry) : R) : T) =
    HMul.hMul (β := T)
      (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
        ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T))
      ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₂ : R) sorry) : R) : T) ↔
  HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T) =
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T) ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T)
Tactic: have h₂ := @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
        ((algebraMap S T x₂) * (algebraMap R T s₁))
        (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) = (algebraMap R S : (a : R) → S) y₁
y₂ : R
s₂ : ↥M
e₂ : HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) = (algebraMap R S : (a : R) → S) y₂
this :
  Eq.{u_3 + 1} (α := T) ((algebraMap R T : (a : R) → T) (y₁ * (↑s₂ : R)) : T)
      ((algebraMap R T : (a : R) → T) (y₂ * (↑s₁ : R)) : T) →
    ∃ (a : ↥N),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₁ * (↑s₂ : R))) : S)
        ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₂ * (↑s₁ : R))) : S)
h₁ :
  HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₁ : R) ⋯) : R) : T) ↔
    Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T)
h₂ :
  HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
          ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T))
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₂ : R) ⋯) : R) : T) =
      HMul.hMul (β := T)
        (HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
          ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T))
        ((algebraMap R T : (a : R) → T) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ N) (↑s₂ : R) ⋯) : R) : T) ↔
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T) =
      HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T) ((algebraMap R T : (a : R) → T) (↑s₁ : R) : T)
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (a : (↑(↑N : Set R) : Type u_1)),
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₁ =
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₂
have h₃ : HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₁ : T)
      ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T) =
    HMul.hMul (α := T) (β := T) ((algebraMap S T : (a : S) → T) x₂ : T)
      ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) : T) ↔
  Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T)
Tactic: simp only [IsScalarTower.algebraMap_apply R S T] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) = (algebraMap R S : (a : R) → S) y₁
y₂ : R
s₂ : ↥M
e₂ : HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) = (algebraMap R S : (a : R) → S) y₂
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) x₁ : T) ((algebraMap S T : (a : S) → T) x₂ : T) →
    ∃ (a : (↑(↑N : Set R) : Type u_1)),
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₁ =
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑a : R) : S) x₂
have suffices : Eq.{u_3 + 1} (α := T) ((algebraMap R T : (a : R) → T) (y₁ * (↑s₂ : R)) : T)
    ((algebraMap R T : (a : R) → T) (y₂ * (↑s₁ : R)) : T) →
  ∃ (a : ↥N),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₁ * (↑s₂ : R))) : S)
      ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₂ * (↑s₁ : R))) : S)
Tactic: suffices algebraMap R T (y₁ * s₂) = algebraMap R T (y₂ * s₁) →
        ∃ a : N, algebraMap R S (a * (y₁ * s₂)) = algebraMap R S (a * (y₂ * s₁)) by
      have h₁ := @IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂)
        (IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)
      have h₂ := @IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
        ((algebraMap S T x₂) * (algebraMap R T s₁))
        (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)
      simp only [IsScalarTower.algebraMap_apply R S T] at h₁ h₂
      simp only [IsScalarTower.algebraMap_apply R S T, map_mul, ← e₁, ← e₂, ← mul_assoc,
        mul_right_comm _ (algebraMap R S s₂),
        (IsLocalization.map_units S s₁).mul_left_inj,
        (IsLocalization.map_units S s₂).mul_left_inj] at this
      rw [h₂, h₁] at this
      simpa only [mul_comm] using this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) = (algebraMap R S : (a : R) → S) y₁
y₂ : R
s₂ : ↥M
e₂ : HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) = (algebraMap R S : (a : R) → S) y₂
⊢ Eq.{u_3 + 1} (α := T) ((algebraMap R T : (a : R) → T) (y₁ * (↑s₂ : R)) : T)
      ((algebraMap R T : (a : R) → T) (y₂ * (↑s₁ : R)) : T) →
    ∃ (a : ↥N),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₁ * (↑s₂ : R))) : S)
        ((algebraMap R S : (a : R) → S) ((↑a : R) * (y₂ * (↑s₁ : R))) : S)
have simp_rw : (∃ (c : ↥N), (↑c : R) * (y₁ * (↑s₂ : R)) = (↑c : R) * (y₂ * (↑s₁ : R))) →
  ∃ (a : ↥N) (c : ↥M), (↑c : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑c : R) * ((↑a : R) * (y₂ * (↑s₁ : R)))
Tactic: simp_rw [IsLocalization.eq_iff_exists N T, IsLocalization.eq_iff_exists M S]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) = (algebraMap R S : (a : R) → S) y₁
y₂ : R
s₂ : ↥M
e₂ : HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) = (algebraMap R S : (a : R) → S) y₂
a : ↥N
e : (↑a : R) * (y₁ * (↑s₂ : R)) = (↑a : R) * (y₂ * (↑s₁ : R))
⊢ (↑1 : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑1 : R) * ((↑a : R) * (y₂ * (↑s₁ : R)))
have h₁ : (↑1 : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑a : R) * (y₁ * (↑s₂ : R))
Tactic: convert! e using 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
M N : Submonoid R
h : M ≤ N
inst_5 : IsLocalization M S
inst_6 : IsLocalization N T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : HMul.hMul (β := S) x₁ ((algebraMap R S : (a : R) → S) (↑s₁ : R) : S) = (algebraMap R S : (a : R) → S) y₁
y₂ : R
s₂ : ↥M
e₂ : HMul.hMul (β := S) x₂ ((algebraMap R S : (a : R) → S) (↑s₂ : R) : S) = (algebraMap R S : (a : R) → S) y₂
a : ↥N
e : (↑a : R) * (y₁ * (↑s₂ : R)) = (↑a : R) * (y₂ * (↑s₁ : R))
h₁ : (↑1 : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑a : R) * (y₁ * (↑s₂ : R))
⊢ (↑1 : R) * ((↑a : R) * (y₁ * (↑s₂ : R))) = (↑1 : R) * ((↑a : R) * (y₂ * (↑s₁ : R)))
have h₂ : (↑1 : R) * ((↑a : R) * (y₂ * (↑s₁ : R))) = (↑a : R) * (y₂ * (↑s₁ : R))
Tactic: convert! e using 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
y : ↥N
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)
have obtain : ∀ (m : R) (hm : m * (↑y : R) ∈ M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)
Tactic: obtain ⟨m, hm⟩ := h' y
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
y : ↥N
m : R
hm : m * (↑y : R) ∈ M
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)
have this : IsUnit.{u_2} (M := S)
  ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) (m * (↑y : R)) hm) : R) : S)
Tactic: have := IsLocalization.map_units S ⟨_, hm⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
y : ↥N
m : R
hm : m * (↑y : R) ∈ M
this :
  IsUnit.{u_2} (M := S)
    ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) (m * (↑y : R)) hm) : R) : S)
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)
have this₁ : IsUnit
  (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) m : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S))
Tactic: rw [map_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
z : S
⊢ ∃ (x : R × ↥N),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1
have obtain : ∀ (y : R) (s : ↥M)
  (e :
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(y, s).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (y, s).1),
  ∃ (x : R × ↥N),
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1
Tactic: obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M z
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M N : Submonoid R
inst_3 : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ (m : R), m * (↑x : R) ∈ M
x x_1 : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) x_1 : S) →
    ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * x_1
have rw : (∃ (c : ↥M), (↑c : R) * x = (↑c : R) * x_1) → ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * x_1
Tactic: rw [IsLocalization.eq_iff_exists M]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalization M S
inst_8 : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
⊢ IsFractionRing S T
have this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
Tactic: have := isLocalization_of_submonoid_le S T M (nonZeroDivisors R) hM