awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
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)
⊢ (∀ (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:
simp_rw [this, forall_and]

Premises used: forall_and
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
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
⊢ IsFinite f ↔ IsIntegralHom 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]

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, and_assoc, RingHom.finite_iff_isIntegral_and_finiteType
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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)).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:
and_congr_right fun ⟨_, _⟩ ↦
    (HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)).symm

Premises used: CommRingCat.Hom.hom, Set.Mem, Set.univ, RingHom.FiniteType, setOf, _private.0.AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType.match_1, AlgebraicGeometry.Scheme.Hom.appTop, and_congr_right, Iff, Set.preimage, AlgebraicGeometry.LocallyOfFiniteType, Iff.symm, AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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)).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:
refine and_congr_right fun ⟨_, _⟩ ↦
    (HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)).symm

Premises used: and_congr_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsFinite x_2 ↔ (@IsIntegralHom ⊓ @LocallyOfFiniteType) x_2
⊢ @IsFinite = @IsIntegralHom ⊓ @LocallyOfFiniteType

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsFinite x_2 ↔ (@IsIntegralHom ⊓ @LocallyOfFiniteType) x_2

Tactic:
IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _

Premises used: AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsFinite x_2 ↔ (@IsIntegralHom ⊓ @LocallyOfFiniteType) x_2

Tactic:
exact IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _

Premises used: AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsFinite f
⊢ IsIntegralHom f

Tactic:
((IsFinite.iff_isIntegralHom_and_locallyOfFiniteType f).mp ‹_›).1

Premises used: And.left, Iff.mp, AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsFinite f
⊢ LocallyOfFiniteType f

Tactic:
((IsFinite.iff_isIntegralHom_and_locallyOfFiniteType f).mp ‹_›).2

Premises used: And.right, Iff.mp, AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsClosedImmersion f ↔ IsFinite f ∧ Mono f
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Tactic:
wlog hY : IsAffine Y

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
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)
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

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]

Premises used: CategoryTheory.MorphismProperty.monomorphisms.iff, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
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)
⊢ (∀ (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:
simp_rw [this, forall_and]

Premises used: forall_and
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
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
⊢ IsClosedImmersion f ↔ IsFinite f ∧ 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]

Premises used: and_comm, RingHom.surjective_iff_epi_and_finite, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, and_assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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

Tactic:
and_congr_right fun ⟨_, _⟩ ↦
    Iff.trans ?_ (arrow_mk_iso_iff (monomorphisms _) (arrowIsoSpecΓOfIsAffine f).symm)

Premises used: AlgebraicGeometry.Scheme, CategoryTheory.Epi, CategoryTheory.Mono, CategoryTheory.MorphismProperty.monomorphisms, AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.arrowIsoSpecΓOfIsAffine, and_congr_right, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff, CategoryTheory.Iso.symm, Iff.trans, _private.0.AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono.match_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
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)))
⊢ (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:
refine and_congr_right fun ⟨_, _⟩ ↦
    Iff.trans ?_ (arrow_mk_iso_iff (monomorphisms _) (arrowIsoSpecΓOfIsAffine f).symm)

Premises used: and_congr_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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 ⊤))
trans₁ :
  Mono (X := Opposite.op Γ(X, f ⁻¹ᵁ ⊤)) (Quiver.Hom.op (Scheme.Hom.app f ⊤)) ↔
    monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))
⊢ Epi (Scheme.Hom.appTop f) ↔ monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))

Tactic:
trans Mono (f.app ⊤).op

Premises used: CategoryTheory.Mono, Quiver.Hom.op, AlgebraicGeometry.Scheme.Hom.app, Top.top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
h_1 : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left : IsAffine X
right : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
h : Mono (X := Opposite.op Γ(X, f ⁻¹ᵁ ⊤)) (Quiver.Hom.op (Scheme.Hom.app f ⊤))
⊢ Epi (X := Opposite.unop (Opposite.op Γ(Y, ⊤))) (Quiver.Hom.unop (Quiver.Hom.op (Scheme.Hom.app f ⊤)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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) ↔ Mono (X := Opposite.op Γ(X, f ⁻¹ᵁ ⊤)) (Quiver.Hom.op (Scheme.Hom.app f ⊤))

Tactic:
exact ⟨fun h ↦ inferInstance, fun h ↦ show Epi (f.app ⊤).op.unop by infer_instance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ Mono (X := Opposite.op Γ(X, f ⁻¹ᵁ ⊤)) (Quiver.Hom.op (Scheme.Hom.app f ⊤)) ↔
    monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))

Tactic:
(Functor.mono_map_iff_mono Scheme.Spec _).symm

Premises used: AlgebraicGeometry.Spec, Set.Mem, Set.univ, setOf, Quiver.Hom.unop, AlgebraicGeometry.Spec.map, AlgebraicGeometry.Scheme.Spec, Set.preimage, CategoryTheory.Functor.mono_map_iff_mono, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ Mono (X := Opposite.op Γ(X, f ⁻¹ᵁ ⊤)) (Quiver.Hom.op (Scheme.Hom.app f ⊤)) ↔
    monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))

Tactic:
exact (Functor.mono_map_iff_mono Scheme.Spec _).symm

Premises used: AlgebraicGeometry.Scheme.Spec, CategoryTheory.Functor.mono_map_iff_mono, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), IsClosedImmersion x_2 ↔ (@IsFinite ⊓ monomorphisms Scheme) x_2
⊢ @IsClosedImmersion = @IsFinite ⊓ monomorphisms Scheme

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsClosedImmersion x_2 ↔ (@IsFinite ⊓ monomorphisms Scheme) x_2

Tactic:
IsClosedImmersion.iff_isFinite_and_mono _

Premises used: AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ IsClosedImmersion x_2 ↔ (@IsFinite ⊓ monomorphisms Scheme) x_2

Tactic:
exact IsClosedImmersion.iff_isFinite_and_mono _

Premises used: AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
inst : IsClosedImmersion f
⊢ IsFinite f

Tactic:
((IsClosedImmersion.iff_isFinite_and_mono f).mp ‹_›).1

Premises used: AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono, And.left, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ HasOfPostcompProperty @IsFinite @IsSeparated

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

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

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

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

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

Premises used: inferInstance, Iff.intro, AlgebraicGeometry.IsFinite.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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)

Tactic:
HasAffineProperty.coprodDesc_affineAnd inferInstance RingHom.finite_respectsIso
    ?_ _ _ ‹_› ‹_›

Premises used: inferInstance, AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd, RingHom.finite_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
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
⊢ IsFinite (X := U ⨿ V) (Limits.coprod.desc f g)

Tactic:
refine HasAffineProperty.coprodDesc_affineAnd inferInstance RingHom.finite_respectsIso
    ?_ _ _ ‹_› ‹_›

Premises used: inferInstance, AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd, RingHom.finite_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ Module.Finite R S

Tactic:
algebraize [f, g]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
⊢ Module.Finite R T

Tactic:
algebraize [f, g]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R T := g.toAlgebra
algebraizeInst : Module.Finite R S
algebraizeInst_1 : Module.Finite R T
⊢ RingHom.Finite.{u, u} (A := R) (B := S × T) (f.prod g)

Tactic:
RingHom.finite_algebraMap.mpr inferInstance

Premises used: Iff.mpr, inferInstance, RingHom.finite_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R T := g.toAlgebra
algebraizeInst : Module.Finite R S
algebraizeInst_1 : Module.Finite R T
⊢ RingHom.Finite.{u, u} (A := R) (B := S × T) (f.prod g)

Tactic:
refine RingHom.finite_algebraMap.mpr inferInstance

Premises used: Iff.mpr, inferInstance, RingHom.finite_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsFinite f
⊢ (CommRingCat.Hom.hom (appTop f)).Finite

Tactic:
(HasAffineProperty.iff_of_isAffine (P := @IsFinite).mp inferInstance).2

Premises used: inferInstance, And.right, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
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
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
wlog hY : ∃ S, Y = Spec S generalizing X Y
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
inst_2 : JacobsonSpace.{u} ↥Y
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
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),
      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)
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥X
inst_1 : IsReduced X
inst_2 : JacobsonSpace.{u} ↥Y
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
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    Subsingleton.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)

Tactic:
have inst (i) := ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding.injective.subsingleton