awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ 1 ∈ J

Tactic:
specialize oJ J x IJ hx xJ
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
rcases :
  ∀ (a b : α) (h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b) (oe : 1 = a • x + b), y ∈ I
⊢ y ∈ I

Tactic:
rcases Submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩

Premises used: Iff.mp, Submodule.mem_span_insert
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
⊢ y * 1 = y * (a • x + b)

Tactic:
congr_arg (fun g : α => y * g) oe

Premises used: HMul.hMul, congr_arg
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
⊢ y * 1 = y * (a • x + b)

Tactic:
obtain F : y * 1 = y * (a • x + b) := congr_arg (fun g : α => y * g) oe

Premises used: HMul.hMul, congr_arg, HAdd.hAdd, HSMul.hSMul
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
rw : a * (x * y) + y * b ∈ I
⊢ y ∈ I

Tactic:
rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, mul_comm, mul_add, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ a * (x * y) + y * b ∈ I

Tactic:
Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y ?_)

Premises used: Set.Mem, Ideal.mul_mem_left, Submodule.smul_mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
refine : b ∈ I
⊢ a * (x * y) + y * b ∈ I

Tactic:
refine Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y ?_)

Premises used: Ideal.mul_mem_left, Submodule.smul_mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : b ∈ I) (oe : 1 = a • x + b) (F : y * 1 = y * (a • x + b)), b ∈ I
⊢ b ∈ I

Tactic:
rwa [Submodule.span_eq] at h

Premises used: Submodule.span_eq
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
β : Type v
F : Type w
a b : α
inst : CommSemiring α
I_1 I : Ideal α
⊢ ∀ [_H : I.IsMaximal], I.IsPrime

Tactic:
@IsMaximal.isPrime _ _ _

Premises used: Ideal.IsMaximal.isPrime
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
have : ∀ (M : Ideal α) (hM : M.IsMaximal) (le : I ≤ M), ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)
⊢ ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)

Tactic:
have ⟨M, hM, le⟩ := exists_le_maximal I hI
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
⊢ M ≠ ⊤

Tactic:
have := hM.1.1
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : M ≠ ⊤
⊢ ∃ a ∈ s, a ∉ (↑M : Set α)

Tactic:
rw [Ne, eq_top_iff, ← hs, span_le, Set.not_subset] at this

Premises used: Ideal.span_le, eq_top_iff, Ne, Set.not_subset
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ (↑M : Set α)
have : ∀ (a : α) (has : a ∈ s) (haM : a ∉ (↑M : Set α)), ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)
⊢ ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)

Tactic:
have ⟨a, has, haM⟩ := this
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ (↑M : Set α)
a : α
has : a ∈ s
haM : a ∉ (↑M : Set α)
⊢ ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)

Tactic:
⟨a, has, Set.disjoint_left.mpr fun x hx ⟨n, hn⟩ ↦
    haM (hM.isPrime.mem_of_pow_mem _ (le <| hn ▸ hx))⟩

Premises used: Iff.mpr, False, Set.disjoint_left, Ideal.IsPrime.mem_of_pow_mem, Ideal.IsMaximal.isPrime, _private.0.Ideal.exists_disjoint_powers_of_span_eq_top.match_3, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ (↑M : Set α)
a : α
has : a ∈ s
haM : a ∉ (↑M : Set α)
⊢ ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)

Tactic:
exact ⟨a, has, Set.disjoint_left.mpr fun x hx ⟨n, hn⟩ ↦
    haM (hM.isPrime.mem_of_pow_mem _ (le <| hn ▸ hx))⟩
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
rw : LE.le (α := Ideal α) (span {x}) (span {y}) ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
rw₁ : y ∣ x ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
rw₂ : y ∣ x ∧ ¬x ∣ y ↔ DvdNotUnit y x
rw₃ rw₄ : DvdNotUnit y x ↔ DvdNotUnit y x
⊢ LT.lt (α := Ideal α) (span {x}) (span {y}) ↔ DvdNotUnit y x

Tactic:
rw [lt_iff_le_not_ge, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
    dvd_and_not_dvd_iff]

Premises used: lt_iff_le_not_ge, Ideal.span_singleton_le_span_singleton, dvd_and_not_dvd_iff
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
S : Submonoid α
disjoint : Disjoint (↑⊤ : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), ⊤ < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
⊢ 1 ∈ (↑S : Set α)

Tactic:
have : 1 ∈ (S : Set α) := S.one_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
S : Submonoid α
disjoint : Disjoint (↑⊤ : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), ⊤ < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
this : 1 ∈ (↑S : Set α)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
by_contra! : ∀ (rid : x ∉ I ∧ y ∉ I), False
⊢ x ∈ I ∨ y ∈ I

Tactic:
by_contra! rid
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
⊢ ¬Disjoint (↑(I ⊔ span {x}) : Set α) (↑S : Set α)

Tactic:
have hx := maximally_disjoint (I ⊔ span {x}) (Submodule.lt_sup_iff_notMem.mpr rid.1)
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ¬Disjoint (↑(I ⊔ span {x}) : Set α) (↑S : Set α)
⊢ ¬Disjoint (↑(I ⊔ span {y}) : Set α) (↑S : Set α)

Tactic:
have hy := maximally_disjoint (I ⊔ span {y}) (Submodule.lt_sup_iff_notMem.mpr rid.2)
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ¬Disjoint (↑(I ⊔ span {x}) : Set α) (↑S : Set α)
hy : ¬Disjoint (↑(I ⊔ span {y}) : Set α) (↑S : Set α)
⊢ ∃ (x_1 : α), (∃ y ∈ I, ∃ (z : α), x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S

Tactic:
simp only [Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup,
      mem_span_singleton] at hx hy

Premises used: Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ¬Disjoint (↑(I ⊔ span {x}) : Set α) (↑S : Set α)
hy : ¬Disjoint (↑(I ⊔ span {y}) : Set α) (↑S : Set α)
hx₁ : ∃ (x_1 : α), (∃ y ∈ I, ∃ (z : α), x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S
⊢ ∃ (x : α), (∃ y_1 ∈ I, ∃ (z : α), y ∣ z ∧ y_1 + z = x) ∧ x ∈ S

Tactic:
simp only [Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup,
      mem_span_singleton] at hx hy

Premises used: Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ∃ (x_1 : α), (∃ y ∈ I, ∃ (z : α), x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S
hy : ∃ (x : α), (∃ y_1 ∈ I, ∃ (z : α), y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
obtain : ∀ (s₁ : α) (hs₁ : s₁ ∈ S) (i₁ : α) (hi₁ : i₁ ∈ I) (r₁ : α) (hr₁ : i₁ + x * r₁ = s₁), False
⊢ False

Tactic:
obtain ⟨s₁, ⟨i₁, hi₁, ⟨_, ⟨r₁, rfl⟩, hr₁⟩⟩, hs₁⟩ := hx

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hy : ∃ (x : α), (∃ y_1 ∈ I, ∃ (z : α), y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
obtain : ∀ (s₂ : α) (hs₂ : s₂ ∈ S) (i₂ : α) (hi₂ : i₂ ∈ I) (r₂ : α) (hr₂ : i₂ + y * r₂ = s₂), False
⊢ False

Tactic:
obtain ⟨s₂, ⟨i₂, hi₂, ⟨_, ⟨r₂, rfl⟩, hr₂⟩⟩, hs₂⟩ := hy

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
⊢ False

Tactic:
disjoint.ne_of_mem
      (I.add_mem (I.mul_mem_left (i₁ + x * r₁) hi₂) <| I.add_mem (I.mul_mem_right (y * r₂) hi₁) <|
        I.mul_mem_right (r₁ * r₂) hxy)
      (S.mul_mem hs₁ hs₂) ?_

Premises used: HMul.hMul, Submonoid.mul_mem, Ideal.add_mem, HAdd.hAdd, Ideal.mul_mem_right, Ideal.mul_mem_left, Disjoint.ne_of_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
refine : (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = s₁ * s₂
⊢ False

Tactic:
refine disjoint.ne_of_mem
      (I.add_mem (I.mul_mem_left (i₁ + x * r₁) hi₂) <| I.add_mem (I.mul_mem_right (y * r₂) hi₁) <|
        I.mul_mem_right (r₁ * r₂) hxy)
      (S.mul_mem hs₁ hs₂) ?_

Premises used: HMul.hMul, Submonoid.mul_mem, Ideal.add_mem, HAdd.hAdd, Ideal.mul_mem_right, Ideal.mul_mem_left, Disjoint.ne_of_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
rw : (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = (i₁ + x * r₁) * (i₂ + y * r₂)
⊢ (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = s₁ * s₂

Tactic:
rw [← hr₁, ← hr₂]
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
⊢ (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = (i₁ + x * r₁) * (i₂ + y * r₂)

Tactic:
ring
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
refine_2 :
  ∀ (p : Ideal α) (hIp : I ≤ p)
    (hp :
      Maximal
        (fun (x : Ideal α) ↦ Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} x)
        p),
    ∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint (↑p : Set α) (↑S : Set α)
refine_1 :
  ∀ (c : Set (Ideal α)) (hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)})
    (hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c) (x : Ideal α) (hx : x ∈ c),
    ∃ (ub : Ideal α),
      Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
⊢ ∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint (↑p : Set α) (↑S : Set α)

Tactic:
have ⟨p, hIp, hp⟩ := zorn_le_nonempty₀ {p : Ideal α | Disjoint (p : Set α) S}
    (fun c hc hc' x hx ↦ ?_) I disjoint
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
p : Ideal α
hIp : I ≤ p
hp :
  Maximal (fun (x : Ideal α) ↦ Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} x)
    p
⊢ ∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint (↑p : Set α) (↑S : Set α)

Tactic:
⟨p, isPrime_of_maximally_disjoint _ _ hp.1 (fun _ ↦ hp.not_prop_of_gt), hIp, hp.1⟩

Premises used: Ideal.isPrime_of_maximally_disjoint, Maximal.not_prop_of_gt, And.left, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
p : Ideal α
hIp : I ≤ p
hp :
  Maximal (fun (x : Ideal α) ↦ Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} x)
    p
⊢ ∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint (↑p : Set α) (↑S : Set α)

Tactic:
exact ⟨p, isPrime_of_maximally_disjoint _ _ hp.1 (fun _ ↦ hp.not_prop_of_gt), hIp, hp.1⟩
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
refine_1 :
  IsEmpty.{u + 1} (↑c : Type u) →
    ∃ (ub : Ideal α),
      Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
refine_1₁ :
  Nonempty.{u + 1} (↑c : Type u) →
    ∃ (ub : Ideal α),
      Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
⊢ ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
cases isEmpty_or_nonempty c

Premises used: Set.Elem, isEmpty_or_nonempty
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h : IsEmpty.{u + 1} (↑c : Type u)
⊢ ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
⟨I, disjoint, fun J hJ ↦ isEmptyElim (⟨J, hJ⟩ : c)⟩

Premises used: isEmptyElim, Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h : IsEmpty.{u + 1} (↑c : Type u)
⊢ ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
exact ⟨I, disjoint, fun J hJ ↦ isEmptyElim (⟨J, hJ⟩ : c)⟩
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h : Nonempty.{u + 1} (↑c : Type u)
⊢ ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
⟨sSup c, Set.disjoint_left.mpr fun x hx ↦ ?_, fun _ ↦ le_sSup⟩

Premises used: Iff.mpr, Set.disjoint_left, And.intro, Exists.intro, le_sSup, SupSet.sSup
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h : Nonempty.{u + 1} (↑c : Type u)
refine_1 : ∀ (x : α) (hx : x ∈ (↑(sSup c) : Set α)), x ∉ (↑S : Set α)
⊢ ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub

Tactic:
refine ⟨sSup c, Set.disjoint_left.mpr fun x hx ↦ ?_, fun _ ↦ le_sSup⟩
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x_1 : Ideal α
hx_1 : x_1 ∈ c
h : Nonempty.{u + 1} (↑c : Type u)
x : α
hx : x ∈ (↑(sSup c) : Set α)
refine_1 : ∀ (p : { a : Ideal α // a ∈ c }) (hp : x ∈ (↑p : Ideal α)), x ∉ (↑S : Set α)
⊢ x ∉ (↑S : Set α)

Tactic:
have ⟨p, hp⟩ := (Submodule.mem_iSup_of_directed _ hc'.directed).mp (sSup_eq_iSup' c ▸ hx)
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x_1 : Ideal α
hx_1 : x_1 ∈ c
h : Nonempty.{u + 1} (↑c : Type u)
x : α
hx : x ∈ (↑(sSup c) : Set α)
p : { a : Ideal α // a ∈ c }
hp : x ∈ (↑p : Ideal α)
⊢ x ∉ (↑S : Set α)

Tactic:
Set.disjoint_left.mp (hc p.2) hp

Premises used: Set.disjoint_left, Iff.mp, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x_1 : Ideal α
hx_1 : x_1 ∈ c
h : Nonempty.{u + 1} (↑c : Type u)
x : α
hx : x ∈ (↑(sSup c) : Set α)
p : { a : Ideal α // a ∈ c }
hp : x ∈ (↑p : Ideal α)
⊢ x ∉ (↑S : Set α)

Tactic:
exact Set.disjoint_left.mp (hc p.2) hp

Premises used: Set.disjoint_left, Iff.mp, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
rw : ∀ ⦃a_1 : α⦄, Membership.mem (γ := Set α) {1, a} a_1 → a_1 ∉ (↑I : Set α)
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (↑(Submonoid.powers a) : Set α) → a_1 ∉ (↑I : Set α)

Tactic:
rw [ha.coe_powers]

Premises used: IsIdempotentElem.coe_powers
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ 1 ∉ (↑I : Set α)

Tactic:
I.ne_top_iff_one.mp (ne_of_mem_of_not_mem' Submodule.mem_top haI).symm

Premises used: Ideal.ne_top_iff_one, Set.Mem, Ne.symm, Iff.mp, ne_of_mem_of_not_mem', Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ a ∉ (↑I : Set α)

Tactic:
haI
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ 1 ∉ (↑I : Set α)

Tactic:
exacts [I.ne_top_iff_one.mp (ne_of_mem_of_not_mem' Submodule.mem_top haI).symm, haI]

Premises used: Ideal.ne_top_iff_one, Ne.symm, Iff.mp, ne_of_mem_of_not_mem', Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
P : Ideal α
hP : P ≠ ⊥
h : P.IsPrime
obtain :
  ∀ (p : α) (hP : Ne (α := Ideal α) (α ∙ p) ⊥) (h : IsPrime (α ∙ p)),
    ∃ (p_1 : α), Prime p_1 ∧ Eq (α := Ideal α) (α ∙ p) (span {p_1})
⊢ ∃ (p : α), Prime p ∧ P = span {p}

Tactic:
obtain ⟨p, rfl⟩ := Submodule.IsPrincipal.principal P

Premises used: Submodule.IsPrincipal.principal, rfl
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
p : α
hP : Ne (α := Ideal α) (α ∙ p) ⊥
h : IsPrime (α ∙ p)
⊢ ∃ (p_1 : α), Prime p_1 ∧ Eq (α := Ideal α) (α ∙ p) (span {p_1})

Tactic:
exact ⟨p, (span_singleton_prime (by simp [·] at hP)).mp h, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
p : α
hp : Prime p
hP : Ne (α := Ideal α) (span {p}) ⊥
⊢ p ≠ 0

Tactic:
simp [hp.ne_zero]

Premises used: Prime.ne_zero
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
p : α
hp : Prime p
hP : Ne (α := Ideal α) (span {p}) ⊥
rwa rwa₁ rwa₂ rwa₃ : Prime p
⊢ IsPrime (α := α) (span {p})

Tactic:
rwa [span_singleton_prime (by simp [hp.ne_zero])]

Premises used: Ideal.span_singleton_prime