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
x : R
s : ↥M
⊢ (∃ (x_1 : ↥I × ↥M) (c : ↥M), (↑(c * x_1.2) : R) * x = (↑c : R) * (↑x_1.1 : R)) ↔ ∃ s ∈ M, s * x ∈ I

Tactic:
exact ⟨fun ⟨⟨y, t⟩, c, h⟩ ↦ ⟨_, (c * t).2, h ▸ I.mul_mem_left c.1 y.2⟩, fun ⟨s, hs, h⟩ ↦
    ⟨⟨⟨_, h⟩, ⟨s, hs⟩⟩, 1, by simp⟩⟩
-- 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
x : R
rw :
  Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (mk' (M := M) S x 1) ↔ ∃ m ∈ M, m * x ∈ I
rw₁ rw₂ : (∃ s ∈ M, s * x ∈ I) ↔ ∃ m ∈ M, m * x ∈ I
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
      ((algebraMap R S : (a : R) → S) x : S) ↔
    ∃ m ∈ M, m * x ∈ I

Tactic:
rw [← IsLocalization.mk'_one (M := M), mk'_mem_map_algebraMap_iff]

Premises used: IsLocalization.mk'_mem_map_algebraMap_iff, IsLocalization.mk'_one
-- 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
simp : ¬Disjoint (↑M : Set R) (↑I : Set R) ↔ ∃ m ∈ M, m * 1 ∈ I
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤ ↔ Disjoint (↑M : Set R) (↑I : Set R)

Tactic:
simp only [ne_eq, Ideal.eq_top_iff_one, ← map_one (algebraMap R S), not_iff_comm,
    IsLocalization.algebraMap_mem_map_algebraMap_iff M]

Premises used: Algebra.algebraMap, IsLocalization.algebraMap_mem_map_algebraMap_iff, ne_eq, Ideal.eq_top_iff_one, map_one, not_iff_comm
-- 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
⊢ ¬Disjoint (↑M : Set R) (↑I : Set R) ↔ ∃ m ∈ M, m * 1 ∈ I

Tactic:
simp [Set.disjoint_left]

Premises used: Set.disjoint_left
-- 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 R
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ⊓ J))
    (Ideal.map (F := R →+* S) (algebraMap R S) I ⊓ Ideal.map (F := R →+* S) (algebraMap R S) J)

Tactic:
le_antisymm (Ideal.map_inf_le (algebraMap R S)) fun x hx ↦ ?_

Premises used: Algebra.algebraMap, le_antisymm, Ideal.map_inf_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 R
refine :
  ∀ (x : S)
    (hx :
      Membership.mem (γ := Submodule S S)
        (Ideal.map (F := R →+* S) (algebraMap R S) I ⊓ Ideal.map (F := R →+* S) (algebraMap R S) J) x),
    Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ⊓ J)) x
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ⊓ J))
    (Ideal.map (F := R →+* S) (algebraMap R S) I ⊓ Ideal.map (F := R →+* S) (algebraMap R S) J)

Tactic:
refine le_antisymm (Ideal.map_inf_le (algebraMap R S)) fun x hx ↦ ?_

Premises used: Algebra.algebraMap, le_antisymm, Ideal.map_inf_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 R
x : S
hx :
  Membership.mem (γ := Submodule S S)
    (Ideal.map (F := R →+* S) (algebraMap R S) I ⊓ Ideal.map (F := R →+* S) (algebraMap R S) J) x
simp :
  ∀
    (hx :
      (∃ (a : ↥I) (b : ↥M),
          HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) =
            (algebraMap R S : (a : R) → S) (↑a : R)) ∧
        ∃ (a : ↥J) (b : ↥M),
          HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)),
    ∃ (a : ↥(I ⊓ J)) (b : ↥M),
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (I ⊓ J)) x

Tactic:
simp only [Ideal.mem_inf, IsLocalization.mem_map_algebraMap_iff M, Prod.exists] at hx ⊢

Premises used: Ideal.mem_inf, IsLocalization.mem_map_algebraMap_iff, Prod.exists
-- 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 R
x : S
hx :
  (∃ (a : ↥I) (b : ↥M),
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)) ∧
    ∃ (a : ↥J) (b : ↥M),
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
obtain :
  ∀ (i : R) (hi : i ∈ I) (mi : ↥M)
    (hi' :
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mi : R) : S) =
        (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R))
    (j : R) (hj : j ∈ J) (mj : ↥M)
    (hj' :
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mj : R) : S) =
        (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ J) j hj) : R)),
    ∃ (a : ↥(I ⊓ J)) (b : ↥M),
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)

Tactic:
obtain ⟨⟨⟨i, hi⟩, mi, hi'⟩, ⟨j, hj⟩, mj, hj'⟩ := hx
-- 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 R
x : S
i : R
hi : i ∈ I
mi : ↥M
hi' :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mi : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R)
j : R
hj : j ∈ J
mj : ↥M
hj' :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mj : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ J) j hj) : R)
⊢ x = mk' S i mi

Tactic:
simp only [← IsLocalization.eq_mk'_iff_mul_eq] at hi' hj'

Premises used: IsLocalization.eq_mk'_iff_mul_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
I J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
hi' :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mi : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I) i hi) : R)
j : R
hj : j ∈ J
mj : ↥M
hj' :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑mj : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ J) j hj) : R)
hi'₁ : x = mk' S i mi
⊢ x = mk' S j mj

Tactic:
simp only [← IsLocalization.eq_mk'_iff_mul_eq] at hi' hj'

Premises used: IsLocalization.eq_mk'_iff_mul_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
I J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
obtain :
  ∀ (m : ↥M) (hm : (↑m : R) * ((↑mj : R) * i) = (↑m : R) * ((↑mi : R) * j)),
    ∃ (a : ↥(I ⊓ J)) (b : ↥M),
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)

Tactic:
obtain ⟨m, hm⟩ := IsLocalization.eq.mp (hi'.symm.trans hj')

Premises used: Iff.mp, Eq.symm, IsLocalization.eq, Eq.trans
-- 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 R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : (↑m : R) * ((↑mj : R) * i) = (↑m : R) * ((↑mi : R) * j)
⊢ i * ((↑m : R) * (↑mj : R)) = j * ((↑m : R) * (↑mi : R))

Tactic:
rw [← mul_assoc, ← mul_assoc, mul_comm, ← mul_comm (j : R)] at hm

Premises used: mul_assoc, mul_comm
-- 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 R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * ((↑m : R) * (↑mj : R)) = j * ((↑m : R) * (↑mi : R))
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)

Tactic:
⟨⟨i * (m * mj : M), I.mul_mem_right _ hi, hm ▸ J.mul_mem_right _ hj⟩, mi * (m * mj), ?_⟩

Premises used: HMul.hMul, Eq.rec, Subtype.mk, Ideal.mul_mem_right, And.intro, Exists.intro, Eq.symm, Subtype.val
-- 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 R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * ((↑m : R) * (↑mj : R)) = j * ((↑m : R) * (↑mi : R))
refine :
  HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(mi * (m * mj)) : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I ⊓ J) (i * (↑(m * mj) : R)) ⋯) : R)
⊢ ∃ (a : ↥(I ⊓ J)) (b : ↥M),
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑b : R) : S) = (algebraMap R S : (a : R) → S) (↑a : R)

Tactic:
refine ⟨⟨i * (m * mj : M), I.mul_mem_right _ hi, hm ▸ J.mul_mem_right _ hj⟩, mi * (m * mj), ?_⟩
-- 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 R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * ((↑m : R) * (↑mj : R)) = j * ((↑m : R) * (↑mi : R))
rwa : x = mk' S (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I ⊓ J) (i * (↑(m * mj) : R)) ⋯) : R) (mi * (m * mj))
rwa₁ : x = mk' S (i * (↑(m * mj) : R)) (mi * (m * mj))
rwa₂ rwa₃ rwa₄ rwa₅ : x = mk' S i mi
⊢ HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(mi * (m * mj)) : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ I ⊓ J) (i * (↑(m * mj) : R)) ⋯) : R)

Tactic:
rwa [← IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, IsLocalization.mk'_cancel]

Premises used: Subtype.coe_mk, IsLocalization.mk'_cancel, IsLocalization.eq_mk'_iff_mul_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
I : Ideal R
⊢ Eq.{u_2 + 1} (α := Ideal S)
    (((mapFrameHom M S : FrameHom.{u_1, u_2} (Ideal R) (Ideal S)) : (a : Ideal R) → Ideal S) I : Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S) I : Ideal S)

Tactic:
rfl

Premises used: Ideal.map, Submodule.span, rfl
-- 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 : S
hJ : x ∈ J
obtain :
  ∀ (r : R) (s : ↥M) (hx : mk' S r s = x),
    Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) x
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) x

Tactic:
obtain ⟨r, s, hx⟩ := 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
x : S
hJ : x ∈ J
r : R
s : ↥M
hx : mk' S r s = x
rw :
  ∀ (hJ : mk' S r s ∈ J) (hx : mk' S r s = x),
    Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) (mk' S r s)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) x

Tactic:
rw [← hx] at 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 : Ideal S
x : S
r : R
s : ↥M
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) (mk' S r s)

Tactic:
Ideal.mul_mem_right _ _
        (Ideal.mem_map_of_mem _
          (show (algebraMap R S) r ∈ J from
            mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, Set.Mem, Submonoid.LocalizationMap.mk', Eq.rec, IsLocalization.mk', Ideal.mul_mem_right, Subtype.val, DFunLike.coe, IsLocalization.mk'_spec
-- 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 : S
r : R
s : ↥M
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.under R J)) (mk' S r s)

Tactic:
exact
      Ideal.mul_mem_right _ _
        (Ideal.mem_map_of_mem _
          (show (algebraMap R S) r ∈ J from
            mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, Eq.rec, Ideal.mul_mem_right, Subtype.val, DFunLike.coe, IsLocalization.mk'_spec
-- 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)
contrapose : ∀ (hM : ¬Disjoint (↑M : Set R) (↑I.radical : Set R)), ¬Disjoint (↑M : Set R) (↑I : Set R)
⊢ Disjoint (↑M : Set R) (↑I.radical : Set R)

Tactic:
contrapose hM
-- 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.radical : Set R)
rw : ∀ (hM : ∃ x ∈ (↑M : Set R), x ∈ (↑I.radical : Set R)), ∃ x ∈ (↑M : Set R), x ∈ (↑I : Set R)
⊢ ¬Disjoint (↑M : Set R) (↑I : Set R)

Tactic:
rw [Set.not_disjoint_iff] at hM ⊢

Premises used: 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
I : Ideal R
hI : I.IsPrimary
hM : ∃ x ∈ (↑M : Set R), x ∈ (↑I.radical : Set R)
obtain : ∀ (a : R) (ha : a ∈ (↑M : Set R)) (k : ℕ) (hk : a ^ k ∈ I), ∃ x ∈ (↑M : Set R), x ∈ (↑I : Set R)
⊢ ∃ x ∈ (↑M : Set R), x ∈ (↑I : Set R)

Tactic:
obtain ⟨a, ha, k, hk⟩ := hM
-- 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
a : R
ha : a ∈ (↑M : Set R)
k : ℕ
hk : a ^ k ∈ I
⊢ ∃ x ∈ (↑M : Set R), x ∈ (↑I : Set R)

Tactic:
⟨a ^ k, pow_mem ha k, hk⟩

Premises used: HPow.hPow, And.intro, Exists.intro, pow_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
I : Ideal R
hI : I.IsPrimary
a : R
ha : a ∈ (↑M : Set R)
k : ℕ
hk : a ^ k ∈ I
⊢ ∃ x ∈ (↑M : Set R), x ∈ (↑I : Set R)

Tactic:
exact ⟨a ^ k, pow_mem ha k, hk⟩
-- 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)
⊢ Disjoint (↑M : Set R) (↑I.radical : Set R)

Tactic:
have key : Disjoint (M : Set R) I.radical := by
    contrapose hM
    rw [Set.not_disjoint_iff] at hM ⊢
    obtain ⟨a, ha, k, hk⟩ := hM
    exact ⟨a ^ k, pow_mem ha k, hk⟩
-- 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)
⊢ Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I

Tactic:
le_antisymm (fun a ha ↦ ?_) Ideal.le_comap_map

Premises used: le_antisymm, Ideal.le_comap_map
-- 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)
refine :
  ∀ (a : R)
    (ha :
      Membership.mem (γ := Submodule R R)
        (Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) a),
    a ∈ I
⊢ Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I

Tactic:
refine le_antisymm (fun a ha ↦ ?_) Ideal.le_comap_map

Premises used: le_antisymm, Ideal.le_comap_map
-- 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
ha :
  Membership.mem (γ := Submodule R R) (Ideal.under.{u_1, u_2} R (B := S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    a
⊢ ∃ (x : ↥I × ↥M),
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
      (algebraMap R S : (a : R) → S) (↑x.1 : R)

Tactic:
rw [Ideal.mem_comap, IsLocalization.mem_map_algebraMap_iff M S] at ha

Premises used: IsLocalization.mem_map_algebraMap_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
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
ha :
  ∃ (x : ↥I × ↥M),
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
      (algebraMap R S : (a : R) → S) (↑x.1 : R)
obtain :
  ∀ (b : ↥I) (s : ↥M)
    (h :
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
          ((algebraMap R S : (a : R) → S) (↑(b, s).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (↑(b, s).1 : R)),
    a ∈ I
⊢ a ∈ I

Tactic:
obtain ⟨⟨b, s⟩, h⟩ := ha
-- 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 :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
      ((algebraMap R S : (a : R) → S) (↑(b, s).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(b, s).1 : R)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑s : R) * a) : S)
    ((algebraMap R S : (a : R) → S) (↑b : R) : S)

Tactic:
simpa only [← map_mul, mul_comm] using h

Premises used: map_mul, mul_comm
-- 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 :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S)
      ((algebraMap R S : (a : R) → S) (↑(b, s).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑(b, s).1 : R)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((↑s : R) * a) : S)
    ((algebraMap R S : (a : R) → S) (↑b : R) : S)

Tactic:
replace h : algebraMap R S (s * a) = algebraMap R S b := by
    simpa only [← map_mul, mul_comm] using h
-- 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)
obtain : ∀ (c : ↥M) (hc : (↑c : R) * ((↑s : R) * a) = (↑c : R) * (↑b : R)), a ∈ I
⊢ a ∈ I

Tactic:
obtain ⟨c, hc⟩ := (IsLocalization.eq_iff_exists M S).1 h

Premises used: Iff.mp, IsLocalization.eq_iff_exists
-- 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)
rw : (↑c : R) * (↑b : R) ∈ I
⊢ a * (↑(c * s) : R) ∈ I

Tactic:
rw [mul_comm, Submonoid.coe_mul, mul_assoc, hc]

Premises used: mul_assoc, mul_comm, Submonoid.coe_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
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)
⊢ (↑c : R) * (↑b : R) ∈ I

Tactic:
I.mul_mem_left c b.2

Premises used: Ideal.mul_mem_left, Subtype.val, 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)
⊢ (↑c : R) * (↑b : R) ∈ I

Tactic:
exact I.mul_mem_left c b.2

Premises used: Ideal.mul_mem_left, Subtype.val, 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)
⊢ a * (↑(c * s) : R) ∈ I

Tactic:
have : a * (c * s : M) ∈ I := by
    rw [mul_comm, Submonoid.coe_mul, mul_assoc, hc]
    exact I.mul_mem_left c b.2