awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
P : Type u_3
inst_3 : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
h₁ : inst_2 = RingHom.toAlgebra (algebraMap R S)
⊢ inst_2 = RingHom.toAlgebra (RingHom.comp (algebraMap R S) (h.symm.toRingHom.comp h.symm.symm.toRingHom))

Tactic:
simp only [RingHom.comp_id, RingEquiv.symm_symm, RingEquiv.symm_toRingHom_comp_toRingHom]

Premises used: RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.comp_id, RingEquiv.symm_symm
-- 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
P : Type u_3
inst_3 : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
h₁ : ∀ (r : R), Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
⊢ inst_2 = RingHom.toAlgebra (algebraMap R S)

Tactic:
apply Algebra.algebra_ext

Premises used: Algebra.algebra_ext
-- 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
P : Type u_3
inst_3 : CommSemiring P
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
r : R
h₁ h₂ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)

Tactic:
rw [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
K : Type u_5
inst_2 : CommSemiring K
inst_3 : Algebra R K
e : R ≃+* S
inst_4 : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K)
      ((algebraMap S K : (a : S) → K) ((e : (a : R) → S) x : S) : K)
inst_5 : IsLocalization M₁ K
rw : IsLocalization M₁ K
⊢ IsLocalization M₂ K

Tactic:
rw [IsLocalization.isLocalization_iff_of_base_ringEquiv _ _ e, hM]

Premises used: IsLocalization.isLocalization_iff_of_base_ringEquiv
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
K : Type u_5
inst_2 : CommSemiring K
inst_3 : Algebra R K
e : R ≃+* S
inst_4 : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K)
      ((algebraMap S K : (a : S) → K) ((e : (a : R) → S) x : S) : K)
inst_5 : IsLocalization M₁ K
⊢ IsLocalization M₁ K

Tactic:
(inferInstance : IsLocalization M₁ K)

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
K : Type u_5
inst_2 : CommSemiring K
inst_3 : Algebra R K
e : R ≃+* S
inst_4 : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K)
      ((algebraMap S K : (a : S) → K) ((e : (a : R) → S) x : S) : K)
inst_5 : IsLocalization M₁ K
h₁ : RingHom.toAlgebra (RingHom.comp (algebraMap R K) e.symm.toRingHom) = inst_4
⊢ IsLocalization M₁ K

Tactic:
convert! (inferInstance : IsLocalization M₁ K)

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
K : Type u_5
inst_2 : CommSemiring K
inst_3 : Algebra R K
e : R ≃+* S
inst_4 : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K)
      ((algebraMap S K : (a : S) → K) ((e : (a : R) → S) x : S) : K)
inst_5 : IsLocalization M₁ K
⊢ ∀ (r : S), Eq.{u_5 + 1} (α := K) ((algebraMap S K : (a : S) → K) r : K) ((algebraMap S K : (a : S) → K) r : K)

Tactic:
simp [RingHom.algebraMap_toAlgebra, h]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
K : Type u_5
inst_2 : CommSemiring K
inst_3 : Algebra R K
e : R ≃+* S
inst_4 : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K)
      ((algebraMap S K : (a : S) → K) ((e : (a : R) → S) x : S) : K)
inst_5 : IsLocalization M₁ K
⊢ RingHom.toAlgebra (RingHom.comp (algebraMap R K) e.symm.toRingHom) = inst_4

Tactic:
exact Algebra.algebra_ext _ _ (by simp [RingHom.algebraMap_toAlgebra, h])

Premises used: Algebra.algebra_ext
-- 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
⊢ LE.le (α := Submonoid R) (nonZeroDivisors R) (Submonoid.comap (F := R →+* S) (algebraMap R S) (nonZeroDivisors S))

Tactic:
(toLocalizationMap M S).nonZeroDivisors_le_comap

Premises used: Set.Mem, setOf, Submonoid.LocalizationMap.nonZeroDivisors_le_comap, IsLocalization.toLocalizationMap
-- 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
⊢ LE.le (α := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) (nonZeroDivisors R) : Submonoid S)
    (nonZeroDivisors S : Submonoid S)

Tactic:
(toLocalizationMap M S).map_nonZeroDivisors_le

Premises used: Set.Mem, setOf, Submonoid.LocalizationMap.map_nonZeroDivisors_le, IsLocalization.toLocalizationMap
-- 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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
change : a = mk 1 1
⊢ a = default

Tactic:
change a = mk 1 1

Premises used: Localization.mk, OfNat.ofNat
-- 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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
with_unfolding_all : a = mk 1 1
⊢ a = default

Tactic:
with_unfolding_all change a = mk 1 1

Premises used: Localization.mk, OfNat.ofNat
-- 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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
x : R × ↥M
e_x : x.1 = 1
e_y : x.2 = 1
⊢ Eq (α := Localization (M := R) M) (mk x.1 x.2) (mk 1 1)

Tactic:
congr
-- 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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
x : R × ↥M
⊢ x.1 = 1

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- 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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
x : R × ↥M
⊢ x.2 = 1

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- 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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Subsingleton R
a : Localization (M := R) M
⊢ a = mk 1 1

Tactic:
exact Localization.induction_on a fun _ => by
      congr <;> apply Subsingleton.elim
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a + (↑b : R) * c) (d * b)
⊢ HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑b : R) * c + (↑d : R) * a) (b * d)

Tactic:
rw [add_comm (b * c) (d * a), mul_comm b d]

Premises used: HMul.hMul, add_comm, mul_comm, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a + (↑b : R) * c) (d * b)

Tactic:
OreLocalization.oreDiv_add_oreDiv

Premises used: Localization.mk, OreLocalization.oreNum, OreLocalization.oreDiv_add_oreDiv
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a + (↑b : R) * c) (d * b)

Tactic:
exact OreLocalization.oreDiv_add_oreDiv

Premises used: OreLocalization.oreDiv_add_oreDiv
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
rw :
  ((r'.{u_1} (M := R) M : Con (R × ↥M)) : (a : R × ↥M) → R × ↥M → Prop) ((↑b : R) * c + (↑b : R) * a, b * b) (a + c, b)
⊢ HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk c b) = mk (a + c) b

Tactic:
rw [add_mk, mk_eq_mk_iff, r_eq_r']

Premises used: Localization.r_eq_r', Localization.add_mk, Localization.mk_eq_mk_iff
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ ((r'.{u_1} (M := R) M : Con (R × ↥M)) : (a : R × ↥M) → R × ↥M → Prop) ((↑b : R) * c + (↑b : R) * a, b * b) (a + c, b)

Tactic:
(r' M).symm ⟨1, ?_⟩

Premises used: Con.symm, Localization.r', Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
refine :
  (↑1 : R) * ((↑((↑b : R) * c + (↑b : R) * a, b * b).2 : R) * (a + c, b).1) =
    (↑1 : R) * ((↑(a + c, b).2 : R) * ((↑b : R) * c + (↑b : R) * a, b * b).1)
⊢ ((r'.{u_1} (M := R) M : Con (R × ↥M)) : (a : R × ↥M) → R × ↥M → Prop) ((↑b : R) * c + (↑b : R) * a, b * b) (a + c, b)

Tactic:
refine (r' M).symm ⟨1, ?_⟩

Premises used: Con.symm, Localization.r', Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
simp : 1 * ((↑b : R) * (↑b : R) * (a + c)) = 1 * ((↑b : R) * ((↑b : R) * c + (↑b : R) * a))
⊢ (↑1 : R) * ((↑((↑b : R) * c + (↑b : R) * a, b * b).2 : R) * (a + c, b).1) =
    (↑1 : R) * ((↑(a + c, b).2 : R) * ((↑b : R) * c + (↑b : R) * a, b * b).1)

Tactic:
simp only [Submonoid.coe_one, Submonoid.coe_mul]

Premises used: Submonoid.coe_one, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ 1 * ((↑b : R) * (↑b : R) * (a + c)) = 1 * ((↑b : R) * ((↑b : R) * c + (↑b : R) * a))

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
ι : Type u_4
f : ι → R
s : Finset ι
b : ↥M
⊢ Eq.{u_1 + 1} (α := Localization (M := R) M) (mk (∑ i ∈ s, f i) b) (∑ i ∈ s, mk (f i) b)

Tactic:
map_sum (mkAddMonoidHom b) f s

Premises used: Localization.mk, map_sum, Quotient.mk', Localization.mkAddMonoidHom, OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
l : List R
b : ↥M
⊢ Eq (α := Localization (M := R) M) (mk l.sum b) (List.sum (List.map (fun (a : R) ↦ mk a b) l))

Tactic:
map_list_sum (mkAddMonoidHom b) l

Premises used: Localization.mk, map_list_sum, Quotient.mk', Localization.mkAddMonoidHom, OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
l : Multiset R
b : ↥M
⊢ Eq (α := Localization (M := R) M) (mk l.sum b) (Multiset.sum (Multiset.map (fun (a : R) ↦ mk a b) l))

Tactic:
(mkAddMonoidHom b).map_multiset_sum l

Premises used: Localization.mk, Quotient.mk', AddMonoidHom.map_multiset_sum, Localization.mkAddMonoidHom, OreLocalization.oreDiv
-- 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
P : Type u_3
inst_3 : CommSemiring P
⊢ IsLocalization M (Localization (M := R) M)

Tactic:
⟨(Localization.monoidOf M).isLocalizationMap⟩

Premises used: Submonoid.LocalizationMap.isLocalizationMap, IsLocalization'.mk, Localization.monoidOf
-- 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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : NoZeroDivisors R
⊢ NoZeroDivisors.{u_1} (Localization (M := R) M)

Tactic:
IsLocalization.noZeroDivisors M

Premises used: IsLocalization.noZeroDivisors
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
⊢ toLocalizationMap M (Localization (M := R) M) = monoidOf M

Tactic:
rfl

Premises used: Localization.mk, Set.Mem, Quotient.mk', Localization.monoidOf, OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
x : R
⊢ Eq (α := Localization (M := R) M) ((monoidOf M : (a : R) → Localization M) x : Localization (M := R) M)
    ((algebraMap R (Localization (M := R) M) : (a : R) → Localization M) x : Localization (M := R) M)

Tactic:
rfl

Premises used: Localization.mk, Set.Mem, Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
x : R
⊢ Eq (α := Localization (M := R) M) (mk x 1) ((algebraMap R (Localization (M := R) M) : (a : R) → Localization M) x)

Tactic:
rfl

Premises used: Localization.mk, Set.Mem, Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
x : R
y : ↥M
rw :
  Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y) (mk' (Localization (M := R) M) x y)
rw₁ :
  Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y)
    (Submonoid.LocalizationMap.mk' (toLocalizationMap M (Localization (M := R) M)) x y)
rw₂ rw₃ :
  Eq (α := Localization (M := R) M) (Submonoid.LocalizationMap.mk' (monoidOf M) x y)
    (Submonoid.LocalizationMap.mk' (monoidOf M) x y)
⊢ Eq (α := Localization (M := R) M) (mk x y) (mk' (Localization (M := R) M) x y)

Tactic:
rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]

Premises used: Localization.toLocalizationMap_eq_monoidOf, Localization.mk_eq_monoidOf_mk'_apply, IsLocalization.mk'
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
⊢ Eq.{u_1 + 1} (α := (x : R) → (y : ↥M) → Localization (M := R) M)
    (mk.{u_1} (M := R) (S := M) : (x : R) → (y : ↥M) → Localization (M := R) M)
    (mk' (Localization (M := R) M) : (x : R) → (y : ↥M) → Localization (M := R) M)

Tactic:
mk_eq_monoidOf_mk'

Premises used: Localization.mk_eq_monoidOf_mk', Localization.mk, Set.Mem, IsLocalization.mk', Quotient.mk', Localization.monoidOf, OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
m : A
rw :
  Eq (α := Localization (M := R) M)
    ((algebraMap R (Localization (M := R) M) : (a : R) → Localization M) ((algebraMap A R : (a : A) → R) m) :
      Localization (M := R) M)
    ((algebraMap A (Localization (M := R) M) : (a : A) → Localization M) m : Localization (M := R) M)
⊢ Eq.{u_1 + 1} (α := Localization (M := R) M) (mk ((algebraMap A R : (a : A) → R) m) 1 : Localization (M := R) M)
    ((algebraMap A (Localization (M := R) M) : (a : A) → Localization M) m : Localization (M := R) M)

Tactic:
rw [mk_eq_mk', mk'_eq_iff_eq_mul, Submonoid.coe_one, map_one, mul_one]

Premises used: Localization.mk_eq_mk', Submonoid.coe_one, IsLocalization.mk'_eq_iff_eq_mul, map_one, mul_one
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra A R
m : A
⊢ Eq (α := Localization (M := R) M)
    ((algebraMap R (Localization (M := R) M) : (a : R) → Localization M) ((algebraMap A R : (a : A) → R) m) :
      Localization (M := R) M)
    ((algebraMap A (Localization (M := R) M) : (a : A) → Localization M) m : Localization (M := R) M)

Tactic:
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
inst_3 : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
mp : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S) → x = 0
mpr : x = 0 → Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S) ↔ x = 0

Tactic:
constructor
-- 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
x : R
hM : M ≤ nonZeroDivisors R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
mp : ∀ (c : ↥M) (hc : (↑c : R) * x = 0), x = 0
⊢ x = 0

Tactic:
obtain ⟨c, hc⟩ := (map_eq_zero_iff M _ _).mp h

Premises used: IsLocalization.map_eq_zero_iff, Iff.mp
-- 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
x : R
hM : M ≤ nonZeroDivisors R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
c : ↥M
hc : (↑c : R) * x = 0
⊢ x = 0

Tactic:
(hM c.2).1 x hc

Premises used: And.left, Subtype.property
-- 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
x : R
hM : M ≤ nonZeroDivisors R
h : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
c : ↥M
hc : (↑c : R) * x = 0
⊢ x = 0

Tactic:
exact (hM c.2).1 x hc

Premises used: And.left, Subtype.property
-- 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
x : R
hM : M ≤ nonZeroDivisors R
h : x = 0
mpr : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) (0 : S)
mpr₁ mpr₂ : Eq.{u_2 + 1} (α := S) 0 0
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- 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
hM : ∀ m ∈ M, IsRegular m
⊢ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
(toLocalizationMap M S).injective_iff.mpr hM

Premises used: Iff.mpr, Submonoid.LocalizationMap.injective_iff, IsLocalization.toLocalizationMap
-- 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
inst_4 : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
rw : ¬x = 0
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)

Tactic:
rw [Ne, to_map_eq_zero_iff S hM]

Premises used: IsLocalization.to_map_eq_zero_iff, Ne
-- 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
inst_4 : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ ¬x = 0

Tactic:
nonZeroDivisors.ne_zero hx

Premises used: nonZeroDivisors.ne_zero
-- 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
inst_4 : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ ¬x = 0

Tactic:
exact nonZeroDivisors.ne_zero hx

Premises used: nonZeroDivisors.ne_zero
-- 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
inst_4 : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : S
⊢ (↑(sec M x).2 : R) ≠ 0

Tactic:
nonZeroDivisors.coe_ne_zero ⟨(sec M x).snd.val, hM (sec M x).snd.property⟩

Premises used: IsLocalization.sec, Subtype.mk, nonZeroDivisors.coe_ne_zero, Subtype.val, Prod.snd, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsDomain R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
⊢ IsDomain.{u_1} (Localization (M := R) M)

Tactic:
isDomain_of_le_nonZeroDivisors _ hM

Premises used: IsLocalization.isDomain_of_le_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
a : R
b : ↥M
⊢ Eq (α := Localization (M := R) M) (-mk a b) (mk (-a) b)

Tactic:
OreLocalization.neg_def _ _

Premises used: Localization.mk, OreLocalization.neg_def
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
a c : R
b d : ↥M
rw : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (-mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₁ : HAdd.hAdd (α := Localization (M := R) M) (mk a b) (mk (-c) d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)
rw₂ :
  Eq (α := Localization (M := R) M) (mk ((↑b : R) * -c + (↑d : R) * a) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
rw₃ :
  Eq (α := Localization (M := R) M) (mk ((↑d : R) * a + (↑b : R) * -c) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
rw₄ :
  Eq (α := Localization (M := R) M) (mk ((↑d : R) * a + -((↑b : R) * c)) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
rw₅ rw₆ :
  Eq (α := Localization (M := R) M) (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
    (mk ((↑d : R) * a - (↑b : R) * c) (b * d))
⊢ HSub.hSub (α := Localization (M := R) M) (mk a b) (mk c d) = mk ((↑d : R) * a - (↑b : R) * c) (b * d)

Tactic:
rw [sub_eq_add_neg, neg_mk, add_mk, add_comm, mul_neg, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, add_comm, Localization.add_mk, Localization.neg_mk, mul_neg
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
rw : -mk' S x y = mk' S (-x) y
rw₁ :
  HMul.hMul (β := S) (-mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
rw₂ :
  -HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) (-x)
rw₃ : -HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) = -(algebraMap R S : (a : R) → S) x
rw₄ rw₅ : Eq.{u_2 + 1} (α := S) (-(algebraMap R S : (a : R) → S) x : S) (-(algebraMap R S : (a : R) → S) x : S)
⊢ mk' S (-x) y = -mk' S x y

Tactic:
rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]

Premises used: map_neg, eq_comm, neg_mul, IsLocalization.eq_mk'_iff_mul_eq, IsLocalization.mk'_spec