awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal R
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
a : R
b : ↥I
s : ↥M
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑s : R) * a) : S)
    ((algebraMap R S : (a : R) → S) (↑b : R) : S)
c : ↥M
hc : (↑c : R) * ((↑s : R) * a) = (↑c : R) * (↑b : R)
this : a * (↑(c * s) : R) ∈ I
⊢ a ∈ I

Tactic:
((Ideal.isPrimary_iff.mp hI).2 this).resolve_right (Set.disjoint_left.mp key (c * s).2)

Premises used: HMul.hMul, Set.Mem, Set.disjoint_left, And.right, Iff.mp, Ideal.isPrimary_iff, Or.resolve_right, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal R
hI : I.IsPrimary
hM : Disjoint (↑M : Set R) (↑I : Set R)
key : Disjoint (↑M : Set R) (↑I.radical : Set R)
a : R
b : ↥I
s : ↥M
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑s : R) * a) : S)
    ((algebraMap R S : (a : R) → S) (↑b : R) : S)
c : ↥M
hc : (↑c : R) * ((↑s : R) * a) = (↑c : R) * (↑b : R)
this : a * (↑(c * s) : R) ∈ I
⊢ a ∈ I

Tactic:
exact ((Ideal.isPrimary_iff.mp hI).2 this).resolve_right (Set.disjoint_left.mp key (c * s).2)

Premises used: HMul.hMul, Set.disjoint_left, And.right, Iff.mp, Ideal.isPrimary_iff, Or.resolve_right, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal R
hI : I.IsPrime
hM : Disjoint (↑M : Set R) (↑I : Set R)
⊢ Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I

Tactic:
under_map_of_isPrimary_disjoint M S hI.isPrimary hM

Premises used: Ideal.IsPrime.isPrimary, IsLocalization.under_map_of_isPrimary_disjoint
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J₁ J₂ : Ideal S
mp :
  LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R) →
    J₁ ≤ J₂
mpr :
  J₁ ≤ J₂ →
    LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R)
⊢ LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R) ↔
    J₁ ≤ J₂

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J₁ J₂ : Ideal S
⊢ LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R) →
    J₁ ≤ J₂

Tactic:
fun hJ => (map_under M S) J₁ ▸ (map_under M S) J₂ ▸ Ideal.map_mono hJ

Premises used: Eq.rec, IsLocalization.map_under, Ideal.map_mono
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J₁ J₂ : Ideal S
⊢ LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R) →
    J₁ ≤ J₂

Tactic:
exact fun hJ => (map_under M S) J₁ ▸ (map_under M S) J₂ ▸ Ideal.map_mono hJ
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ →
    LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R)

Tactic:
fun hJ => Ideal.comap_mono hJ

Premises used: Set.Mem, Ideal.comap_mono
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ →
    LE.le.{u_1} (α := Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₁ :
        Ideal R)
      ((({ toFun := fun (J : Ideal S) ↦ Ideal.under R J, inj' := ⋯ } :
              Function.Embedding.{u_2 + 1, u_1 + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          J₂ :
        Ideal R)

Tactic:
exact fun hJ => Ideal.comap_mono hJ

Premises used: Ideal.comap_mono
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I J : Ideal S
⊢ LE.le (α := Ideal R) (Ideal.under R I) (Ideal.under R J) ↔ I ≤ J

Tactic:
(IsLocalization.orderEmbedding M S).le_iff_le

Premises used: Set.Mem, IsLocalization.orderEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I J : Ideal S
⊢ LE.le (α := Ideal R) (Ideal.under R I) (Ideal.under R J) ↔ I ≤ J

Tactic:
exact (IsLocalization.orderEmbedding M S).le_iff_le

Premises used: IsLocalization.orderEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
mp : J.IsPrime → Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
mpr : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R) → J.IsPrime
⊢ J.IsPrime ↔ Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
⊢ J.IsPrime → Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)

Tactic:
fun h =>
      ⟨⟨?_, ?_⟩,
        Set.disjoint_left.mpr fun m hm1 hm2 =>
          h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩

Premises used: Iff.mpr, Set.disjoint_left, Ideal.eq_top_of_isUnit_mem, Subtype.mk, And.intro, Ideal.IsPrime.mk, IsLocalization.map_units, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
mp : ∀ (h : J.IsPrime), Ne (α := Ideal R) (Ideal.under R J) ⊤
mp₁ :
  ∀ (h : J.IsPrime) {x y : R},
    Membership.mem (γ := Ideal R) (Ideal.under R J) (x * y) →
      Membership.mem (γ := Ideal R) (Ideal.under R J) x ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) y
⊢ J.IsPrime → Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)

Tactic:
refine fun h =>
      ⟨⟨?_, ?_⟩,
        Set.disjoint_left.mpr fun m hm1 hm2 =>
          h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : J.IsPrime
⊢ Ne (α := Ideal R) (Ideal.under R J) ⊤

Tactic:
fun hJ => h.ne_top ?_

Premises used: Ideal.IsPrime.ne_top, Not
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : J.IsPrime
mp : ∀ (hJ : Eq (α := Ideal R) (Ideal.under R J) ⊤), J = ⊤
⊢ Ne (α := Ideal R) (Ideal.under R J) ⊤

Tactic:
refine fun hJ => h.ne_top ?_

Premises used: Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : J.IsPrime
hJ : Eq (α := Ideal R) (Ideal.under R J) ⊤
mp :
  LE.le.{u_1} (α := Ideal R)
    (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) ⊤ : Ideal R)
    (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) J : Ideal R)
⊢ J = ⊤

Tactic:
rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]

Premises used: eq_top_iff, IsLocalization.orderEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : J.IsPrime
hJ : Eq (α := Ideal R) (Ideal.under R J) ⊤
⊢ LE.le.{u_1} (α := Ideal R)
    (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) ⊤ : Ideal R)
    (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) J : Ideal R)

Tactic:
le_of_eq hJ.symm

Premises used: le_of_eq, Eq.symm
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : J.IsPrime
hJ : Eq (α := Ideal R) (Ideal.under R J) ⊤
⊢ LE.le.{u_1} (α := Ideal R)
    (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) ⊤ : Ideal R)
    (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) J : Ideal R)

Tactic:
exact le_of_eq hJ.symm

Premises used: le_of_eq, Eq.symm
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : J.IsPrime
x y : R
hxy : Membership.mem (γ := Ideal R) (Ideal.under R J) (x * y)
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ∈ J

Tactic:
rw [Ideal.mem_comap, map_mul] at hxy

Premises used: map_mul, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : J.IsPrime
x y : R
hxy : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ∈ J
⊢ Membership.mem (γ := Ideal R) (Ideal.under R J) x ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) y

Tactic:
h.mem_or_mem hxy

Premises used: Set.Mem, setOf, Ideal.IsPrime.mem_or_mem, Set.preimage
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : J.IsPrime
x y : R
hxy : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ∈ J
⊢ Membership.mem (γ := Ideal R) (Ideal.under R J) x ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) y

Tactic:
exact h.mem_or_mem hxy

Premises used: Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
⊢ Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R) → J.IsPrime

Tactic:
fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 ?_), ?_⟩

Premises used: Iff.mpr, eq_top_iff, And.left, Ideal.IsPrime.mk, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
mpr :
  ∀ (h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)) (hJ : J = ⊤),
    LE.le (α := Ideal R) ⊤ (Ideal.under R J)
mpr₁ :
  ∀ (h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)) {x y : S},
    x * y ∈ J → x ∈ J ∨ y ∈ J
⊢ Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R) → J.IsPrime

Tactic:
refine fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 ?_), ?_⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
hJ : J = ⊤
mpr : ∀ (hJ : ⊤ ≤ J), LE.le (α := Ideal R) ⊤ (Ideal.under R J)
mpr₁ mpr₂ mpr₃ mpr₄ :
  ∀
    (hJ :
      LE.le.{u_1} (α := Ideal R)
        (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) ⊤ : Ideal R)
        (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) J : Ideal R)),
    LE.le (α := Ideal R) ⊤ (Ideal.under R J)
⊢ LE.le (α := Ideal R) ⊤ (Ideal.under R J)

Tactic:
rwa [eq_top_iff, ← (orderEmbedding M S).le_iff_le] at hJ

Premises used: eq_top_iff, IsLocalization.orderEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
mpr : ∀ (a : R) (s : ↥M) (ha : mk' S a s = x), x ∈ J ∨ y ∈ J
⊢ x ∈ J ∨ y ∈ J

Tactic:
obtain ⟨a, s, ha⟩ := exists_mk'_eq M x

Premises used: IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
mpr : ∀ (b : R) (t : ↥M) (hb : mk' S b t = y), x ∈ J ∨ y ∈ J
⊢ x ∈ J ∨ y ∈ J

Tactic:
obtain ⟨b, t, hb⟩ := exists_mk'_eq M y

Premises used: IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
rwa : mk' S a s * mk' S b t ∈ J
rwa₁ : x * mk' S b t ∈ J
rwa₂ rwa₃ rwa₄ rwa₅ : x * y ∈ J
⊢ mk' S (a * b) (s * t) ∈ J

Tactic:
rwa [mk'_mul, ha, hb]

Premises used: IsLocalization.mk'_mul
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
⊢ mk' S (a * b) (s * t) ∈ J

Tactic:
have : mk' S (a * b) (s * t) ∈ J := by rwa [mk'_mul, ha, hb]
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : mk' S (a * b) (s * t) ∈ J
⊢ Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)

Tactic:
rw [mk'_mem_iff, ← Ideal.mem_comap] at this

Premises used: IsLocalization.mk'_mem_iff, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
⊢ Membership.mem (γ := Ideal R) (Ideal.under R J) a ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) b

Tactic:
have this₂ := (h.1).mul_mem_iff_mem_or_mem.1 this
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
this₂ : Membership.mem (γ := Ideal R) (Ideal.under R J) a ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) b
⊢ Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨
    Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) b : S)

Tactic:
rw [Ideal.mem_comap, Ideal.mem_comap] at this₂

Premises used: Ideal.mem_comap
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
this₂ :
  Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨
    Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) b : S)
mpr : mk' S a s ∈ J ∨ y ∈ J
mpr₁ : mk' S a s ∈ J ∨ mk' S b t ∈ J
mpr₂ : Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨ mk' S b t ∈ J
mpr₃ mpr₄ mpr₅ mpr₆ :
  Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨
    Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) b : S)
⊢ x ∈ J ∨ y ∈ J

Tactic:
rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]

Premises used: IsLocalization.mk'_mem_iff
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal R
hp : I.IsPrime
hd : Disjoint (↑M : Set R) (↑I : Set R)
rw : I.IsPrime ∧ Disjoint (↑M : Set R) (↑I : Set R)
⊢ Ideal.IsPrime.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
rw [isPrime_iff_isPrime_disjoint M S, under_map_of_isPrime_disjoint M S hp hd]

Premises used: IsLocalization.isPrime_iff_isPrime_disjoint, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal R
hp : I.IsPrime
hd : Disjoint (↑M : Set R) (↑I : Set R)
⊢ I.IsPrime ∧ Disjoint (↑M : Set R) (↑I : Set R)

Tactic:
⟨hp, hd⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.Localization.Ideal
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
I : Ideal R
hp : I.IsPrime
hd : Disjoint (↑M : Set R) (↑I : Set R)
⊢ I.IsPrime ∧ Disjoint (↑M : Set R) (↑I : Set R)

Tactic:
exact ⟨hp, hd⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
rw : J = ⊤ ↔ ∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)
⊢ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R) ↔ J ≠ ⊤

Tactic:
rw [← iff_not_comm, Set.not_disjoint_iff]

Premises used: iff_not_comm, Set.not_disjoint_iff
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
mp : J = ⊤ → ∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)
mpr : (∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)) → J = ⊤
⊢ J = ⊤ ↔ ∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Ideal
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 ∈ (↑M : Set R), x ∈ (↑(Ideal.under.{u_1, u_2} R (B := S) ⊤) : Set R)

Tactic:
⟨1, M.one_mem, ⟨⟩⟩

Premises used: Submonoid.one_mem, And.intro, Exists.intro, OfNat.ofNat, True.intro
-- Module: Mathlib.RingTheory.Localization.Ideal
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 ∈ (↑M : Set R), x ∈ (↑(Ideal.under.{u_1, u_2} R (B := S) ⊤) : Set R)

Tactic:
exact ⟨1, M.one_mem, ⟨⟩⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
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
J : Ideal S
x : R
hxM : x ∈ (↑M : Set R)
hxJ : x ∈ (↑(Ideal.under R J) : Set R)
⊢ J = ⊤

Tactic:
J.eq_top_of_isUnit_mem hxJ (IsLocalization.map_units S ⟨x, hxM⟩)

Premises used: Ideal.eq_top_of_isUnit_mem, Subtype.mk, IsLocalization.map_units