awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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.{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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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) (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)
have 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)
Tactic: simp only [mul_eq_mul_left_iff, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
have 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)
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 ?_))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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
⊢ 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)
have 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)
Tactic: rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
⊢ 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)
have neg₂ : Eq (α := S ⧸ I) 1 ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) 1)
Tactic: rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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)
⊢ 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)
have neg₃ : Eq.{u_2 + 1} (α := S ⧸ I) 1 1
Tactic: rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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 ≠ ⊥
⊢ LT.lt (α := Ideal R) ⊥ (Ideal.under R p)
have this : IsDomain S
Tactic: haveI : IsDomain S := isDomain_of_le_nonZeroDivisors _ hM
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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.under R p)
have rw : LT.lt (α := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) ⊥) (Ideal.under R p)
Tactic: rw [← Ideal.comap_bot_of_injective (algebraMap R S) (IsLocalization.injective _ hM)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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
⊢ Module.IsTorsionFree Rₚ Sₚ
have e : 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 _ _))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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⁰
⊢ Module.IsTorsionFree Rₚ Sₚ
have this : IsDomain Sₚ
Tactic: have : IsDomain Sₚ := IsLocalization.isDomain_of_le_nonZeroDivisors _ e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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) ⋯)
have 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) sorry) (algebraMap R Rₚ))
Tactic: apply IsLocalization.ringHom_ext M
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
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ₚ
⊢ Module.IsTorsionFree Rₚ Sₚ
have this₁ : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) sorry)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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) ⋯)
⊢ Module.IsTorsionFree Rₚ Sₚ
have rw : ∀ (x : Rₚ), Eq.{u_4 + 1} (α := Sₚ) ((algebraMap Rₚ Sₚ : (a : Rₚ) → Sₚ) x : Sₚ) (0 : Sₚ) → x = 0
Tactic: rw [Module.isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
    RingHom.ker_eq_bot_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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ₚ)
⊢ x = 0
have 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
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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
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
have simp : ∀
  (hx :
    ∃ (a : S),
      Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) a ∧
        HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) x : S) = 0),
  ∃ a ∈ M, a * x = 0
Tactic: simp only [IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
    Subtype.exists, exists_prop, this] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
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
s : ↥M
hx :
  ∃ (a : S),
    Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) a ∧
      HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) x : S) = 0
⊢ ∃ a ∈ M, a * x = 0
have obtain : ∀ (a : R) (ha : a ∈ (↑M : Set R))
  (H : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) x : S) = 0),
  ∃ a ∈ M, a * x = 0
Tactic: obtain ⟨_, ⟨a, ha, rfl⟩, H⟩ := hx
Cleared hypotheses: hx