awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
this_1 : SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)
L : (x : ↥(pullback f g)) → (↑{x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)} : Type u_1) :=
  fun (x : ↥(pullback f g)) ↦
    Subtype.mk (p := fun (x : ↥X × ↥Y) ↦
      Membership.mem (γ := Set (↥X × ↥Y)) {x : ↥X × ↥Y | Eq (α := ↥Z) (f x.1 : ↥Z) (g x.2 : ↥Z)} x)
      ((pullback.fst f g) x, (pullback.snd f g) x) ⋯
this : IsEmbedding L
⊢ IsEmbedding (X := ↥(pullback f g)) (Y := ↥X) ⇑(pullback.fst f g)

Tactic:
exact IsEmbedding.subtypeVal.comp ((TopCat.pullbackHomeoPreimage _ f.continuous _
    g.isEmbedding).isEmbedding.comp this)

Premises used: Homeomorph.isEmbedding, AlgebraicGeometry.Scheme.Hom.isEmbedding, Topology.IsEmbedding.comp, TopCat.pullbackHomeoPreimage, AlgebraicGeometry.Scheme.Hom.continuous, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : IsPreimmersion g
⊢ IsPreimmersion (X := Limits.pullback f g) (Limits.pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : IsPreimmersion f
⊢ IsPreimmersion (X := Limits.pullback f g) (Limits.pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Goal:
X Y Z : Scheme
f_1 : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
V : Y.Opens
inst : IsPreimmersion f
⊢ IsPreimmersion (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y), IsProper f ↔ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f
⊢ @IsProper = @IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  (IsSeparated f ∧ UniversallyClosed f) ∧ LocallyOfFiniteType f ↔
    (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f
⊢ IsProper f ↔ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Tactic:
rw [isProper_iff, ← and_assoc]

Premises used: AlgebraicGeometry.isProper_iff, and_assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (IsSeparated f ∧ UniversallyClosed f) ∧ LocallyOfFiniteType f ↔
    (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).RespectsIso
⊢ MorphismProperty.RespectsIso @IsProper

Tactic:
rw [isProper_eq]

Premises used: AlgebraicGeometry.isProper_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).RespectsIso

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderComposition
⊢ MorphismProperty.IsStableUnderComposition @IsProper

Tactic:
rw [isProper_eq]

Premises used: AlgebraicGeometry.isProper_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderComposition

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsMultiplicative
⊢ MorphismProperty.IsMultiplicative @IsProper

Tactic:
rw [isProper_eq]

Premises used: AlgebraicGeometry.isProper_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsMultiplicative

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderBaseChange
⊢ MorphismProperty.IsStableUnderBaseChange @IsProper

Tactic:
rw [isProper_eq]

Premises used: AlgebraicGeometry.isProper_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderBaseChange

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : IsZariskiLocalAtTarget.{u_1} (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)
⊢ IsZariskiLocalAtTarget @IsProper

Tactic:
rw [isProper_eq]

Premises used: AlgebraicGeometry.isProper_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget.{u_1} (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
⊢ @IsAffineHom ⊓ @IsSeparated = @IsAffineHom

Tactic:
have : (@IsAffineHom ⊓ @IsSeparated : MorphismProperty _) = @IsAffineHom :=
    inf_eq_left.mpr fun _ _ _ _ ↦ inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
rw : @IsFinite = @IsAffineHom ⊓ @IsProper
rw₁ : @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)
rw₂ : @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType))
rw₃ : @IsFinite = @IsAffineHom ⊓ @IsSeparated ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
rw₄ : @IsFinite = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
rw₅ : @IsIntegralHom ⊓ @LocallyOfFiniteType = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
rw₆ :
  @UniversallyClosed ⊓ @IsAffineHom ⊓ @LocallyOfFiniteType = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
rw₇ :
  @UniversallyClosed ⊓ (@IsAffineHom ⊓ @LocallyOfFiniteType) =
    @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
rw₈ rw₉ :
  @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType) =
    @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom

Tactic:
rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]

Premises used: inf_comm, AlgebraicGeometry.isProper_eq, AlgebraicGeometry.IsFinite.eq_inf, inf_assoc, AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_left_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
rw : (@IsProper ⊓ @IsAffineHom) f ↔ IsProper f ∧ IsAffineHom f
⊢ IsFinite f ↔ IsProper f ∧ IsAffineHom f

Tactic:
rw [eq_isProper_inf_isAffineHom]

Premises used: AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (@IsProper ⊓ @IsAffineHom) f ↔ IsProper f ∧ IsAffineHom f

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsFinite f
⊢ IsProper f

Tactic:
(IsFinite.iff_isProper_and_isAffineHom.mp ‹_›).1

Premises used: AlgebraicGeometry.IsFinite.iff_isProper_and_isAffineHom, And.left, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.HasOfPostcompProperty @UniversallyClosed @IsSeparated

Tactic:
MorphismProperty.hasOfPostcompProperty_iff_le_diagonal.mpr
    fun _ _ _ _ ↦ inferInstanceAs (UniversallyClosed _)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : UniversallyClosed (f ≫ g)
inst_1 : IsSeparated g
⊢ UniversallyClosed f

Tactic:
MorphismProperty.of_postcomp _ _ g ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.HasOfPostcompProperty @IsProper @IsSeparated

Tactic:
MorphismProperty.hasOfPostcompProperty_iff_le_diagonal.mpr
    fun _ _ _ _ ↦ inferInstanceAs (IsProper _)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : UniversallyClosed f
⊢ UniversallyClosed (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsProper (f ≫ g)
inst_1 : IsSeparated g
⊢ IsProper f

Tactic:
MorphismProperty.of_postcomp _ _ g ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsProper g
⊢ IsProper (f ≫ g) ↔ IsProper f

Tactic:
⟨fun _ ↦ .of_comp f g, fun _ ↦ inferInstance⟩

Premises used: inferInstance, AlgebraicGeometry.IsProper.of_comp, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
⊢ CompactSpace.{u} ↥X

Tactic:
have : CompactSpace X := (quasiCompact_iff_compactSpace f).mp inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
this : CompactSpace.{u} ↥X
rwa : UniversallyClosed (f ≫ Y.toSpecΓ)
rwa₁ rwa₂ rwa₃ rwa₄ : UniversallyClosed f
⊢ UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))

Tactic:
rwa [← Scheme.toSpecΓ_naturality,
      MorphismProperty.cancel_right_of_respectsIso (P := @UniversallyClosed)]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.UniversallyClosed, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
this : CompactSpace.{u} ↥X
⊢ UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))

Tactic:
have : UniversallyClosed (X.toSpecΓ ≫ Spec.map f.appTop) := by
    rwa [← Scheme.toSpecΓ_naturality,
      MorphismProperty.cancel_right_of_respectsIso (P := @UniversallyClosed)]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
this_1 : CompactSpace.{u} ↥X
this : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
⊢ UniversallyClosed X.toSpecΓ

Tactic:
have : UniversallyClosed X.toSpecΓ := .of_comp_of_isSeparated _ (Spec.map f.appTop)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
this_1 : CompactSpace.{u} ↥X
this_2 : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
rw : UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Tactic:
rw [← IsIntegralHom.SpecMap_iff, IsIntegralHom.iff_universallyClosed_and_isAffineHom]

Premises used: AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom, AlgebraicGeometry.IsIntegralHom.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
this_1 : CompactSpace.{u} ↥X
this_2 : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))

Tactic:
⟨.of_comp_surjective X.toSpecΓ _, inferInstance⟩

Premises used: AlgebraicGeometry.UniversallyClosed.of_comp_surjective, inferInstance, AlgebraicGeometry.Scheme.toSpecΓ, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
this_1 : CompactSpace.{u} ↥X
this_2 : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))

Tactic:
exact ⟨.of_comp_surjective X.toSpecΓ _, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := Iso.inv (Scheme.ΓSpecIso (CommRingCat.of K)) ≫ Scheme.Hom.appTop f
x : (Scheme.Hom.appTop f).hom'.IsIntegral
⊢ (CommRingCat.Hom.hom F).IsIntegral

Tactic:
apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, RingHom.isIntegral_respectsIso, AlgebraicGeometry.Scheme.ΓSpecIso, And.right, CategoryTheory.Iso.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := Iso.inv (Scheme.ΓSpecIso (CommRingCat.of K)) ≫ Scheme.Hom.appTop f
⊢ (Scheme.Hom.appTop f).hom'.IsIntegral

Tactic:
isIntegral_appTop_of_universallyClosed f

Premises used: AlgebraicGeometry.isIntegral_appTop_of_universallyClosed
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := Iso.inv (Scheme.ΓSpecIso (CommRingCat.of K)) ≫ Scheme.Hom.appTop f
⊢ (Scheme.Hom.appTop f).hom'.IsIntegral

Tactic:
exact isIntegral_appTop_of_universallyClosed f

Premises used: AlgebraicGeometry.isIntegral_appTop_of_universallyClosed
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := Iso.inv (Scheme.ΓSpecIso (CommRingCat.of K)) ≫ Scheme.Hom.appTop f
⊢ (CommRingCat.Hom.hom F).IsIntegral

Tactic:
have : F.hom.IsIntegral := by
    apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)
    exact isIntegral_appTop_of_universallyClosed f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := Iso.inv (Scheme.ΓSpecIso (CommRingCat.of K)) ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
⊢ let algInst := (CommRingCat.Hom.hom F).toAlgebra;
  Algebra.IsIntegral.{u, u} (↑(CommRingCat.of K) : Type u) (↑Γ(X, ⊤) : Type u)

Tactic:
algebraize [F.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := Iso.inv (Scheme.ΓSpecIso (CommRingCat.of K)) ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
algInst : Algebra (↑(CommRingCat.of K) : Type u) (↑Γ(X, ⊤) : Type u) := (CommRingCat.Hom.hom F).toAlgebra
algebraizeInst : Algebra.IsIntegral.{u, u} (↑(CommRingCat.of K) : Type u) (↑Γ(X, ⊤) : Type u)
⊢ IsField.{u} (↑Γ(X, ⊤) : Type u)

Tactic:
isField_of_isIntegral_of_isField' (Field.toIsField K)

Premises used: Field.toIsField, isField_of_isIntegral_of_isField'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := Iso.inv (Scheme.ΓSpecIso (CommRingCat.of K)) ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
algInst : Algebra (↑(CommRingCat.of K) : Type u) (↑Γ(X, ⊤) : Type u) := (CommRingCat.Hom.hom F).toAlgebra
algebraizeInst : Algebra.IsIntegral.{u, u} (↑(CommRingCat.of K) : Type u) (↑Γ(X, ⊤) : Type u)
⊢ IsField.{u} (↑Γ(X, ⊤) : Type u)

Tactic:
exact isField_of_isIntegral_of_isField' (Field.toIsField K)

Premises used: Field.toIsField, isField_of_isIntegral_of_isField'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
inst_3 : LocallyOfFiniteType f
have : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
have x : X := Nonempty.some inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
inst_3 : LocallyOfFiniteType f
x : ↥X
obtain :
  ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)),
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
inst_3 : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this_1 : Field (↑Γ(Spec (CommRingCat.of K), ⊤) : Type u) := IsField.toField ⋯
this : Field (↑Γ(X, ⊤) : Type u) := ⋯.toField
⊢ Nonempty.{u + 1} ↥(↑U : Scheme)

Tactic:
have : Nonempty U := ⟨⟨x, hxU⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
inst_3 : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this_1 : Field (↑Γ(Spec (CommRingCat.of K), ⊤) : Type u) := IsField.toField ⋯
this_2 : Field (↑Γ(X, ⊤) : Type u) := ⋯.toField
this : Nonempty.{u + 1} ↥(↑U : Scheme)
hfg :
  RingHom.FiniteType (B := (↑Γ(X, U) : Type u))
    (RingHom.comp (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
apply RingHom.finite_of_algHom_finiteType_of_isJacobsonRing (A := Γ(X, U))
    (g := (X.presheaf.map (homOfLE le_top).op).hom)

Premises used: RingHom.finite_of_algHom_finiteType_of_isJacobsonRing
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
inst_3 : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this_1 : Field (↑Γ(Spec (CommRingCat.of K), ⊤) : Type u) := IsField.toField ⋯
this_2 : Field (↑Γ(X, ⊤) : Type u) := ⋯.toField
this : Nonempty.{u + 1} ↥(↑U : Scheme)
⊢ U ≤ f ⁻¹ᵁ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Proper
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
inst_3 : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this_1 : Field (↑Γ(Spec (CommRingCat.of K), ⊤) : Type u) := IsField.toField ⋯
this_2 : Field (↑Γ(X, ⊤) : Type u) := ⋯.toField
this : Nonempty.{u + 1} ↥(↑U : Scheme)
⊢ RingHom.FiniteType (B := (↑Γ(X, U) : Type u))
    (RingHom.comp (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)))

Tactic:
exact f.finiteType_appLE (isAffineOpen_top _) hU (by simp)

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Scheme.Hom.finiteType_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
h_1 : QuasiCompact f
h : ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)
⊢ Continuous (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst rwa rwa₁ rwa₂ rwa₃ : QuasiCompact f
⊢ IsSpectralMap (α := ↥X) (β := ↥Y) ⇑f

Tactic:
rwa [← quasiCompact_iff_isSpectralMap]

Premises used: AlgebraicGeometry.quasiCompact_iff_isSpectralMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
U : Y.Opens
hU : IsCompact (↑U : Set ↥Y)
⊢ IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)

Tactic:
f.isSpectralMap.2 U.2 hU

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.Hom.isSpectralMap, Set.preimage, IsSpectralMap.isCompact_preimage_of_isOpen, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
isCompact_preimage : ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)
⊢ QuasiCompact f

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
isCompact_preimage : IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)
⊢ IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h : IsOpen U
hU' : IsCompact U
⊢ IsCompact ((TopCat.Hom.hom (inv f.base)).toFun '' U)

Tactic:
hU'.image (inv f.base).hom.continuous_toFun

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', ContinuousMap.continuous_toFun, TopCat.Hom.hom, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.inv, IsCompact.image
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h_1 : IsOpen U
hU' : IsCompact U
h : ⇑f ⁻¹' U = (TopCat.Hom.hom (inv f.base)).toFun '' U
⊢ IsCompact (X := ↥X) (⇑f ⁻¹' U)

Tactic:
convert! hU'.image (inv f.base).hom.continuous_toFun using 1

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', ContinuousMap.continuous_toFun, TopCat.Hom.hom, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.inv, IsCompact.image
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h_1 : IsOpen U
hU' : IsCompact U
h : Function.LeftInverse (⇑f) (TopCat.Hom.hom (inv f.base)).toFun
h₁ : Function.RightInverse (⇑f) (TopCat.Hom.hom (inv f.base)).toFun
⊢ ⇑f ⁻¹' U = (TopCat.Hom.hom (inv f.base)).toFun '' U

Tactic:
rw [Set.image_eq_preimage_of_inverse]

Premises used: Set.image_eq_preimage_of_inverse
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h : IsOpen U
hU' : IsCompact U
⊢ ∀ (x : ↥Y), f ((TopCat.Hom.hom (inv f.base)).toFun x) = x

Tactic:
IsIso.inv_hom_id_apply f.base

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.IsIso.inv_hom_id_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h : IsOpen U
hU' : IsCompact U
⊢ ∀ (x : ↥Y), f ((TopCat.Hom.hom (inv f.base)).toFun x) = x

Tactic:
exact IsIso.inv_hom_id_apply f.base

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.IsIso.inv_hom_id_apply