awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
e : a * b = 0
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
obtain :
  ∀ (x : ↥X) (hxU : x ∈ U)
    (hx₁ :
      IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
              (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) →
                (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
            a :
          (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1)))
    (w : x ∈ U)
    (hx₂ :
      IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
              (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) →
                (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
            b :
          (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))),
    False
⊢ False

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

Premises used: And.right, And.left, AlgebraicGeometry.Scheme.basicOpen, TopologicalSpace.Opens.is_open', nonempty_preirreducible_inter
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
e : a * b = 0
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
w : x ∈ U
hx₂ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        (a * b) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
replace e := congr_arg (X.presheaf.germ U x hxU) e
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
w : x ∈ U
hx₂ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
e :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        (a * b) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ HMul.hMul (α := (↑(X.presheaf.stalk x) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          a :
        (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          b :
        (↑(X.presheaf.stalk x) : Type u_1)) =
    0

Tactic:
rw [map_mul, map_zero] at e

Premises used: map_zero, map_mul
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
w : x ∈ U
hx₂ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
e :
  HMul.hMul (α := (↑(X.presheaf.stalk x) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          a :
        (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          b :
        (↑(X.presheaf.stalk x) : Type u_1)) =
    0
⊢ False

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

Premises used: CommRingCat.carrier, TopCat.Presheaf.stalk, isUnit_zero_iff, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Iff.mp, AlgebraicGeometry.PresheafedSpace.presheaf, zero_ne_one', AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
w : x ∈ U
hx₂ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
e :
  HMul.hMul (α := (↑(X.presheaf.stalk x) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          a :
        (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          b :
        (↑(X.presheaf.stalk x) : Type u_1)) =
    0
refine : IsUnit.{u_1} (M := (↑(X.presheaf.stalk x) : Type u_1)) 0
⊢ False

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

Premises used: CommRingCat.carrier, TopCat.Presheaf.stalk, isUnit_zero_iff, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Iff.mp, AlgebraicGeometry.PresheafedSpace.presheaf, zero_ne_one', AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
⊢ NoZeroDivisors.{u_1} (↑(X.presheaf.obj (op U)) : Type u_1)

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 [map_mul, map_zero] at e
    refine zero_ne_one' (X.presheaf.stalk x) (isUnit_zero_iff.1 ?_)
    convert! hx₁.mul hx₂
    exact e.symm
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this_1 : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
this : NoZeroDivisors.{u_1} (↑(X.presheaf.obj (op U)) : Type u_1)
⊢ IsDomain.{u_1} (↑Γ(X, U) : Type u_1)

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this_1 : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
this : NoZeroDivisors.{u_1} (↑(X.presheaf.obj (op U)) : Type u_1)
⊢ IsDomain.{u_1} (↑Γ(X, U) : Type u_1)

Tactic:
exact NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
⊢ IsIntegral X ↔ IrreducibleSpace.{u_1} ↥X ∧ IsReduced X

Tactic:
⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ =>
    isIntegral_of_irreducibleSpace_of_isReduced X⟩

Premises used: AlgebraicGeometry.IsIntegral, AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced, inferInstance, And.intro, Iff.intro, _private.0.AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced.match_1
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
nonempty : autoParam (Nonempty.{u_1 + 1} ↥X) IsIntegral.nonempty._autoParam
component_integral :
  autoParam (∀ (U : X.Opens) [Nonempty.{u_1 + 1} ↥(↑U : Scheme)], IsDomain.{u_1} (↑Γ(X, U) : Type u_1))
    IsIntegral.component_integral._autoParam
⊢ IsIntegral X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
⊢ autoParam (Nonempty.{u_1 + 1} ↥X) IsIntegral.nonempty._autoParam

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
component_integral : IsDomain.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)
⊢ IsDomain.{u_1} (↑Γ(X, U) : Type u_1)

Tactic:
rw [← f.preimage_image_eq U]

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
inst_2 : IsIntegral Y
inst_3 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
inst : Nonempty.{u_1 + 1} ↥(↑(f ''ᵁ U) : Scheme)
⊢ IsDomain.{u_1} (↑Γ(Y, f ''ᵁ U) : Type u_1)

Tactic:
apply +allowSynthFailures IsIntegral.component_integral

Premises used: AlgebraicGeometry.IsIntegral.component_integral
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Nonempty.{u_1 + 1} ↥(↑(f ''ᵁ U) : Scheme)

Tactic:
⟨⟨_, _, hU.some.prop, rfl⟩⟩

Premises used: Nonempty.some, Nonempty.intro, Subtype.mk, Subtype.prop, And.intro, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Nonempty.{u_1 + 1} ↥(↑(f ''ᵁ U) : Scheme)

Tactic:
exact ⟨⟨_, _, hU.some.prop, rfl⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ IsDomain.{u_1} (↑Γ(Y, f ''ᵁ U) : Type u_1)

Tactic:
have : IsDomain Γ(Y, f ''ᵁ U) := by
    apply +allowSynthFailures IsIntegral.component_integral
    exact ⟨⟨_, _, hU.some.prop, rfl⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : IsDomain.{u_1} (↑Γ(Y, f ''ᵁ U) : Type u_1)
⊢ IsDomain.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)

Tactic:
(asIso <| f.app (f ''ᵁ U) :
    Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CategoryTheory.Iso.commRingCatIsoToRingEquiv, RingEquiv.toMulEquiv, AlgebraicGeometry.Scheme.Hom.app, MulEquiv.isDomain, CategoryTheory.Iso.symm, CategoryTheory.Functor.obj, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : IsDomain.{u_1} (↑Γ(Y, f ''ᵁ U) : Type u_1)
⊢ IsDomain.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)

Tactic:
exact (asIso <| f.app (f ''ᵁ U) :
    Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CategoryTheory.Iso.commRingCatIsoToRingEquiv, RingEquiv.toMulEquiv, AlgebraicGeometry.Scheme.Hom.app, MulEquiv.isDomain, CategoryTheory.Iso.symm, CategoryTheory.Functor.obj, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
h : IsIntegral X
f : X ⟶ Y
inst : IsIso f
suffices : Nonempty.{u + 1} ↥Y
⊢ IsIntegral Y

Tactic:
suffices Nonempty Y from isIntegral_of_isOpenImmersion (inv f)
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
h : IsIntegral X
f : X ⟶ Y
inst : IsIso f
⊢ Nonempty.{u + 1} ↥Y

Tactic:
Nonempty.map f inferInstance

Premises used: CategoryTheory.ConcreteCategory.hom, inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Nonempty.map, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
h : IsIntegral X
f : X ⟶ Y
inst : IsIso f
⊢ Nonempty.{u + 1} ↥Y

Tactic:
exact Nonempty.map f inferInstance

Premises used: CategoryTheory.ConcreteCategory.hom, inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Nonempty.map, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
⊢ IrreducibleSpace.{u_1} (PrimeSpectrum (↑R : Type u_1))

Tactic:
PrimeSpectrum.irreducibleSpace (R := R)

Premises used: PrimeSpectrum.irreducibleSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
⊢ IrreducibleSpace.{u_1} ↥(Spec R)

Tactic:
convert! PrimeSpectrum.irreducibleSpace (R := R)

Premises used: PrimeSpectrum.irreducibleSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
⊢ IsIntegral.{u_1} (Spec R)

Tactic:
isIntegral_of_irreducibleSpace_of_isReduced _

Premises used: AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
R : CommRingCat
⊢ IsIntegral.{u_1} (Spec R) ↔ IsDomain.{u_1} (↑R : Type u_1)

Tactic:
⟨fun _ => MulEquiv.isDomain Γ(Spec R, ⊤)
    (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv.toMulEquiv, fun _ => inferInstance⟩

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, AlgebraicGeometry.Spec, CommRingCat.carrier, RingEquiv.toMulEquiv, inferInstance, AlgebraicGeometry.Scheme.ΓSpecIso, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, MulEquiv.isDomain, Iff.intro, CategoryTheory.Iso.symm, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Top.top, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsAffine X
inst_1 : Nonempty.{u_1 + 1} ↥X
inst_2 : IsDomain.{u_1} (↑Γ(X, ⊤) : Type u_1)
⊢ IsIntegral X

Tactic:
isIntegral_of_isOpenImmersion X.isoSpec.hom

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.isIntegral_of_isOpenImmersion, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
rw :
  ∀ (a : (↑Γ(X, V) : Type u_1)),
    Eq (α := (↑Γ(X, U) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i.op) :
              (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
            a :
          (↑Γ(X, U) : Type u_1))
        (0 : (↑Γ(X, U) : Type u_1)) →
      a = 0
⊢ Function.Injective (α := (↑Γ(X, V) : Type u_1)) (β := (↑Γ(X, U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X.presheaf.map i.op)) :
      (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
hx :
  Eq (α := (↑Γ(X, U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
        x :
      (↑Γ(X, U) : Type u_1))
    (0 : (↑Γ(X, U) : Type u_1))
rw :
  ∀
    (hx :
      X.basicOpen (U := U)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i.op) :
              (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
            x) =
        ⊥),
    X.basicOpen x = ⊥
⊢ x = 0

Tactic:
rw [← basicOpen_eq_bot_iff] at hx ⊢

Premises used: AlgebraicGeometry.basicOpen_eq_bot_iff
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
hx :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
        x) =
    ⊥
⊢ U ⊓ X.basicOpen x = ⊥

Tactic:
rw [Scheme.basicOpen_res] at hx

Premises used: AlgebraicGeometry.Scheme.basicOpen_res
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
hx : U ⊓ X.basicOpen x = ⊥
revert : ∀ (hx : U ⊓ X.basicOpen x = ⊥), X.basicOpen x = ⊥
⊢ X.basicOpen x = ⊥

Tactic:
revert hx