-- Mathlib/AlgebraicGeometry/Properties.lean
theorem isIntegral_of_irreducibleSpace_of_isReduced [IsReduced X] [H : IrreducibleSpace X] :
    IsIntegral X

Proof state:
case intro.intro.intro.intro
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
e : a * b = 0
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
⊢ False

Tactic:
replace e := congr_arg (X.presheaf.germ U x hxU) e

Result:
case intro.intro.intro.intro
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (a * b) = (ConcreteCategory.hom (X.presheaf.germ U x hxU)) 0
⊢ False

Proof state:
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
e : a * b = 0
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
⊢ False

Tactic:
obtain ⟨x, ⟨hxU, hx₁⟩, _, hx₂⟩ :=
  nonempty_preirreducible_inter (X.basicOpen a).2 (X.basicOpen b).2 h.1 h.2

Result:
case intro.intro.intro.intro
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
e : a * b = 0
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
⊢ False

Proof state:
case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : ∃ x y, x ≠ y
⊢ IsDomain ↑Γ(X, U)

Tactic:
have : NoZeroDivisors
    (X.toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.obj (op U)) := by
  refine ⟨fun {a b} e => ?_⟩
  simp_rw [← basicOpen_eq_bot_iff, ← Opens.not_nonempty_iff_eq_bot]
  by_contra! h
  obtain ⟨x, ⟨hxU, hx₁⟩, _, hx₂⟩ :=
    nonempty_preirreducible_inter (X.basicOpen a).2 (X.basicOpen b).2 h.1 h.2
  replace e := congr_arg (X.presheaf.germ U x hxU) e
  rw [RingHom.map_mul, RingHom.map_zero] at e
  refine zero_ne_one' (X.presheaf.stalk x) (isUnit_zero_iff.1 ?_)
  convert hx₁.mul hx₂
  exact e.symm

Result:
case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : ∃ x y, x ≠ y
this : NoZeroDivisors ↑(X.presheaf.obj (op U))
⊢ IsDomain ↑Γ(X, U)

Proof state:
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
e : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
simp_rw [← basicOpen_eq_bot_iff, ← Opens.not_nonempty_iff_eq_bot]

Result:
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
e : a * b = 0
⊢ ¬(↑(X.basicOpen a)).Nonempty ∨ ¬(↑(X.basicOpen b)).Nonempty