awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ : (a : R) → Rₘ) (r * n) = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
have rw : HMul.hMul (α := Rₘ) (β := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) : Rₘ) =
  (algebraMap R Rₘ : (a : R) → Rₘ) r
Tactic: rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
rw :
  HMul.hMul (α := Rₘ) (β := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) : Rₘ) =
    (algebraMap R Rₘ : (a : R) → Rₘ) r
⊢ (algebraMap R Rₘ : (a : R) → Rₘ) (r * n) = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
have rw₁ : Eq.{u_5 + 1} (α := Rₘ)
  ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R)) : Rₘ)
  ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
Tactic: rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
rw :
  HMul.hMul (α := Rₘ) (β := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) : Rₘ) =
    (algebraMap R Rₘ : (a : R) → Rₘ) r
rw₁ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R)) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
⊢ (algebraMap R Rₘ : (a : R) → Rₘ) (r * n) = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
have rw₂ : Eq.{u_5 + 1} (α := Rₘ)
  ((algebraMap R Rₘ : (a : R) → Rₘ) (r * (n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R))) : Rₘ)
  ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
Tactic: rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
rw :
  HMul.hMul (α := Rₘ) (β := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) : Rₘ) =
    (algebraMap R Rₘ : (a : R) → Rₘ) r
rw₁ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R)) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₂ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * (n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R))) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
⊢ (algebraMap R Rₘ : (a : R) → Rₘ) (r * n) = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
have rw₃ : Eq.{u_5 + 1} (α := Rₘ)
  ((algebraMap R Rₘ : (a : R) → Rₘ) (r * ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) * n)) : Rₘ)
  ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
Tactic: rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
rw :
  HMul.hMul (α := Rₘ) (β := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) : Rₘ) =
    (algebraMap R Rₘ : (a : R) → Rₘ) r
rw₁ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R)) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₂ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * (n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R))) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₃ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) * n)) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
⊢ (algebraMap R Rₘ : (a : R) → Rₘ) (r * n) = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
have rw₄ : Eq.{u_5 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * 1) : Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
Tactic: rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
rw :
  HMul.hMul (α := Rₘ) (β := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) : Rₘ) =
    (algebraMap R Rₘ : (a : R) → Rₘ) r
rw₁ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R)) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₂ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * (n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R))) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₃ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) * n)) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₄ : Eq.{u_5 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * 1) : Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
⊢ (algebraMap R Rₘ : (a : R) → Rₘ) (r * n) = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
have rw₅ : Eq.{u_5 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
Tactic: rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Sₘ : Type u_5
inst_3 : CommSemiring Sₘ
inst_4 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit.{u_5} (M := Sₘ) ((algebraMap R Sₘ : (a : R) → Sₘ) (↑y : R) : Sₘ)
have rw : IsUnit.{u_5} (M := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : Sₘ)
Tactic: rw [IsScalarTower.algebraMap_apply _ S]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) (mk' Rₘ x y) =
    mk'.{u_2, u_5} (R := S) (M := (Algebra.algebraMapSubmonoid S M : Submonoid S)) Sₘ
      ((algebraMap R S : (a : R) → S) x : S)
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
          ((algebraMap R S : (a : R) → S) (↑y : R)) ⋯ :
        ↥(Algebra.algebraMapSubmonoid S M))
have rw : Eq.{u_5 + 1} (α := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) (mk' Rₘ ((↑y : R) * x) y) : Sₘ)
  ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x : Rₘ) : Sₘ)
Tactic: rw [IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, ←
    IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ Sₘ,
    IsScalarTower.algebraMap_apply R Rₘ Sₘ, ← map_mul, mul_comm,
    IsLocalization.mul_mk'_eq_mk'_of_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
x : R
⊢ Eq.{u_5 + 1} (α := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x : Rₘ) : Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) x : S) : Sₘ)
have rw : Eq.{u_5 + 1} (α := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x : Rₘ) : Sₘ)
  ((algebraMap R Sₘ : (a : R) → Sₘ) x : Sₘ)
Tactic: rw [← IsScalarTower.algebraMap_apply R S Sₘ, ← IsScalarTower.algebraMap_apply R Rₘ Sₘ]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : Algebra R Sₘ
inst_10 : IsScalarTower R Rₘ Sₘ
inst_11 : IsScalarTower R S Sₘ
x : R
rw :
  Eq.{u_5 + 1} (α := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x : Rₘ) : Sₘ)
    ((algebraMap R Sₘ : (a : R) → Sₘ) x : Sₘ)
⊢ Eq.{u_5 + 1} (α := Sₘ) ((algebraMap Rₘ Sₘ : (a : Rₘ) → Sₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) x : Rₘ) : Sₘ)
    ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) x : S) : Sₘ)
have rw₁ : Eq.{u_5 + 1} (α := Sₘ) ((algebraMap R Sₘ : (a : R) → Sₘ) x : Sₘ) ((algebraMap R Sₘ : (a : R) → Sₘ) x : Sₘ)
Tactic: rw [← IsScalarTower.algebraMap_apply R S Sₘ, ← IsScalarTower.algebraMap_apply R Rₘ Sₘ]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
Rₘ : Type u_3
inst_2 : CommRing Rₘ
inst_3 : Algebra R Rₘ
inst_4 : IsLocalization M Rₘ
Sₘ : Type u_4
N : Submonoid S
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization N Sₘ
hf : M ≤ Submonoid.comap f N
hN : 0 ∉ N
inst_8 : IsDomain S
hf' : Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Injective.{u_3 + 1, u_4 + 1} (α := Rₘ) (β := Sₘ) (⇑(map Sₘ f hf) : (a : Rₘ) → Sₘ)
have refine : ∀ (x : Rₘ) (h : Eq.{u_4 + 1} (α := Sₘ) ((map Sₘ f hf : (a : Rₘ) → Sₘ) x : Sₘ) (0 : Sₘ)), x = 0
Tactic: refine (injective_iff_map_eq_zero (map Sₘ f hf)).mpr fun x h ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
Rₘ : Type u_3
inst_2 : CommRing Rₘ
inst_3 : Algebra R Rₘ
inst_4 : IsLocalization M Rₘ
Sₘ : Type u_4
N : Submonoid S
inst_5 : CommRing Sₘ
inst_6 : Algebra S Sₘ
inst_7 : IsLocalization N Sₘ
hf : M ≤ Submonoid.comap f N
hN : 0 ∉ N
inst_8 : IsDomain S
hf' : Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : Rₘ
h : Eq.{u_4 + 1} (α := Sₘ) ((map Sₘ f hf : (a : Rₘ) → Sₘ) x : Sₘ) (0 : Sₘ)
⊢ x = 0
have obtain : ∀ (x : R) (s : ↥M) (h : Eq.{u_4 + 1} (α := Sₘ) ((map Sₘ f hf : (a : Rₘ) → Sₘ) (mk' Rₘ x s) : Sₘ) (0 : Sₘ)),
  mk' Rₘ x s = 0
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
⊢ ((r.{u_1} (M := R) M : Con (R × ↥M)) : (a : R × ↥M) → R × ↥M → Prop) (a, b) (c, d) ↔ a * (↑d : R) = (↑b : R) * c
have simp : (∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)) ↔ a * (↑d : R) = (↑b : R) * c
Tactic: simp only [Localization.r_eq_r', Localization.r', Subtype.exists, exists_prop, Con.rel_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
⊢ (∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)) ↔ a * (↑d : R) = (↑b : R) * c
have refine : (∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)) →
  ∀ (u : R) (hu : u ∈ M) (h : u * ((↑d : R) * a) = u * ((↑b : R) * c)), a * (↑d : R) = (↑b : R) * c
Tactic: refine ⟨fun ⟨u, hu, h⟩ ↦ ?_,
    fun h ↦ ⟨1, Submonoid.one_mem M, by simpa only [one_mul, mul_comm a] using h⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
h_1 : ∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)
u : R
hu : u ∈ M
h : u * ((↑d : R) * a) = u * ((↑b : R) * c)
⊢ a * (↑d : R) = (↑b : R) * c
have hu' : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) u
Tactic: have hu' : u ∈ nonZeroDivisors R := hM hu
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
h_1 : ∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)
u : R
hu : u ∈ M
h : u * ((↑d : R) * a) = u * ((↑b : R) * c)
hu' : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) u
⊢ a * (↑d : R) = (↑b : R) * c
have hu'₁ : ∀ (x : R), u * x = 0 → x = 0
Tactic: simp only [mem_nonZeroDivisors_iff, mul_comm, and_self] at hu'
Cleared hypotheses: hu'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
h_1 : ∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)
u : R
hu : u ∈ M
h : u * ((↑d : R) * a) = u * ((↑b : R) * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
⊢ a * (↑d : R) = (↑b : R) * c
have rw : a * (↑d : R) - (↑b : R) * c = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
h_1 : ∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)
u : R
hu : u ∈ M
h : u * ((↑d : R) * a) = u * ((↑b : R) * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
⊢ a * (↑d : R) - (↑b : R) * c = 0
have a₁ : u * (a * (↑d : R) - (↑b : R) * c) = 0
Tactic: apply hu'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
h_1 : ∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)
u : R
hu : u ∈ M
h : u * ((↑d : R) * a) = u * ((↑b : R) * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
⊢ u * (a * (↑d : R) - (↑b : R) * c) = 0
have a₁ : u * (a * (↑d : R)) - u * ((↑b : R) * c) = 0
Tactic: rwa [mul_sub, sub_eq_zero, mul_comm a]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
h_1 : ∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)
u : R
hu : u ∈ M
h : u * ((↑d : R) * a) = u * ((↑b : R) * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
a₁ : u * (a * (↑d : R)) - u * ((↑b : R) * c) = 0
⊢ u * (a * (↑d : R) - (↑b : R) * c) = 0
have a₂ : u * (a * (↑d : R)) = u * ((↑b : R) * c)
Tactic: rwa [mul_sub, sub_eq_zero, mul_comm a]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
L : Type v
inst_1 : CommSemiring L
inst_2 : Algebra R L
S : Submonoid R
inst_3 : IsLocalization S L
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R
have this : #(Localization (M := R) S) ≤ #R
Tactic: have := Localization.cardinalMk_le S
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
L : Type v
inst_1 : CommSemiring L
inst_2 : Algebra R L
S : Submonoid R
inst_3 : IsLocalization S L
this : #(Localization (M := R) S) ≤ #R
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R
have rwa : ∀ (this : Cardinal.lift.{v, u} #(Localization (M := R) S) ≤ Cardinal.lift.{v, u} #R),
  Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R
Tactic: rwa [← lift_le.{v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
L : Type v
inst_1 : CommSemiring L
inst_2 : Algebra R L
S : Submonoid R
inst_3 : IsLocalization S L
this : #(Localization (M := R) S) ≤ #R
rwa :
  ∀ (this : Cardinal.lift.{v, u} #(Localization (M := R) S) ≤ Cardinal.lift.{v, u} #R),
    Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R
have rwa₁ : ∀ (this : Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R), Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R
Tactic: rwa [← lift_le.{v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ #(Localization (M := R) S) = #R
have hS₁ : S ≤ nonZeroDivisorsLeft R
Tactic: apply OreLocalization.cardinalMk
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommRing R
L : Type v
inst_1 : CommRing L
inst_2 : Algebra R L
S : Submonoid R
inst_3 : IsLocalization S L
hS : S ≤ R⁰
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R
have this : #(Localization (M := R) S) = #R
Tactic: have := Localization.cardinalMk hS
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
L : Type v
inst_1 : CommRing L
inst_2 : Algebra R L
S : Submonoid R
inst_3 : IsLocalization S L
hS : S ≤ R⁰
this : #(Localization (M := R) S) = #R
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R
have rwa : ∀ (this : Cardinal.lift.{v, u} #(Localization (M := R) S) = Cardinal.lift.{v, u} #R),
  Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R
Tactic: rwa [← lift_inj.{u, v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Cardinality (goal)
Goal:
R : Type u
inst : CommRing R
L : Type v
inst_1 : CommRing L
inst_2 : Algebra R L
S : Submonoid R
inst_3 : IsLocalization S L
hS : S ≤ R⁰
this : #(Localization (M := R) S) = #R
rwa :
  ∀ (this : Cardinal.lift.{v, u} #(Localization (M := R) S) = Cardinal.lift.{v, u} #R),
    Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R
have rwa₁ : ∀ (this : Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R), Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R
Tactic: rwa [← lift_inj.{u, v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ IsLocalization M S ↔
    (∀ (y : ↥M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)) ∧
      (∀ (z : S),
          ∃ (x : R × ↥M),
            HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1) ∧
        ∀ {x y : R},
          Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
            ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y
have rw : Submonoid.IsLocalizationMap.{u_1, u_2} (M := R) (N := S) M (⇑(algebraMap R S) : (a : R) → S) ↔
  (∀ (y : ↥M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)) ∧
    (∀ (z : S),
        ∃ (x : R × ↥M),
          HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1) ∧
      ∀ {x y : R},
        Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
          ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y
Tactic: rw [isLocalization_iff_isLocalizationMap, Submonoid.isLocalizationMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
rw :
  Submonoid.IsLocalizationMap.{u_1, u_2} (M := R) (N := S) M (⇑(algebraMap R S) : (a : R) → S) ↔
    (∀ (y : ↥M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)) ∧
      (∀ (z : S),
          ∃ (x : R × ↥M),
            HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1) ∧
        ∀ {x y : R},
          Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
            ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y
⊢ IsLocalization M S ↔
    (∀ (y : ↥M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)) ∧
      (∀ (z : S),
          ∃ (x : R × ↥M),
            HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1) ∧
        ∀ {x y : R},
          Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
            ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y
have rw₁ : ((∀ (y : ↥M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)) ∧
    (∀ (z : S),
        ∃ (x : R × ↥M),
          HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1) ∧
      ∀ {x y : R},
        Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
          ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y) ↔
  (∀ (y : ↥M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)) ∧
    (∀ (z : S),
        ∃ (x : R × ↥M),
          HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) = (algebraMap R S : (a : R) → S) x.1) ∧
      ∀ {x y : R},
        Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
          ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y
Tactic: rw [isLocalization_iff_isLocalizationMap, Submonoid.isLocalizationMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)
x y : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) →
    ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * y
have rw : (∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y) → ∃ (c : ↥N), (↑c : R) * x = (↑c : R) * y
Tactic: rw [IsLocalization.eq_iff_exists M]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S) ↔ ∃ m ∈ M, x ∣ m
have refine : ∀ (h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)), ∃ m ∈ M, x ∣ m
Tactic: refine ⟨fun h ↦ ?_, fun ⟨m, hm, dvd⟩ ↦ isUnit_of_dvd_unit (map_dvd _ dvd) (map_units S ⟨m, hm⟩)⟩