awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rn : R
hn :
  Eq.{u_2 + 1} (α := S ⧸ I)
    ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
        (HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I)) (β :=
          HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
                (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
              m :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I : Ideal R))) :
      S ⧸ I)
    ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I) 1 : S ⧸ I)
⊢ HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
              (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
            m) :
        S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn) :
        S ⧸ I) =
    1

Tactic:
rw [map_one, map_mul] at hn

Premises used: map_mul, map_one
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rn : R
hn :
  HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
              (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
            m) :
        S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn) :
        S ⧸ I) =
    1
neg :
  Eq (α := S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((algebraMap R S : R →+* S) : (a : R) → S) (r * rn)) : S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S)
          (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm))) :
      S ⧸ I)
⊢ Eq.{u_2 + 1} (α := S ⧸ I)
    (((Ideal.quotientMap I (algebraMap R S) H : RingHom.{u_1, u_2} (R ⧸ J) (S ⧸ I)) : (a : R ⧸ J) → S ⧸ I)
        ((Ideal.Quotient.mk J : (a : R) → R ⧸ J) (r * rn)) :
      S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)

Tactic:
rw [Ideal.quotientMap_mk, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem, ←
      Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, mk'_eq_mul_mk'_one]

Premises used: map_sub, sub_eq_zero, IsLocalization.mk'_eq_mul_mk'_one, Ideal.quotientMap_mk, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rn : R
hn :
  HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
              (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
            m) :
        S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn) :
        S ⧸ I) =
    1
neg :
  Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((algebraMap R S : R →+* S) : (a : R) → S) rn) : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I) ∨
    Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((algebraMap R S : R →+* S) : (a : R) → S) r) : S ⧸ I)
      (0 : S ⧸ I)
⊢ Eq (α := S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((algebraMap R S : R →+* S) : (a : R) → S) (r * rn)) : S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S)
          (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm))) :
      S ⧸ I)

Tactic:
simp only [mul_eq_mul_left_iff, map_mul]

Premises used: mul_eq_mul_left_iff, map_mul
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rn : R
hn :
  HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
              (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
            m) :
        S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn) :
        S ⧸ I) =
    1
⊢ Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((algebraMap R S : R →+* S) : (a : R) → S) rn) : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I) ∨
    Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((algebraMap R S : R →+* S) : (a : R) → S) r) : S ⧸ I)
      (0 : S ⧸ I)

Tactic:
Or.inl
        (mul_left_cancel₀ (M₀ := S ⧸ I)
          (fun hn =>
            hM
              (Ideal.Quotient.eq_zero_iff_mem.2
                (Ideal.mem_comap.2 (Ideal.Quotient.eq_zero_iff_mem.1 hn))))
          (_root_.trans hn ?_))

Premises used: Iff.mpr, trans, mul_left_cancel₀, Ideal.Quotient.eq_zero_iff_mem, Iff.mp, Or.inl, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rn : R
hn :
  HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
              (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
            m) :
        S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn) :
        S ⧸ I) =
    1
neg :
  1 =
    HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) ((algebraMap R S : (a : R) → S) m) : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
⊢ Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((algebraMap R S : R →+* S) : (a : R) → S) rn) : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I) ∨
    Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (((algebraMap R S : R →+* S) : (a : R) → S) r) : S ⧸ I)
      (0 : S ⧸ I)

Tactic:
refine
      Or.inl
        (mul_left_cancel₀ (M₀ := S ⧸ I)
          (fun hn =>
            hM
              (Ideal.Quotient.eq_zero_iff_mem.2
                (Ideal.mem_comap.2 (Ideal.Quotient.eq_zero_iff_mem.1 hn))))
          (_root_.trans hn ?_))

Premises used: Iff.mpr, trans, mul_left_cancel₀, Ideal.Quotient.eq_zero_iff_mem, Iff.mp, Or.inl, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal S
inst_4 : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R I))
r m : R
hm : m ∈ M
hM :
  ¬Eq (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
            (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
          m :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) I))
rn : R
hn :
  HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.comap (F := R →+* S) (algebraMap R S) I) :
              (a : R) → R ⧸ Ideal.comap (algebraMap R S) I)
            m) :
        S ⧸ I)
      ((Ideal.quotientMap I (algebraMap R S) ⋯ : (a : R ⧸ Ideal.comap (algebraMap R S) I) → S ⧸ I)
          ((Ideal.Quotient.mk (Ideal.under R I) : (a : R) → R ⧸ Ideal.under R I) rn) :
        S ⧸ I) =
    1
neg :
  Eq (α := S ⧸ I) (1 : S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) m : S)
          (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm))) :
      S ⧸ I)
neg₁ :
  Eq (α := S ⧸ I) (1 : S ⧸ I)
    ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S m (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)
neg₂ : Eq (α := S ⧸ I) 1 ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) 1)
neg₃ neg₄ : Eq.{u_2 + 1} (α := S ⧸ I) 1 1
⊢ 1 =
    HMul.hMul (α := S ⧸ I) (β := S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) ((algebraMap R S : (a : R) → S) m) : S ⧸ I)
      ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)) : S ⧸ I)

Tactic:
rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, map_one]

Premises used: IsLocalization.mk'_eq_mul_mk'_one, IsLocalization.mk'_self, map_mul, map_one
-- Module: Mathlib.RingTheory.Localization.Ideal
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
inst_4 : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
⊢ IsDomain S

Tactic:
haveI : IsDomain S := isDomain_of_le_nonZeroDivisors _ hM
-- Module: Mathlib.RingTheory.Localization.Ideal
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
inst_4 : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
this : IsDomain S
rw : LT.lt (α := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) ⊥) (Ideal.under R p)
⊢ LT.lt (α := Ideal R) ⊥ (Ideal.under R p)

Tactic:
rw [← Ideal.comap_bot_of_injective (algebraMap R S) (IsLocalization.injective _ hM)]

Premises used: Algebra.algebraMap, IsLocalization.injective, Ideal.comap_bot_of_injective
-- Module: Mathlib.RingTheory.Localization.Ideal
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
inst_4 : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
this : IsDomain S
⊢ LT.lt.{u_1} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
    (((orderIsoOfPrime M S :
            OrderIso.{u_2, u_1} { p : Ideal S // p.IsPrime }
              { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) :
          (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
        (Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime) ⊥ ⋯) :
      { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
    (((orderIsoOfPrime M S :
            OrderIso.{u_2, u_1} { p : Ideal S // p.IsPrime }
              { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) :
          (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
        (Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime) p hpp) :
      { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })

Tactic:
(orderIsoOfPrime M S).lt_iff_lt.mpr
      (show (⟨⊥, Ideal.isPrime_bot⟩ : { p : Ideal S // p.IsPrime }) < ⟨p, hpp⟩ from hp0.bot_lt)

Premises used: Iff.mpr, OrderIso.lt_iff_lt, IsLocalization.orderIsoOfPrime, Ne.bot_lt
-- Module: Mathlib.RingTheory.Localization.Ideal
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
inst_4 : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
this : IsDomain S
⊢ LT.lt (α := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) ⊥) (Ideal.under R p)

Tactic:
convert!
    (orderIsoOfPrime M S).lt_iff_lt.mpr
      (show (⟨⊥, Ideal.isPrime_bot⟩ : { p : Ideal S // p.IsPrime }) < ⟨p, hpp⟩ from hp0.bot_lt)

Premises used: Iff.mpr, OrderIso.lt_iff_lt, IsLocalization.orderIsoOfPrime, Ne.bot_lt
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
⊢ LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰

Tactic:
have e : Algebra.algebraMapSubmonoid S M ≤ S⁰ :=
    Submonoid.map_le_of_le_comap _ <| hM.trans
      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
        (FaithfulSMul.algebraMap_injective _ _))
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
⊢ IsDomain Sₚ

Tactic:
have : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors _ e
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this : IsDomain Sₚ
h :
  Eq (α := R →+* Sₚ) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯) (algebraMap R Rₚ))
⊢ Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)

Tactic:
apply IsLocalization.ringHom_ext M

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this : IsDomain Sₚ
⊢ Eq (α := R →+* Sₚ) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯) (algebraMap R Rₚ))

Tactic:
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Premises used: IsLocalization.map_comp, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this : IsDomain Sₚ
⊢ Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)

Tactic:
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
    (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this_1 : IsDomain Sₚ
this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
rw : ∀ (x : Rₚ), Eq.{u_4 + 1} (α := Sₚ) ((algebraMap Rₚ Sₚ : (a : Rₚ) → Sₚ) x : Sₚ) (0 : Sₚ) → x = 0
⊢ Module.IsTorsionFree Rₚ Sₚ

Tactic:
rw [Module.isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
    RingHom.ker_eq_bot_iff_eq_zero]

Premises used: RingHom.ker_eq_bot_iff_eq_zero, Module.isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.RingTheory.Localization.Ideal
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this_1 : IsDomain Sₚ
this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
x : Rₚ
hx : Eq.{u_4 + 1} (α := Sₚ) ((algebraMap Rₚ Sₚ : (a : Rₚ) → Sₚ) x : Sₚ) (0 : Sₚ)
obtain :
  ∀ (x : R) (s : ↥M) (hx : Eq.{u_4 + 1} (α := Sₚ) ((algebraMap Rₚ Sₚ : (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