awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
⊢ IsFractionRing S T
have refine_1 : LE.le (α := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R) : Submonoid S)
  (nonZeroDivisors S : Submonoid S)
Tactic: refine @isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
refine_1 :
  LE.le (α := Submonoid S)
    (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R) : Submonoid S)
    (nonZeroDivisors S : Submonoid S)
⊢ IsFractionRing S T
have refine_2 : ∀ (x : ↥(nonZeroDivisors S : Submonoid S)),
  ∃ (m : S),
    Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
      (m * (↑x : S))
Tactic: refine @isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set S)
⊢ ∃ (m : S),
    Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
      (m *
        (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x ⋯) :
          S))
have refine_2 : ∀ (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),
  ∃ (m : S),
    Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
      (m *
        (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x sorry) :
          S))
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 : 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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
⊢ ∃ (m : S),
    Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
      (m *
        (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x ⋯) :
          S))
have h : Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
  (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
    (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x sorry) : S))
Tactic: use algebraMap R S s
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
⊢ Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
      (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (nonZeroDivisors S : Submonoid S) x) x ⋯) :
        S))
have h : Membership.mem (α := S) (γ := Submonoid S)
  (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
  ((algebraMap R S : (a : R) → S) (y, s).1 : S)
Tactic: rw [mul_comm, Subtype.coe_mk, e]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
⊢ Membership.mem (α := S) (γ := Submonoid S)
    (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R))
    ((algebraMap R S : (a : R) → S) (y, s).1 : S)
have h : ∀ (x : R), x * (y, s).1 = 0 → x = 0
Tactic: refine Set.mem_image_of_mem (algebraMap R S) (mem_nonZeroDivisors_iff_right.mpr ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
⊢ z = 0
have h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) 0 : S)
Tactic: apply IsLocalization.injective S hM
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) 0 : S)
have h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) z : S) (0 : S)
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) z : S) (0 : S)
have h : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
Tactic: apply hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
have h : HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x)
    ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
  HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
h :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x)
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
have h₁ : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S)
    (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
  HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
h :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x)
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₁ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S)
      (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
have h₂ : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (y, s).1 : S) =
  HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
h :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x)
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₁ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S)
      (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₂ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (y, s).1 : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
have h₃ : (algebraMap R S : (a : R) → S) (z * (y, s).1) =
  HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
h :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x)
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₁ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S)
      (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₂ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (y, s).1 : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₃ :
  (algebraMap R S : (a : R) → S) (z * (y, s).1) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
have h₄ : (algebraMap R S : (a : R) → S) 0 = HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
h :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x)
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₁ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S)
      (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₂ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (y, s).1 : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₃ :
  (algebraMap R S : (a : R) → S) (z * (y, s).1) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₄ :
  (algebraMap R S : (a : R) → S) 0 = HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
have h₅ : 0 = HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
Tactic: rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
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
this : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R : Submonoid R)) T
x : S
left : x ∈ (↑(nonZeroDivisorsLeft S) : Set S)
hx : x ∈ (↑(nonZeroDivisorsRight S) : Set 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
z : R
hz : z * (y, s).1 = 0
h :
  HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x)
      ((algebraMap R S : (a : R) → S) (↑s : R) : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₁ :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S)
      (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑s : R) : S)) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₂ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (y, s).1 : S) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₃ :
  (algebraMap R S : (a : R) → S) (z * (y, s).1) =
    HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₄ :
  (algebraMap R S : (a : R) → S) 0 = HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
h₅ : 0 = HMul.hMul (α := S) (β := S) (0 : S) ((algebraMap R S : (a : R) → S) (↑s : R) : S)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x = 0
have h₆ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
⊢ IsFractionRing S T
have this : Nontrivial T
Tactic: haveI := IsFractionRing.nontrivial R T
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this : Nontrivial T
⊢ IsFractionRing S T
have this₁ : Nontrivial S
Tactic: haveI := (algebraMap S T).domain_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
⊢ IsFractionRing S T
have apply : M ≤ nonZeroDivisors R
Tactic: apply isFractionRing_of_isLocalization M S T
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x
have rw : x ≠ 0
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ False
have a : Eq.{u_2 + 1} (α := S) 0 1
Tactic: apply @zero_ne_one S
-- Lean 4 proof step from Mathlib.RingTheory.Localization.LocalizationLocalization (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
inst_1 : IsDomain R
S : Type u_2
T : Type u_3
inst_2 : CommRing S
inst_3 : CommRing T
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : IsLocalization M S
inst_9 : IsFractionRing R T
this_1 : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ Eq.{u_2 + 1} (α := S) 0 1
have a : ∃ (m : ↥M), (↑m : R) * 1 = 0
Tactic: rw [← (algebraMap R S).map_one, ← @mk'_one R _ M, @comm _ Eq, mk'_eq_zero_iff]