awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
inst_2 : Submodule.IsPrincipal (M := R) (R ∙ x)
rw :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
rw₁ :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
rw₂ :
  Eq (α := Submodule S S) (Ideal.span (Set.image (α := R) (⇑f : (a : R) → S) {x}))
    (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
rw₃ :
  Eq (α := Submodule S S) (Ideal.span (singleton (α := S) ((f : (a : R) → S) x : S)))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
rw₄ rw₅ :
  Eq (α := Submodule S S) (Ideal.span (singleton (α := S) ((f : (a : R) → S) x : S)))
    (Ideal.span (singleton (α := S) ((f : (a : R) → S) x : S)))
⊢ Eq (α := Submodule S S) (Ideal.map f (R ∙ x)) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))

Tactic:
rw [← Ideal.span, ← Set.image_singleton, Ideal.map_span, Set.image_singleton,
      Ideal.submodule_span_eq]

Premises used: Ideal.submodule_span_eq, Set.image_singleton, Ideal.map_span, Ideal.span
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
inst_2 : Submodule.IsPrincipal (M := R) (R ∙ x)
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := S) (Ideal.map f (R ∙ x))

Tactic:
exact ⟨f x, by
    rw [← Ideal.span, ← Set.image_singleton, Ideal.map_span, Set.image_singleton,
      Ideal.submodule_span_eq]⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
⊢ LE.le (α := Ideal ((i : ι) → R i)) (Ideal.span {HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1)})
    (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i))

Tactic:
simp [Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
refine :
  ∀ (x : (i : ι) → R i)
    (hx :
      Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
        (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i)) x),
    Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
      (Ideal.span {HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1)}) x
⊢ Eq (α := Ideal ((i : ι) → R i)) (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i))
    (Ideal.span {HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1)})

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (by simp [Ideal.span_le])

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx :
  Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i)) x
⊢ x i = 0

Tactic:
simp only [RingHom.mem_ker, Pi.evalRingHom_apply] at hx

Premises used: Pi.evalRingHom_apply, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
rw : HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1) ∣ x
⊢ Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (Ideal.span {HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1)}) x

Tactic:
rw [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
h : x = HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1) * (x + Pi.single (M := R) i 1)
⊢ HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1) ∣ x

Tactic:
use x + Pi.single i 1

Premises used: Pi.single, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
⊢ x = HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1) * (x + Pi.single (M := R) i 1)

Tactic:
simp [mul_add, sub_mul, one_mul, ← Pi.single_mul_left, hx]

Premises used: sub_mul, Pi.single_mul_left, mul_add, one_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
rcases : ∀ (x' : A) (hx' : (f : (a : A) → B) x' = x), ∃ y ∈ J, (f : (a : A) → B) y = x
⊢ ∃ y ∈ J, (f : (a : A) → B) y = x

Tactic:
rcases surj x with ⟨x', hx'⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
x' : A
hx' : (f : (a : A) → B) x' = x
⊢ x' ∈ RingHom.ker f ⊔ J

Tactic:
rw [← hx', ← Ideal.mem_comap, eq] at hx

Premises used: Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
x' : A
hx' : (f : (a : A) → B) x' = x
hx₁ : x' ∈ RingHom.ker f ⊔ J
⊢ (f : (a : A) → B) x' = x

Tactic:
rw [← hx', ← Ideal.mem_comap, eq] at hx

Premises used: Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : (f : (a : A) → B) x' = x
rcases :
  ∀ (y : A) (hy : Membership.mem (γ := Submodule A A) (RingHom.ker f) y) (z : A) (hz : z ∈ J) (hyz : y + z = x'),
    ∃ y ∈ J, (f : (a : A) → B) y = x
⊢ ∃ y ∈ J, (f : (a : A) → B) y = x

Tactic:
rcases Submodule.mem_sup.mp hx with ⟨y, hy, z, hz, hyz⟩

Premises used: Iff.mp, Submodule.mem_sup
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : (f : (a : A) → B) x' = x
y : A
hy : Membership.mem (γ := Submodule A A) (RingHom.ker f) y
z : A
hz : z ∈ J
hyz : y + z = x'
right : (f : (a : A) → B) z = x
⊢ ∃ y ∈ J, (f : (a : A) → B) y = x

Tactic:
use z, hz
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : (f : (a : A) → B) x' = x
y : A
hy : Membership.mem (γ := Submodule A A) (RingHom.ker f) y
z : A
hz : z ∈ J
hyz : y + z = x'
⊢ (f : (a : A) → B) z = x

Tactic:
simpa [← hx', ← hyz, ← RingHom.mem_ker] using hy

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
⊢ I = map f J

Tactic:
le_antisymm (fun x hx ↦ ?_)
    (Ideal.map_le_iff_le_comap.mpr (le_of_le_of_eq le_sup_right eq.symm))

Premises used: Iff.mpr, le_of_le_of_eq, le_sup_right, Ideal.map_le_iff_le_comap, le_antisymm, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
refine : ∀ (x : B) (hx : x ∈ I), Membership.mem (γ := Submodule B B) (map f J) x
⊢ I = map f J

Tactic:
refine le_antisymm (fun x hx ↦ ?_)
    (Ideal.map_le_iff_le_comap.mpr (le_of_le_of_eq le_sup_right eq.symm))

Premises used: Iff.mpr, le_of_le_of_eq, Ideal.map_le_iff_le_comap, le_antisymm, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
rcases : ∀ (y : A) (mem : y ∈ J) (hy : (f : (a : A) → B) y = x), Membership.mem (γ := Submodule B B) (map f J) x
⊢ Membership.mem (γ := Submodule B B) (map f J) x

Tactic:
rcases Ideal.exists_of_comap_eq_ker_sup _ surj eq hx with ⟨y, mem, hy⟩

Premises used: Ideal.exists_of_comap_eq_ker_sup
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
y : A
mem : y ∈ J
hy : (f : (a : A) → B) y = x
⊢ Membership.mem (γ := Submodule B B) (map f J) x

Tactic:
simpa [← hy] using Ideal.mem_map_of_mem _ mem

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ I.IsMaximal ↔ IsCoatom I

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Ideal.IsMaximal.mk, Ideal.IsMaximal.out, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
h : I.IsMaximal
⊢ I ≠ ⊤

Tactic:
(isMaximal_def.1 h).1

Premises used: And.left, Iff.mp, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
h : I.IsMaximal
⊢ I < ⊤

Tactic:
h.ne_top.lt_top

Premises used: Ne.lt_top, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
simp_rw : IsCoatom I ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
simp_rw₁ :
  (I ≠ ⊤ ∧ ∀ (H : Ideal α) (g : α), I ≤ H → g ∉ I → g ∈ H → H = ⊤) ↔
    1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
simp_rw₂ :
  (1 ∉ I ∧ ∀ (H : Ideal α) (g : α), I ≤ H → g ∉ I → g ∈ H → H = ⊤) ↔
    1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
simp_rw [isMaximal_def, SetLike.isCoatom_iff, Ideal.ne_top_iff_one, ← Ideal.eq_top_iff_one]

Premises used: SetLike.isCoatom_iff, Ideal.ne_top_iff_one, Ideal.eq_top_iff_one, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I J : Ideal α
hI : I.IsMaximal
hJ : J ≠ ⊤
IJ : I ≤ J
⊢ I = J

Tactic:
eq_iff_le_not_lt.2 ⟨IJ, fun h => hJ (hI.1.2 _ h)⟩

Premises used: Iff.mpr, And.right, Ideal.IsMaximal.out, And.intro, eq_iff_le_not_lt
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I J : Ideal α
hI : I.IsMaximal
hJ : J ≠ ⊤
⊢ I = J → I ≤ J

Tactic:
aesop
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
⊢ IsCoatomic.{u} (Ideal α)

Tactic:
CompleteLattice.coatomic_of_top_compact isCompactElement_top

Premises used: CompleteLattice.coatomic_of_top_compact, Ideal.isCompactElement_top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
hne : M ≠ M'
contrapose! : ∀ (h : M ⊔ M' ≠ ⊤), M = M'
⊢ M ⊔ M' = ⊤

Tactic:
contrapose! hne with h
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
h : M ⊔ M' ≠ ⊤
⊢ M = M'

Tactic:
hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)

Premises used: LE.le.trans_eq, le_sup_left, le_sup_right, Ideal.IsMaximal.eq_of_le, Ideal.IsMaximal.ne_top, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
h : M ⊔ M' ≠ ⊤
⊢ M = M'

Tactic:
exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)

Premises used: LE.le.trans_eq, le_sup_left, le_sup_right, Ideal.IsMaximal.eq_of_le, Ideal.IsMaximal.ne_top, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I ≠ ⊤
⊢ ∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M

Tactic:
let ⟨m, hm⟩ := (eq_top_or_exists_le_coatom I).resolve_left hI
  ⟨m, ⟨⟨hm.1⟩, hm.2⟩⟩

Premises used: Exists, Or.resolve_left, IsCoatomic.eq_top_or_exists_le_coatom, LE.le, Ideal.IsMaximal.mk, And, And.right, And.left, And.intro, Exists.intro, Ideal.IsMaximal, _private.0.Ideal.exists_le_maximal.match_1
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
inst_1 : Nontrivial α
⊢ ∃ (M : Ideal α), M.IsMaximal

Tactic:
let ⟨I, ⟨hI, _⟩⟩ := exists_le_maximal (⊥ : Ideal α) bot_ne_top
  ⟨I, hI⟩

Premises used: _private.0.Ideal.exists_maximal.match_1, Exists, Bot.bot, Exists.intro, Ideal.IsMaximal, Ideal.exists_le_maximal, bot_ne_top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ I ≠ ⊤ ↔ ∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M

Tactic:
⟨exists_le_maximal I, ?_⟩

Premises used: Iff.intro, Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
refine : (∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M) → I ≠ ⊤
⊢ I ≠ ⊤ ↔ ∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M

Tactic:
refine ⟨exists_le_maximal I, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
contrapose! : I = ⊤ → ∀ (M : Ideal α) (_ : M.IsMaximal), ¬I ≤ M
⊢ (∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M) → I ≠ ⊤

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
M : Ideal α
hMmax : M.IsMaximal
rw : ¬M = ⊤
⊢ ¬⊤ ≤ M

Tactic:
rw [top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
M : Ideal α
hMmax : M.IsMaximal
⊢ ¬M = ⊤

Tactic:
IsMaximal.ne_top hMmax

Premises used: Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
M : Ideal α
hMmax : M.IsMaximal
⊢ ¬M = ⊤

Tactic:
exact IsMaximal.ne_top hMmax

Premises used: Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
inst_1 : Nontrivial α
rcases : ∀ (M : Ideal α) (hM : M ≠ ⊤), (∀ (b : Ideal α), M < b → b = ⊤) → Nontrivial.{u} (Ideal α)
⊢ Nontrivial.{u} (Ideal α)

Tactic:
rcases @exists_maximal α _ _ with ⟨M, hM, _⟩

Premises used: Ideal.exists_maximal
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
inst_1 : Nontrivial α
M : Ideal α
hM : M ≠ ⊤
right : ∀ (b : Ideal α), M < b → b = ⊤
⊢ Nontrivial.{u} (Ideal α)

Tactic:
nontrivial_of_ne M ⊤ hM

Premises used: nontrivial_of_ne, Top.top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
inst_1 : Nontrivial α
M : Ideal α
hM : M ≠ ⊤
right : ∀ (b : Ideal α), M < b → b = ⊤
⊢ Nontrivial.{u} (Ideal α)

Tactic:
exact nontrivial_of_ne M ⊤ hM

Premises used: nontrivial_of_ne, Top.top
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
by_contra : ∀ (hnonmax : ¬J = ⊤), False
⊢ J = ⊤

Tactic:
by_contra hnonmax
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
rcases : ∀ (M : Ideal α) (hM1 : M.IsMaximal) (hM2 : J ≤ M), False
⊢ False

Tactic:
rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
M : Ideal α
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ False

Tactic:
hmax M (lt_of_lt_of_le hPJ hM2) hM1

Premises used: lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
M : Ideal α
hM1 : M.IsMaximal
hM2 : J ≤ M
⊢ False

Tactic:
exact hmax M (lt_of_lt_of_le hPJ hM2) hM1

Premises used: lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
⊢ 1 ∉ I

Tactic:
obtain ⟨H₁, H₂⟩ := isMaximal_iff.1 hI

Premises used: Ideal.isMaximal_iff, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
⊢ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
obtain ⟨H₁, H₂⟩ := isMaximal_iff.1 hI

Premises used: Ideal.isMaximal_iff, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
rcases :
  ∀ (y z : α) (hz : Membership.mem (γ := Ideal α) (span (↑I : Set α)) z) (hy : 1 = y * x + z),
    ∃ (y : α), ∃ i ∈ I, y * x + i = 1
⊢ ∃ (y : α), ∃ i ∈ I, y * x + i = 1

Tactic:
rcases mem_span_insert.1
      (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx
        (subset_span (mem_insert _ _))) with
    ⟨y, z, hz, hy⟩

Premises used: Ideal.subset_span, Set.Subset.trans, Insert.insert, SetLike.coe, Iff.mp, Set.mem_insert, Ideal.span, Ideal.mem_span_insert, Set.subset_insert
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : Membership.mem (γ := Ideal α) (span (↑I : Set α)) z
hy : 1 = y * x + z
⊢ ∃ (y : α), ∃ i ∈ I, y * x + i = 1

Tactic:
⟨y, z, ?_, hy.symm⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : Membership.mem (γ := Ideal α) (span (↑I : Set α)) z
hy : 1 = y * x + z
refine : z ∈ I
⊢ ∃ (y : α), ∃ i ∈ I, y * x + i = 1

Tactic:
refine ⟨y, z, ?_, hy.symm⟩
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : Membership.mem (γ := Ideal α) (span (↑I : Set α)) z
hy : 1 = y * x + z
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Ideal α) (span (↑I : Set α)) z
⊢ z ∈ I

Tactic:
rwa [← span_eq I]

Premises used: Ideal.span_eq
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : x * y ∈ sInf s
hx : x ∉ sInf s
rw : ∀ (e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I) (hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x ∈ I) ⦃I : Ideal α⦄, I ∈ s → y ∈ I
⊢ y ∈ sInf s

Tactic:
rw [Ideal.mem_sInf] at hx e ⊢

Premises used: Ideal.mem_sInf
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x ∈ I
⊢ ∃ I ∈ s, x ∉ I

Tactic:
push Not at hx

Premises used: Not
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
hx : ∃ I ∈ s, x ∉ I
obtain : ∀ (I : Ideal α) (hI : I ∈ s) (hI' : x ∉ I) ⦃I : Ideal α⦄, I ∈ s → y ∈ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y ∈ I

Tactic:
obtain ⟨I, hI, hI'⟩ := hx
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
I : Ideal α
hI : I ∈ s
hI' : x ∉ I
J : Ideal α
hJ : J ∈ s
inl : ∀ (h : I ≤ J), y ∈ J
inr : ∀ (h : J ≤ I), y ∈ J
⊢ y ∈ J

Tactic:
rcases hs'.total hI hJ with h | h

Premises used: IsChain.total
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
I : Ideal α
hI : I ∈ s
hI' : x ∉ I
J : Ideal α
hJ : J ∈ s
h : I ≤ J
⊢ y ∈ J

Tactic:
h (((H I hI).mem_or_mem (e hI)).resolve_left hI')

Premises used: Set.Mem, Or.resolve_left, Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
I : Ideal α
hI : I ∈ s
hI' : x ∉ I
J : Ideal α
hJ : J ∈ s
h : I ≤ J
⊢ y ∈ J

Tactic:
exact h (((H I hI).mem_or_mem (e hI)).resolve_left hI')

Premises used: Or.resolve_left, Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
I : Ideal α
hI : I ∈ s
hI' : x ∉ I
J : Ideal α
hJ : J ∈ s
h : J ≤ I
⊢ y ∈ J

Tactic:
((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x

Premises used: Or.resolve_left, Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
I : Ideal α
hI : I ∈ s
hI' : x ∉ I
J : Ideal α
hJ : J ∈ s
h : J ≤ I
⊢ y ∈ J

Tactic:
exact ((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x

Premises used: Or.resolve_left, Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
p : α
hp : p ≠ 0
⊢ IsPrime (α := α) (span {p}) ↔ Prime p

Tactic:
simp [isPrime_iff, Prime, span_singleton_eq_top, hp, mem_span_singleton]

Premises used: Prime, Ideal.span_singleton_eq_top, Ideal.isPrime_iff, Ideal.mem_span_singleton
-- 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 α))
⊢ I ≤ J

Tactic:
have IJ : I ≤ J := Set.Subset.trans (subset_insert _ _) subset_span
-- 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
⊢ x ∈ J

Tactic:
have xJ : x ∈ J := Ideal.subset_span (Set.mem_insert x I)
-- 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
⊢ 1 ∉ I

Tactic:
obtain ⟨_, oJ⟩ := isMaximal_iff.1 H

Premises used: Ideal.isMaximal_iff, Iff.mp
-- 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
⊢ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
obtain ⟨_, oJ⟩ := isMaximal_iff.1 H

Premises used: Ideal.isMaximal_iff, Iff.mp