Theorem: ideal.span_ne_mem_kaplanski.set (Kaplanski4/Kaplanski.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
⊢ Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
Tactic:
have hzero : 0 ∉ S := by
  intro h
  rcases Submonoid.exists_multiset_of_mem_closure h with ⟨l, ⟨hl, hprod⟩⟩
  exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
⊢ Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
⊢ Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
Tactic:
intro h
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False
Tactic:
rcases exists_maximal_ideal _ hzero with ⟨T, hT, hT₂⟩
State after:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
⊢ False

State before:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
⊢ False
Tactic:
have hT₃ : T ≠ ⊥ := by
  intro h₂
  rw [h₂] at hT₂
  exact ha (Ideal.span_singleton_eq_bot.1 (hT₂ (Ideal.span {a}) h (zero_le (Ideal.span {a}))))
State after:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
⊢ False

State before:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
⊢ False
Tactic:
rw [Set.nonempty_def] at hP
State after:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : ∃ x, x ∈ {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
⊢ False

State before:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : ∃ x, x ∈ {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
⊢ False
Tactic:
cases' hP with x hx
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
⊢ False

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
⊢ False
Tactic:
have := Set.mem_of_subset_of_mem Submonoid.subset_closure hx
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ ↑(Submonoid.closure {r | Prime r})
⊢ False

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ ↑(Submonoid.closure {r | Prime r})
⊢ False
Tactic:
simp at this
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ Submonoid.closure {r | Prime r}
⊢ False

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ Submonoid.closure {r | Prime r}
⊢ False
Tactic:
rw [← Submonoid.mem_toSubsemigroup] at this
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False
Tactic:
have := Set.nonempty_def.2 ⟨x, this⟩
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this✝ : x ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this✝ : x ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False
Tactic:
rcases (H T) hT₃ (isPrime_of_maximal this hT hT₂) with ⟨x, H₃, H₄⟩
State after:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x✝ : R
hx : x✝ ∈ {r | Prime r}
this✝ : x✝ ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False

State before:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x✝ : R
hx : x✝ ∈ {r | Prime r}
this✝ : x✝ ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
Tactic:
rw [Kaplansky.set_def, Set.eq_empty_iff_forall_not_mem] at hT
State after:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : ∀ (x : R), x ∉ ↑T ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x✝ : R
hx : x✝ ∈ {r | Prime r}
this✝ : x✝ ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False

State before:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : ∀ (x : R), x ∉ ↑T ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x✝ : R
hx : x✝ ∈ {r | Prime r}
this✝ : x✝ ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
Tactic:
exact hT x ⟨H₃, Submonoid.subset_closure H₄⟩
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
⊢ 0 ∉ Submonoid.closure {r | Prime r}
Tactic:
intro h
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
⊢ False

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
⊢ False
Tactic:
rcases Submonoid.exists_multiset_of_mem_closure h with ⟨l, ⟨hl, hprod⟩⟩
State after:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | Prime r}
hprod : Multiset.prod l = 0
⊢ False

State before:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | Prime r}
hprod : Multiset.prod l = 0
⊢ False
Tactic:
exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
⊢ T ≠ ⊥
Tactic:
intro h₂
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
h₂ : T = ⊥
⊢ False

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
h₂ : T = ⊥
⊢ False
Tactic:
rw [h₂] at hT₂
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, ⊥ ≤ I → I = ⊥
h₂ : T = ⊥
⊢ False

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, ⊥ ≤ I → I = ⊥
h₂ : T = ⊥
⊢ False
Tactic:
exact ha (Ideal.span_singleton_eq_bot.1 (hT₂ (Ideal.span {a}) h (zero_le (Ideal.span {a}))))
State after:
no goals