awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X Y : Scheme
f : X ⟶ Y
this :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIntegralHom f → topologically (@IsClosedMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsIntegralHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
          (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)) →
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      topologically @IsClosedMap (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
          (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
fun a i ↦ this _ ⟨_, rfl⟩ (a i)

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X Y : Scheme
f : X ⟶ Y
this :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIntegralHom f → topologically (@IsClosedMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsIntegralHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
          (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)) →
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      topologically @IsClosedMap (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
          (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
exact fun a i ↦ this _ ⟨_, rfl⟩ (a i)

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X Y : Scheme
f : X ⟶ Y
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R), IsIntegralHom f → topologically (@IsClosedMap) f
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inr :
  ∀
    (this :
      ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
        IsIntegralHom f → topologically (@IsClosedMap) f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f → topologically (@IsClosedMap) f
wlog :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
wlog hX : ∃ S, X = Spec S generalizing X
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
H : IsIntegralHom f
⊢ IsAffine X

Tactic:
have inst : IsAffine X := isAffine_of_isAffineHom f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
H : IsIntegralHom f
inst : IsAffine X
inr : topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)
⊢ topologically (@IsClosedMap) f

Tactic:
rw [← cancel_left_of_respectsIso (P := topologically _) X.isoSpec.inv]

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.topologically, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
H : IsIntegralHom f
inst : IsAffine X
⊢ IsIntegralHom (X.isoSpec.inv ≫ f)

Tactic:
rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv] at H

Premises used: AlgebraicGeometry.IsIntegralHom, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : IsAffine X
H : IsIntegralHom (X.isoSpec.inv ≫ f)
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)

Tactic:
this _ ⟨_, rfl⟩ H

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this :
  ∀ ⦃X : Scheme.{u}⦄ (f : X ⟶ Spec R) (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : IsAffine X
H : IsIntegralHom (X.isoSpec.inv ≫ f)
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)

Tactic:
exact this _ ⟨_, rfl⟩ H

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S : Scheme
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R), IsIntegralHom f → topologically (@IsClosedMap) f
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S_1 : Scheme
R S : CommRingCat
f : Spec S ⟶ Spec R
obtain : ∀ (φ : R ⟶ S), IsIntegralHom (Spec.map φ) → topologically (@IsClosedMap) (Spec.map φ)
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S_1 : Scheme
R S : CommRingCat
φ : R ⟶ S
rw : (CommRingCat.Hom.hom φ).IsIntegral → topologically (@IsClosedMap) (Spec.map φ)
⊢ IsIntegralHom (Spec.map φ) → topologically (@IsClosedMap) (Spec.map φ)

Tactic:
rw [SpecMap_iff]

Premises used: AlgebraicGeometry.IsIntegralHom.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S_1 : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (CommRingCat.Hom.hom φ).IsIntegral → topologically (@IsClosedMap) (Spec.map φ)

Tactic:
PrimeSpectrum.isClosedMap_comap_of_isIntegral _

Premises used: PrimeSpectrum.isClosedMap_comap_of_isIntegral, AlgebraicGeometry.topologically, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S_1 : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (CommRingCat.Hom.hom φ).IsIntegral → topologically (@IsClosedMap) (Spec.map φ)

Tactic:
exact PrimeSpectrum.isClosedMap_comap_of_isIntegral _

Premises used: PrimeSpectrum.isClosedMap_comap_of_isIntegral
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩

Premises used: AlgebraicGeometry.IsIntegralHom, _private.0.AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom.match_1, inferInstance, And.intro, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
refine : UniversallyClosed f ∧ IsAffineHom f → ∀ (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f), IsIntegralHom f
⊢ IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
wlog :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
⊢ IsIntegralHom f

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsIntegralHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ IsIntegralHom f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
H₃ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ IsAffineHom f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
H₃ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
H₄ : IsAffineHom f
⊢ ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
H₃ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
H₄ : IsAffineHom f
this₁ :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
⊢ ¬∃ (R : CommRingCat.{u}), Y = Spec R

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsAffineHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsAffineHom) Y.affineCover] at H₂

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
H₃ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsAffineHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsAffineHom) Y.affineCover] at H₂

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
H₂ : IsAffineHom f
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
H₃ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsAffineHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
this₁ :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
⊢ ¬∃ (R : CommRingCat.{u}), Y = Spec R

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsAffineHom) Y.affineCover] at H₂

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
H₂ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsAffineHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsIntegralHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
fun _ ↦ this inferInstance inferInstance ⟨_, rfl⟩

Premises used: inferInstance, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    UniversallyClosed (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
H₂ :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsAffineHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsIntegralHom (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)

Tactic:
exact fun _ ↦ this inferInstance inferInstance ⟨_, rfl⟩

Premises used: inferInstance, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain : ∀ (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f), IsIntegralHom f
⊢ IsIntegralHom f

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
wlog :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
⊢ IsIntegralHom f

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsAffine X

Tactic:
have inst : IsAffine X := isAffine_of_isAffineHom f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : IsAffine X
inr : IsIntegralHom (X.isoSpec.inv ≫ f)
⊢ IsIntegralHom f

Tactic:
rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv]

Premises used: AlgebraicGeometry.IsIntegralHom, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : IsAffine X
⊢ IsIntegralHom (X.isoSpec.inv ≫ f)

Tactic:
this _ inferInstance inferInstance ⟨_, rfl⟩

Premises used: inferInstance, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) {f : X ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIntegralHom f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : IsAffine X
⊢ IsIntegralHom (X.isoSpec.inv ≫ f)

Tactic:
exact this _ inferInstance inferInstance ⟨_, rfl⟩

Premises used: inferInstance, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain : ∀ (S : CommRingCat.{u}) {f : Spec S ⟶ Spec R} (H₁ : UniversallyClosed f) (H₂ : IsAffineHom f), IsIntegralHom f
⊢ IsIntegralHom f

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ ∃ (φ : R ⟶ S), Spec.map φ = f

Tactic:
⟨_, Spec.map_preimage _⟩

Premises used: Exists.intro, AlgebraicGeometry.Spec.map_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
obtain : ∀ (φ : R ⟶ S) (H₁ : UniversallyClosed (Spec.map φ)) (H₂ : IsAffineHom (Spec.map φ)), IsIntegralHom (Spec.map φ)
⊢ IsIntegralHom f

Tactic:
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
rw : (CommRingCat.Hom.hom φ).IsIntegral
⊢ IsIntegralHom (Spec.map φ)

Tactic:
rw [SpecMap_iff]

Premises used: AlgebraicGeometry.IsIntegralHom.SpecMap_iff