awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Basic
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 S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : Sₘ)

Tactic:
exact IsLocalization.map_units Sₘ ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩

Premises used: Algebra.algebraMap, Subtype.mk, IsLocalization.map_units, Subtype.val, DFunLike.coe, Algebra.mem_algebraMapSubmonoid_of_mem
-- Module: Mathlib.RingTheory.Localization.Basic
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
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ₘ)
⊢ (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))

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]

Premises used: Subtype.coe_mk, map_mul, mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.eq_mk'_iff_mul_eq, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
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
⊢ 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:
congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)

Premises used: Algebra.algebraMap, IsLocalization.mk'_mul_cancel_left, congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Basic
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
⊢ 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:
exact congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)

Premises used: Algebra.algebraMap, IsLocalization.mk'_mul_cancel_left, congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Basic
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ₘ)
rw₁ rw₂ : Eq.{u_5 + 1} (α := Sₘ) ((algebraMap R Sₘ : (a : R) → Sₘ) x : 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ₘ)

Tactic:
rw [← IsScalarTower.algebraMap_apply R S Sₘ, ← IsScalarTower.algebraMap_apply R Rₘ Sₘ]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
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ₘ) x : Sₘ)
    ((map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯ : (a : Rₘ) → Sₘ) x : Sₘ)

Tactic:
DFunLike.congr_fun (IsLocalization.algebraMap_eq_map_map_submonoid _ _ _ _) x

Premises used: DFunLike.congr_fun, IsLocalization.algebraMap_eq_map_map_submonoid
-- Module: Mathlib.RingTheory.Localization.Basic
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ₘ
⊢ Eq (α := Rₘ →+* Sₘ) (lift.{u_1, u_4, u_5} (R := R) (M := M) (g := algebraMap R Sₘ) ⋯) (algebraMap Rₘ Sₘ)

Tactic:
IsLocalization.lift_unique _ fun _ => (IsScalarTower.algebraMap_apply _ _ _ _).symm

Premises used: IsLocalization.lift_unique, Eq.symm, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
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ₘ
⊢ Eq (α := Rₘ →+* Sₘ) (algebraMap Rₘ Sₘ) (map (M := M) (T := Algebra.algebraMapSubmonoid S M) Sₘ (algebraMap R S) ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Basic
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ₘ
hRS : Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Injective.{u_4 + 1, u_5 + 1} (α := Rₘ) (β := Sₘ) (⇑(algebraMap Rₘ Sₘ) : (a : Rₘ) → Sₘ)

Tactic:
have : IsLocalization (M.map (algebraMap R S)) Sₘ := i
  IsLocalization.map_injective_of_injective _ _ _ hRS

Premises used: IsLocalization.map_injective_of_injective
-- Module: Mathlib.RingTheory.Localization.Basic
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
Rₘ : Type u_4
Sₘ : Type u_5
inst_4 : CommSemiring Rₘ
inst_5 : CommSemiring Sₘ
inst_6 : Algebra R Rₘ
inst_7 : IsLocalization M Rₘ
inst_8 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
⊢ IsLocalization (Algebra.algebraMapSubmonoid R M) Rₘ

Tactic:
simpa
-- Module: Mathlib.RingTheory.Localization.Basic
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ₘ)

Tactic:
(injective_iff_map_eq_zero (map Sₘ f hf)).mpr fun x h ↦ ?_

Premises used: Iff.mpr, IsLocalization.map, injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Localization.Basic
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)
refine : ∀ (x : Rₘ) (h : Eq.{u_4 + 1} (α := Sₘ) ((map Sₘ f hf : (a : Rₘ) → Sₘ) x : Sₘ) (0 : Sₘ)), x = 0
⊢ Injective.{u_3 + 1, u_4 + 1} (α := Rₘ) (β := Sₘ) (⇑(map Sₘ f hf) : (a : Rₘ) → Sₘ)

Tactic:
refine (injective_iff_map_eq_zero (map Sₘ f hf)).mpr fun x h ↦ ?_

Premises used: Iff.mpr, IsLocalization.map, injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Localization.Basic
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ₘ)
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
⊢ x = 0

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Basic
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
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:
aesop (add simp [map_mk', mk'_eq_zero_iff])

Premises used: IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
m : ℤ
⊢ Eq.{u_1 + 1} (α := Localization (M := R) M) (mk (↑m : R) 1) (↑m : Localization M)

Tactic:
simpa using mk_algebraMap (R := R) (A := ℤ) _

Premises used: Localization.mk_algebraMap
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
simp : (∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑b : R) * c)) ↔ a * (↑d : R) = (↑b : R) * c
⊢ ((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

Tactic:
simp only [Localization.r_eq_r', Localization.r', Subtype.exists, exists_prop, Con.rel_mk]

Premises used: Localization.r_eq_r', Con.rel_mk, Subtype.exists, exists_prop, Localization.r'
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
h : a * (↑d : R) = (↑b : R) * c
⊢ 1 * ((↑d : R) * a) = 1 * ((↑b : R) * c)

Tactic:
simpa only [one_mul, mul_comm a] using h

Premises used: mul_comm, one_mul
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
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
⊢ (∃ a_1 ∈ M, a_1 * ((↑d : R) * a) = a_1 * ((↑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⟩⟩
-- Module: Mathlib.RingTheory.Localization.Basic
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)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) u

Tactic:
have hu' : u ∈ nonZeroDivisors R := hM hu
-- Module: Mathlib.RingTheory.Localization.Basic
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
⊢ ∀ (x : R), u * x = 0 → x = 0

Tactic:
simp only [mem_nonZeroDivisors_iff, mul_comm, and_self] at hu'

Premises used: mem_nonZeroDivisors_iff, and_self, mul_comm
-- Module: Mathlib.RingTheory.Localization.Basic
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
rw : a * (↑d : R) - (↑b : R) * c = 0
⊢ a * (↑d : R) = (↑b : R) * c

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.Localization.Basic
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) - (↑b : R) * c) = 0
⊢ a * (↑d : R) - (↑b : R) * c = 0

Tactic:
apply hu'
-- Module: Mathlib.RingTheory.Localization.Basic
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
a₂ : u * (a * (↑d : R)) = u * ((↑b : R) * c)
a₃ a₄ a₅ a₆ : u * ((↑d : R) * a) = u * ((↑b : R) * c)
⊢ u * (a * (↑d : R) - (↑b : R) * c) = 0

Tactic:
rwa [mul_sub, sub_eq_zero, mul_comm a]

Premises used: mul_sub, sub_eq_zero, mul_comm
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring L
inst_3 : Semiring B
W : Submonoid A
inst_4 : Algebra A L
inst_5 : IsLocalization W L
inst_6 : Algebra R A
inst_7 : Algebra R L
inst_8 : IsScalarTower R A L
inst_9 : Algebra R B
f g : L →ₐ[R] B
h : Eq (α := A →ₐ[R] B) (f.comp (Algebra.algHom R A L)) (g.comp (Algebra.algHom R A L))
⊢ f = g

Tactic:
AlgHom.coe_ringHom_injective <| IsLocalization.ringHom_ext W <| RingHom.ext <| AlgHom.ext_iff.mp h

Premises used: AlgHom.coe_ringHom_injective, AlgHom.ext_iff, RingHom.ext, Iff.mp, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
W : Submonoid A
f g : AlgHom.{u_1, u_2, u_3} R (Localization (M := A) W) B
h :
  Eq (α := A →ₐ[R] B) (f.comp (Algebra.algHom R A (Localization (M := A) W)))
    (g.comp (Algebra.algHom R A (Localization (M := A) W)))
⊢ f = g

Tactic:
IsLocalization.algHom_ext W h

Premises used: IsLocalization.algHom_ext
-- Module: Mathlib.RingTheory.Localization.Cardinality
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
⊢ #(Localization (M := R) S) ≤ #R

Tactic:
have := Localization.cardinalMk_le S
-- Module: Mathlib.RingTheory.Localization.Cardinality
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
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Cardinal.lift.{u, v} #L ≤ 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

Tactic:
rwa [← lift_le.{v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this

Premises used: Iff.mpr, Localization.algEquiv, Cardinal.lift_mk_eq', Nonempty.intro, AlgEquiv.toEquiv
-- Module: Mathlib.RingTheory.Localization.Cardinality
Goal:
R : Type u
inst : CommSemiring R
L : Type u
inst_1 : CommSemiring L
inst_2 : Algebra R L
S : Submonoid R
inst_3 : IsLocalization S L
⊢ #L ≤ #R

Tactic:
simpa using lift_cardinalMk_le (L := L) S

Premises used: IsLocalization.lift_cardinalMk_le
-- Module: Mathlib.RingTheory.Localization.Cardinality
Goal:
R : Type u
inst : CommRing R
S : Submonoid R
hS : S ≤ R⁰
hS₁ : S ≤ nonZeroDivisorsLeft R
⊢ #(Localization (M := R) S) = #R

Tactic:
apply OreLocalization.cardinalMk

Premises used: OreLocalization.cardinalMk
-- Module: Mathlib.RingTheory.Localization.Cardinality
Goal:
R : Type u
inst : CommRing R
S : Submonoid R
hS : S ≤ R⁰
hS₁ hS₂ hS₃ hS₄ : S ≤ R⁰
⊢ S ≤ nonZeroDivisorsLeft R

Tactic:
rwa [nonZeroDivisorsLeft_eq_nonZeroDivisors]

Premises used: nonZeroDivisorsLeft_eq_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.Cardinality
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⁰
⊢ #(Localization (M := R) S) = #R

Tactic:
have := Localization.cardinalMk hS
-- Module: Mathlib.RingTheory.Localization.Cardinality
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
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Cardinal.lift.{u, v} #L = 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

Tactic:
rwa [← lift_inj.{u, v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this

Premises used: Iff.mpr, Localization.algEquiv, Cardinal.lift_mk_eq', Nonempty.intro, AlgEquiv.toEquiv
-- Module: Mathlib.RingTheory.Localization.Cardinality
Goal:
R : Type u
inst : CommRing R
L : Type u
inst_1 : CommRing L
inst_2 : Algebra R L
S : Submonoid R
inst_3 : IsLocalization S L
hS : S ≤ R⁰
⊢ #L = #R

Tactic:
simpa using lift_cardinalMk L S hS

Premises used: IsLocalization.lift_cardinalMk
-- Module: Mathlib.RingTheory.Localization.Cardinality
Goal:
R : Type u
inst : CommRing R
⊢ #(FractionRing R) = #R

Tactic:
IsLocalization.cardinalMk (FractionRing R) R⁰ le_rfl

Premises used: IsLocalization.cardinalMk, le_rfl, FractionRing, nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.Cardinality
Goal:
R : Type u
inst : CommRing R
L : Type v
inst_1 : CommRing L
inst_2 : Algebra R L
inst_3 : IsFractionRing R L
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R

Tactic:
IsLocalization.lift_cardinalMk L _ le_rfl

Premises used: IsLocalization.lift_cardinalMk, le_rfl
-- Module: Mathlib.RingTheory.Localization.Cardinality
Goal:
R : Type u
inst : CommRing R
L : Type u
inst_1 : CommRing L
inst_2 : Algebra R L
inst_3 : IsFractionRing R L
⊢ #L = #R

Tactic:
IsLocalization.cardinalMk L _ le_rfl

Premises used: IsLocalization.cardinalMk, le_rfl
-- Module: Mathlib.RingTheory.Localization.Defs
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 ↔ Submonoid.IsLocalizationMap.{u_1, u_2} (M := R) (N := S) M (⇑(algebraMap R S) : (a : R) → S)

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: Algebra.algebraMap, IsLocalization'.mk, Submonoid.IsLocalizationMap, _private.0.isLocalization_iff_isLocalizationMap.match_1, Iff.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Defs
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
rw₁ 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
⊢ 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

Tactic:
rw [isLocalization_iff_isLocalizationMap, Submonoid.isLocalizationMap_iff]

Premises used: Submonoid.isLocalizationMap_iff, isLocalization_iff_isLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
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
⊢ ∀ (y : ↥M), IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)

Tactic:
IsLocalization'.toIsLocalizationMap.map_units

Premises used: Submonoid.IsLocalizationMap.map_units, Set.Mem, IsLocalization'.toIsLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
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
⊢ ∀ (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

Tactic:
IsLocalization'.toIsLocalizationMap.surj

Premises used: Set.Mem, IsLocalization'.toIsLocalizationMap, Submonoid.IsLocalizationMap.surj