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}))))
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
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