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

Proof state:
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
⊢ IsIntegral X

Tactic:
constructor

Result:
case nonempty
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
⊢ autoParam (Nonempty ↑↑X.toPresheafedSpace) _auto✝

case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
⊢ autoParam (∀ (U : X.Opens) [inst : Nonempty ↑↑(↑U).toPresheafedSpace], IsDomain ↑Γ(X, U)) _auto✝

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

Tactic:
rw [RingHom.map_mul, RingHom.map_zero] at 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 * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ False

Proof state:
case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
⊢ autoParam (∀ (U : X.Opens) [inst : Nonempty ↑↑(↑U).toPresheafedSpace], IsDomain ↑Γ(X, U)) _auto✝

Tactic:
intro U hU

Result:
case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ IsDomain ↑Γ(X, U)

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

Tactic:
haveI := (@LocallyRingedSpace.component_nontrivial X.toLocallyRingedSpace U hU).1

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
⊢ 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
⊢ NoZeroDivisors ↑(X.presheaf.obj (op U))

Tactic:
refine ⟨fun {a b} e => ?_⟩

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
⊢ a = 0 ∨ b = 0

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
⊢ ¬(↑(X.basicOpen a)).Nonempty ∨ ¬(↑(X.basicOpen b)).Nonempty

Tactic:
by_contra! h

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
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
⊢ False

Proof state:
case h.e'_3
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 * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ 0 =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a *
      (ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b

Tactic:
exact e.symm

Result:
no goals

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))
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 * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ False

Tactic:
refine zero_ne_one' (X.presheaf.stalk x) (isUnit_zero_iff.1 ?_)

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 * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ IsUnit 0

Proof state:
case nonempty
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↑↑X.toPresheafedSpace
⊢ autoParam (Nonempty ↑↑X.toPresheafedSpace) _auto✝

Tactic:
infer_instance

Result:
no goals

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
this : NoZeroDivisors ↑(X.presheaf.obj (op U))
⊢ IsDomain ↑Γ(X, U)

Tactic:
exact NoZeroDivisors.to_isDomain _

Result:
no goals

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))
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 * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ IsUnit 0

Tactic:
convert hx₁.mul hx₂

Result:
case h.e'_3
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 * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ 0 =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a *
      (ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b