-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma basicOpen_injOn_isIdempotentElem :
    {e : R | IsIdempotentElem e}.InjOn basicOpen := fun x hx y hy eq ↦ by
  by_contra! ne
  wlog ne' : x * y ≠ x generalizing x y
  · apply this y hy x hx eq.symm ne.symm
    rwa [mul_comm, of_not_not ne']
  have : x ∉ Ideal.span {y} := fun mem ↦ ne' <| by
    obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton'.mp mem
    rw [mul_assoc, hy]
  have ⟨p, prime, le, nmem⟩ := Ideal.exists_le_prime_nmem_of_isIdempotentElem _ x hx this
  exact ne_of_mem_of_not_mem' (a := ⟨p, prime⟩) nmem
    (not_not.mpr <| p.span_singleton_le_iff_mem.mp le) eq

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
⊢ False

Tactic:
wlog ne' : x * y ≠ x generalizing x y

Result:
case inr
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ False

R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
⊢ False

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
mem : x ∈ Ideal.span {y}
⊢ x * y = x

Tactic:
obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton'.mp mem

Result:
case intro
R : Type u
inst✝ : CommSemiring R
y : R
hy : y ∈ {e | IsIdempotentElem e}
r : R
hx : r * y ∈ {e | IsIdempotentElem e}
eq : basicOpen (r * y) = basicOpen y
ne : r * y ≠ y
ne' : r * y * y ≠ r * y
mem : r * y ∈ Ideal.span {y}
⊢ r * y * y = r * y

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
⊢ False

Tactic:
have : x ∉ Ideal.span {y} := fun mem ↦ ne' <| by
  obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton'.mp mem
  rw [mul_assoc, hy]

Result:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
⊢ False

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
y : R
hy : y ∈ {e | IsIdempotentElem e}
r : R
hx : r * y ∈ {e | IsIdempotentElem e}
eq : basicOpen (r * y) = basicOpen y
ne : r * y ≠ y
ne' : r * y * y ≠ r * y
mem : r * y ∈ Ideal.span {y}
⊢ r * y * y = r * y

Tactic:
rw [mul_assoc, hy]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
⊢ False

Tactic:
have ⟨p, prime, le, nmem⟩ := Ideal.exists_le_prime_nmem_of_isIdempotentElem _ x hx this

Result:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
p : Ideal R
prime : p.IsPrime
le : Ideal.span {y} ≤ p
nmem : x ∉ p
⊢ False

Proof state:
case inr
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ y * x ≠ y

Tactic:
rwa [mul_comm, of_not_not ne']

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
p : Ideal R
prime : p.IsPrime
le : Ideal.span {y} ≤ p
nmem : x ∉ p
⊢ False

Tactic:
exact ne_of_mem_of_not_mem' (a := ⟨p, prime⟩) nmem
  (not_not.mpr <| p.span_singleton_le_iff_mem.mp le) eq

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
⊢ x = y

Tactic:
by_contra! ne

Result:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
⊢ False

Proof state:
case inr
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ False

Tactic:
apply this y hy x hx eq.symm ne.symm

Result:
case inr
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
this :
  ∀ x ∈ {e | IsIdempotentElem e}, ∀ y ∈ {e | IsIdempotentElem e}, basicOpen x = basicOpen y → x ≠ y → x * y ≠ x → False
ne' : ¬x * y ≠ x
⊢ y * x ≠ y