awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hX :
  ∀ (x : ↥X),
    ∃ (U : Scheme.{u}) (i : U ⟶ X) (x_1 : IsOpenImmersion i), x ∈ Scheme.Hom.opensRange i ∧ IsOpenImmersion (i ≫ f)
⊢ IsOpenImmersion f
have choose : ∀ (U : (x : ↥X) → Scheme.{u}) (i : (x : ↥X) → U x ⟶ X) (x : ∀ (x : ↥X), IsOpenImmersion (i x))
  (hxi : ∀ (x_1 : ↥X), x_1 ∈ Scheme.Hom.opensRange (i x_1)) (hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)),
  IsOpenImmersion f
Tactic: choose U i _ hxi hi using hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
⊢ IsOpenImmersion =
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
      stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  IsOpenImmersion f ↔
    ((topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
        stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
          Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
      f
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
⊢ IsZariskiLocalAtTarget.{u_1}
    (stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
have hP : RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
  Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)
Tactic: apply stalkwiseIsZariskiLocalAtTarget_of_respectsIso
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)
have hP : (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)).RespectsIso
Tactic: rw [RingHom.toMorphismProperty_respectsIso_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
⊢ (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)).RespectsIso
have h : (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
    Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)) =
  MorphismProperty.isomorphisms CommRingCat
Tactic: convert! (inferInstance : (MorphismProperty.isomorphisms CommRingCat).RespectsIso)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion (goal)
Goal:
X Y : Scheme
⊢ (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S)) =
    MorphismProperty.isomorphisms CommRingCat
have h : ∀ ⦃X Y : CommRingCat.{u_1}⦄ (f : X ⟶ Y),
  RingHom.toMorphismProperty
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑x : (a : R) → S))
      f ↔
    MorphismProperty.isomorphisms CommRingCat f
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (goal)
Goal:
⊢ @IsPreimmersion =
    @SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
  IsPreimmersion x_2 ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding)
      x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (goal)
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsPreimmersion x_2 ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding)
      x_2
have h : SurjectiveOnStalks x_2 ∧ IsEmbedding (X := ↥x) (Y := ↥x_1) ⇑x_2 ↔
  (@SurjectiveOnStalks ⊓ topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding) x_2
Tactic: rw [isPreimmersion_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
x : ↥X
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f 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) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
have h : Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) 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) (Scheme.Hom.stalkMap (f ≫ g) x)) :
    (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
Tactic: have h := (f ≫ g).stalkMap_surjective x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
x : ↥X
h :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) 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) (Scheme.Hom.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f 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) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
have h₁ : Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) 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) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
    (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
Tactic: rw [Scheme.Hom.stalkMap_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
⊢ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f
have h : IsEmbedding (X := ↥X) (Y := ↥Z) ⇑(f ≫ g)
Tactic: have h := (f ≫ g).isEmbedding
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsPreimmersion g
inst_1 : IsPreimmersion (f ≫ g)
h : IsEmbedding (X := ↥X) (Y := ↥Z) ⇑(f ≫ g)
⊢ IsEmbedding (X := ↥X) (Y := ↥Y) ⇑f
have rwa : IsEmbedding (X := ↥X) (Y := ↥Z) (Function.comp (β := ↥Y) ⇑g ⇑f)
Tactic: rwa [← g.isEmbedding.of_comp_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ IsPreimmersion (Spec.map f) ↔
    IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks
have rw : IsEmbedding (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f) ∧ SurjectiveOnStalks (Spec.map f) ↔
  IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ SurjectiveOnStalks (Spec.map f)
Tactic: rw [← HasRingHomProperty.Spec_iff (P := @SurjectiveOnStalks), isPreimmersion_iff, and_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (goal)
Goal:
⊢ IsStableUnderBaseChange @IsPreimmersion
have refine : ∀ (X Y Z : Scheme.{u_1}) (f : X ⟶ Z) (g : Y ⟶ Z) (x : HasPullback f g),
  IsPreimmersion g → IsPreimmersion (X := pullback f g) (pullback.fst f g)
Tactic: refine .mk' fun X Y Z f g _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
⊢ IsPreimmersion (X := pullback f g) (pullback.fst f g)
have this : SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)
Tactic: have := pullback_fst (P := @SurjectiveOnStalks) f g inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
this : SurjectiveOnStalks (X := pullback f g) (pullback.fst f g)
⊢ IsPreimmersion (X := pullback f g) (pullback.fst f g)
have isEmbedding : IsEmbedding (X := ↥(pullback f g)) (Y := ↥X) ⇑(pullback.fst f g)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Preimmersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
h : HasPullback f g
h_1 : IsPreimmersion g
this : 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) ⋯
⊢ IsEmbedding (X := ↥(pullback f g)) (Y := ↥X) ⇑(pullback.fst f g)
have this₁ : IsEmbedding L
Tactic: have : IsEmbedding L := IsEmbedding.of_comp (by fun_prop) continuous_subtype_val
    (SurjectiveOnStalks.isEmbedding_pullback f g)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
⊢ @IsProper = @IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType
have h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y), IsProper f ↔ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsProper f ↔ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f
have h : (IsSeparated f ∧ UniversallyClosed f) ∧ LocallyOfFiniteType f ↔
  (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f
Tactic: rw [isProper_iff, ← and_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsProper
have rw : (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).RespectsIso
Tactic: rw [isProper_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderComposition @IsProper
have rw : (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderComposition
Tactic: rw [isProper_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsMultiplicative @IsProper
have rw : (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsMultiplicative
Tactic: rw [isProper_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsProper
have rw : (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderBaseChange
Tactic: rw [isProper_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @IsProper
have rw : IsZariskiLocalAtTarget.{u_1} (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)
Tactic: rw [isProper_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (hypothesis)
Goal:
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
Tactic: have : (@IsAffineHom ⊓ @IsSeparated : MorphismProperty _) = @IsAffineHom :=
    inf_eq_left.mpr fun _ _ _ _ ↦ inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw : @IsFinite = @IsAffineHom ⊓ @IsProper
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
rw : @IsFinite = @IsAffineHom ⊓ @IsProper
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw₁ : @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
rw : @IsFinite = @IsAffineHom ⊓ @IsProper
rw₁ : @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw₂ : @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType))
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
rw : @IsFinite = @IsAffineHom ⊓ @IsProper
rw₁ : @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)
rw₂ : @IsFinite = @IsAffineHom ⊓ (@IsSeparated ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType))
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw₃ : @IsFinite = @IsAffineHom ⊓ @IsSeparated ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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)
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw₄ : @IsFinite = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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)
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw₅ : @IsIntegralHom ⊓ @LocallyOfFiniteType = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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)
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw₆ : @UniversallyClosed ⊓ @IsAffineHom ⊓ @LocallyOfFiniteType = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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)
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw₇ : @UniversallyClosed ⊓ (@IsAffineHom ⊓ @LocallyOfFiniteType) = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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)
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom
have rw₈ : @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType) = @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)
Tactic: rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
    IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsProper f ∧ IsAffineHom f
have rw : (@IsProper ⊓ @IsAffineHom) f ↔ IsProper f ∧ IsAffineHom f
Tactic: rw [eq_isProper_inf_isAffineHom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral
have this : CompactSpace.{u} ↥X
Tactic: have : CompactSpace X := (quasiCompact_iff_compactSpace f).mp inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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))
have rwa : UniversallyClosed (f ≫ Y.toSpecΓ)
Tactic: rwa [← Scheme.toSpecΓ_naturality,
      MorphismProperty.cancel_right_of_respectsIso (P := @UniversallyClosed)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsAffine Y
this : CompactSpace.{u} ↥X
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral
have this₁ : 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)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (hypothesis)
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))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral
have this₁ : UniversallyClosed X.toSpecΓ
Tactic: have : UniversallyClosed X.toSpecΓ := .of_comp_of_isSeparated _ (Spec.map f.appTop)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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Γ
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral
have rw : UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))
Tactic: rw [← IsIntegralHom.SpecMap_iff, IsIntegralHom.iff_universallyClosed_and_isAffineHom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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
have x : (Scheme.Hom.appTop f).hom'.IsIntegral
Tactic: apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (hypothesis)
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
⊢ IsField.{u} (↑Γ(X, ⊤) : Type u)
have this : (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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (hypothesis)
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
⊢ IsField.{u} (↑Γ(X, ⊤) : Type u)
have algebraizeInst : let algInst := (CommRingCat.Hom.hom F).toAlgebra;
Algebra.IsIntegral.{u, u} (↑(CommRingCat.of K) : Type u) (↑Γ(X, ⊤) : Type u)
Tactic: algebraize [F.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
have have : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
Tactic: have x : X := Nonempty.some inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
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
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
have obtain : ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)),
  (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