awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
⊢ @Etale = @SmoothOfRelativeDimension 0
have h : ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.Etale ↔
    RingHom.Locally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.IsStandardSmoothOfRelativeDimension 0) f
Tactic: apply HasRingHomProperty.ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
have h : ∀ (x x_1 : Type u_1) (x_2 : CommRing x) (x_3 : CommRing x_1) (x_4 : x →+* x_1),
  x_4.Etale ↔ RingHom.IsStandardSmoothOfRelativeDimension 0 x_4
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (hypothesis)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ f.Etale ↔
    RingHom.Locally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.IsStandardSmoothOfRelativeDimension 0) f
have this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
Tactic: have : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0 := by
    ext; apply RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ f.Etale ↔
    RingHom.Locally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.IsStandardSmoothOfRelativeDimension 0) f
have h : RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale
Tactic: rw [← this, RingHom.locally_iff_of_localizationSpanTarget]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
h : RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale
⊢ f.Etale ↔
    RingHom.Locally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.IsStandardSmoothOfRelativeDimension 0) f
have h₁ : RingHom.OfLocalizationSpanTarget.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale
Tactic: rw [← this, RingHom.locally_iff_of_localizationSpanTarget]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Etale f ↔ SmoothOfRelativeDimension 0 f
have rw : SmoothOfRelativeDimension 0 f ↔ SmoothOfRelativeDimension 0 f
Tactic: rw [eq_smoothOfRelativeDimension_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ HasOfPostcompProperty (@Etale) (@LocallyOfFiniteType ⊓ @FormallyUnramified)
have rw : @LocallyOfFiniteType ⊓ @FormallyUnramified ≤ diagonal @Etale
Tactic: rw [MorphismProperty.hasOfPostcompProperty_iff_le_diagonal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ (@LocallyOfFiniteType ⊓ @FormallyUnramified) f → diagonal (@Etale) f
have this : ∀ (hft : LocallyOfFiniteType f) (hfu : FormallyUnramified f), diagonal (@Etale) f
Tactic: ⟨hft, hfu⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ HasOfPostcompProperty @Etale @Etale
have apply : @Etale ≤ @LocallyOfFiniteType ⊓ @FormallyUnramified
Tactic: apply MorphismProperty.HasOfPostcompProperty.of_le (W := @Etale)
    (Q := (@LocallyOfFiniteType ⊓ @FormallyUnramified))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ (@LocallyOfFiniteType ⊓ @FormallyUnramified) f
have left : LocallyOfFiniteType f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : Etale f
left : LocallyOfFiniteType f
⊢ (@LocallyOfFiniteType ⊓ @FormallyUnramified) f
have right : FormallyUnramified f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Etale f ↔ Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f
have rw : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale) ↔
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ∧
    (∀ {U : Y.Opens},
        IsAffineOpen U →
          ∀ {V : X.Opens},
            IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified) ∧
      ∀ {U : Y.Opens},
        IsAffineOpen U →
          ∀ {V : X.Opens},
            IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FinitePresentation
Tactic: rw [etale_iff, flat_iff, formallyUnramified_iff, locallyOfFinitePresentation_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : FormallyUnramified f
inst_2 : LocallyOfFinitePresentation f
⊢ Etale f
have rw : Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f
Tactic: rw [Etale.iff_flat_and_formallyUnramified]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
⊢ HasAffineProperty (@IsFinite) (affineAnd fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Finite)
have rw : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y),
  IsFinite f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite
Tactic: rw [HasAffineProperty.affineAnd_iff _ RingHom.finite_respectsIso
    RingHom.finite_localizationPreserves.away RingHom.finite_ofLocalizationSpan]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ IsFinite (Spec.map f) ↔ (CommRingCat.Hom.hom f).Finite
have rw : IsAffine.{u} (Spec S) ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔ (CommRingCat.Hom.hom f).Finite
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite), and_iff_right (by infer_instance),
    RingHom.finite_respectsIso.arrow_mk_iso_iff (arrowIsoΓSpecOfIsAffine f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
rw :
  IsAffine.{u} (Spec S) ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔ (CommRingCat.Hom.hom f).Finite
⊢ IsFinite (Spec.map f) ↔ (CommRingCat.Hom.hom f).Finite
have rw₁ : (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔ (CommRingCat.Hom.hom f).Finite
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite), and_iff_right (by infer_instance),
    RingHom.finite_respectsIso.arrow_mk_iso_iff (arrowIsoΓSpecOfIsAffine f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
rw :
  IsAffine.{u} (Spec S) ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔ (CommRingCat.Hom.hom f).Finite
rw₁ : (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔ (CommRingCat.Hom.hom f).Finite
⊢ IsFinite (Spec.map f) ↔ (CommRingCat.Hom.hom f).Finite
have rw₂ : (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔
  (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite), and_iff_right (by infer_instance),
    RingHom.finite_respectsIso.arrow_mk_iso_iff (arrowIsoΓSpecOfIsAffine f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
have inr : ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
  (hY : ¬IsAffine Y), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
Tactic: wlog hY : IsAffine Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inr :
  ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
    (hY : ¬IsAffine Y), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
Tactic: wlog hY : IsAffine Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
hY : ¬IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
have inr : (∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsFinite (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),
      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),
      LocallyOfFiniteType (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 := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsFinite (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),
        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),
        LocallyOfFiniteType (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)
have 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) ∧
      LocallyOfFiniteType (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),
      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),
      LocallyOfFiniteType (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: simp_rw [this, forall_and]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
have rw : (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FiniteType ↔
  (IsAffine X ∧ RingHom.IsIntegral (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤))) ∧
    LocallyOfFiniteType f
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite),
    HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom),
    RingHom.finite_iff_isIntegral_and_finiteType, ← and_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
⊢ @IsFinite = @IsIntegralHom ⊓ @LocallyOfFiniteType
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsFinite x_2 ↔ (@IsIntegralHom ⊓ @LocallyOfFiniteType) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f
have inr : ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
  (hY : ¬IsAffine Y), IsClosedImmersion f ↔ IsFinite f ∧ Mono f
Tactic: wlog hY : IsAffine Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inr :
  ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
    (hY : ¬IsAffine Y), IsClosedImmersion f ↔ IsFinite f ∧ Mono f
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsClosedImmersion f ↔ IsFinite f ∧ Mono f
Tactic: wlog hY : IsAffine Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsClosedImmersion f ↔ IsFinite f ∧ Mono f
hY : ¬IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f
have inr : (∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsClosedImmersion (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),
      IsFinite (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),
      monomorphisms Scheme (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 [← monomorphisms.iff, IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := monomorphisms _) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsClosedImmersion f ↔ IsFinite f ∧ Mono f
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1),
      IsClosedImmersion (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),
        IsFinite (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),
        monomorphisms Scheme (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)
have inr : (∀ (i : Y.affineCover.toPreZeroHypercover.1),
    IsFinite (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) ∧
      Mono (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),
      IsFinite (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),
      monomorphisms Scheme (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: simp_rw [this, forall_and]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f
have rw : (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Epi (Scheme.Hom.appTop f) ↔
  (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @IsClosedImmersion),
    HasAffineProperty.iff_of_isAffine (P := @IsFinite),
    RingHom.surjective_iff_epi_and_finite, @and_comm (Epi _), ← and_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Epi (Scheme.Hom.appTop f) ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f
have refine : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite →
  IsAffine X →
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite →
      (Epi (Scheme.Hom.appTop f) ↔ monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f)))
Tactic: refine and_congr_right fun ⟨_, _⟩ ↦
    Iff.trans ?_ (arrow_mk_iso_iff (monomorphisms _) (arrowIsoSpecΓOfIsAffine f).symm)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
h : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left : IsAffine X
right : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ Epi (Scheme.Hom.appTop f) ↔ monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))
have trans : Epi (Scheme.Hom.appTop f) ↔ Mono (X := Opposite.op Γ(X, f ⁻¹ᵁ ⊤)) (Quiver.Hom.op (Scheme.Hom.app f ⊤))
Tactic: trans Mono (f.app ⊤).op
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
h : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left : IsAffine X
right : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
trans : Epi (Scheme.Hom.appTop f) ↔ Mono (X := Opposite.op Γ(X, f ⁻¹ᵁ ⊤)) (Quiver.Hom.op (Scheme.Hom.app f ⊤))
⊢ Epi (Scheme.Hom.appTop f) ↔ monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))
have trans₁ : Mono (X := Opposite.op Γ(X, f ⁻¹ᵁ ⊤)) (Quiver.Hom.op (Scheme.Hom.app f ⊤)) ↔
  monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))
Tactic: trans Mono (f.app ⊤).op
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
⊢ @IsClosedImmersion = @IsFinite ⊓ monomorphisms Scheme
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsClosedImmersion x_2 ↔ (@IsFinite ⊓ monomorphisms Scheme) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsFinite f
inst_1 : IsFinite g
⊢ IsFinite (X := U ⨿ V) (Limits.coprod.desc f g)
have refine : ∀ {R S T : Type u} [inst : CommRing R] [inst_2 : CommRing S] [inst_3 : CommRing T] (f : R →+* S) (g : R →+* T),
  f.Finite → g.Finite → (f.prod g).Finite
Tactic: refine HasAffineProperty.coprodDesc_affineAnd inferInstance RingHom.finite_respectsIso
    ?_ _ _ ‹_› ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
U V X : Scheme
f_2 : U ⟶ X
g_1 : V ⟶ X
inst : IsFinite f_2
inst_1 : IsFinite g_1
R S T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
f : R →+* S
g : R →+* T
h : f.Finite
h_1 : g.Finite
⊢ RingHom.Finite.{u, u} (A := R) (B := S × T) (f.prod g)
have algebraizeInst : Module.Finite R S
Tactic: algebraize [f, g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (hypothesis)
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
U V X : Scheme
f_2 : U ⟶ X
g_1 : V ⟶ X
inst : IsFinite f_2
inst_1 : IsFinite g_1
R S T : Type u
inst_2 : CommRing R
inst_3 : CommRing S
inst_4 : CommRing T
f : R →+* S
g : R →+* T
h : f.Finite
h_1 : g.Finite
algebraizeInst : Module.Finite R S
⊢ RingHom.Finite.{u, u} (A := R) (B := S × T) (f.prod g)
have algebraizeInst₁ : Module.Finite R T
Tactic: algebraize [f, g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
inst_2 : JacobsonSpace.{u} ↥Y
⊢ IsFinite f ↔ LocallyOfFiniteType f
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [Subsingleton.{u + 1} ↥X] [IsReduced X] [JacobsonSpace.{u} ↥Y]
      (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f)
  (hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f
Tactic: wlog hY : ∃ S, Y = Spec S generalizing X Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Finite (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
inst_2 : JacobsonSpace.{u} ↥Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [Subsingleton.{u + 1} ↥X] [IsReduced X] [JacobsonSpace.{u} ↥Y]
        (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f)
    (hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f
⊢ IsFinite f ↔ LocallyOfFiniteType f
have wlog : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} [Subsingleton.{u + 1} ↥X] [IsReduced X] [JacobsonSpace.{u} ↥Y]
  (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsFinite f ↔ LocallyOfFiniteType f
Tactic: wlog hY : ∃ S, Y = Spec S generalizing X Y
Cleared hypotheses: X, Y, f, inst, inst_1, inst_2