awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
φ : R ⟶ S
h : P' (Spec.map φ)
Y : CommRingCat
g : Spec Y ⟶ Spec R
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this : IsAffine.{u} (Spec Y)
⊢ ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)

Tactic:
simp [SpecMap_iff_of_affineAnd _ hQ]

Premises used: AlgebraicGeometry.HasAffineProperty.SpecMap_iff_of_affineAnd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    Etale f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale) f
⊢ @Etale = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ {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) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale) f
h₁ h₂ :
  (∀ {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)).Etale
⊢ Etale f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale) f

Tactic:
rw [etale_iff, affineLocally_iff_forall_isAffineOpen]

Premises used: AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.etale_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsMultiplicative @Etale

Tactic:
HasRingHomProperty.isMultiplicative RingHom.Etale.stableUnderComposition
    RingHom.Etale.containsIdentities

Premises used: RingHom.Etale.stableUnderComposition, AlgebraicGeometry.HasRingHomProperty.isMultiplicative, RingHom.Etale.containsIdentities
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
inst : Etale f
inst_1 : Etale g
⊢ Etale (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ f g ‹Etale f› ‹Etale g›

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderBaseChange @Etale

Tactic:
HasRingHomProperty.isStableUnderBaseChange RingHom.Etale.isStableUnderBaseChange

Premises used: RingHom.Etale.isStableUnderBaseChange, AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ Etale f

Tactic:
HasRingHomProperty.of_isOpenImmersion RingHom.Etale.containsIdentities

Premises used: AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion, RingHom.Etale.containsIdentities
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : Etale g
⊢ Etale (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : Etale f
⊢ Etale (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g inferInstance

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

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f_1 f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : Etale f
⊢ Etale (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
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
⊢ @Etale = @SmoothOfRelativeDimension 0

Tactic:
apply HasRingHomProperty.ext

Premises used: AlgebraicGeometry.HasRingHomProperty.ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
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
⊢ @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
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:
apply RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero

Premises used: RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0

Tactic:
have : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0 := by
    ext; apply RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
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
h₁ : RingHom.OfLocalizationSpanTarget.{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

Tactic:
rw [← this, RingHom.locally_iff_of_localizationSpanTarget]

Premises used: RingHom.locally_iff_of_localizationSpanTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale

Tactic:
RingHom.Etale.respectsIso

Premises used: RingHom.Etale.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale

Tactic:
exact RingHom.Etale.respectsIso

Premises used: RingHom.Etale.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ RingHom.OfLocalizationSpanTarget.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale

Tactic:
RingHom.Etale.ofLocalizationSpanTarget

Premises used: RingHom.Etale.ofLocalizationSpanTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ RingHom.OfLocalizationSpanTarget.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale

Tactic:
exact RingHom.Etale.ofLocalizationSpanTarget

Premises used: RingHom.Etale.ofLocalizationSpanTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
rw rw₁ : SmoothOfRelativeDimension 0 f ↔ SmoothOfRelativeDimension 0 f
⊢ Etale f ↔ SmoothOfRelativeDimension 0 f

Tactic:
rw [eq_smoothOfRelativeDimension_zero]

Premises used: AlgebraicGeometry.Etale.eq_smoothOfRelativeDimension_zero
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
inst rwa rwa₁ rwa₂ rwa₃ : Etale f
⊢ SmoothOfRelativeDimension 0 f

Tactic:
rwa [← iff_smoothOfRelativeDimension_zero]

Premises used: AlgebraicGeometry.Etale.iff_smoothOfRelativeDimension_zero
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Etale f
⊢ Smooth f

Tactic:
SmoothOfRelativeDimension.smooth 0 f

Premises used: AlgebraicGeometry.SmoothOfRelativeDimension.smooth, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
rw : @LocallyOfFiniteType ⊓ @FormallyUnramified ≤ diagonal @Etale
⊢ HasOfPostcompProperty (@Etale) (@LocallyOfFiniteType ⊓ @FormallyUnramified)

Tactic:
rw [MorphismProperty.hasOfPostcompProperty_iff_le_diagonal]

Premises used: CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
this : ∀ (hft : LocallyOfFiniteType f) (hfu : FormallyUnramified f), diagonal (@Etale) f
⊢ (@LocallyOfFiniteType ⊓ @FormallyUnramified) f → diagonal (@Etale) f

Tactic:
⟨hft, hfu⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hft : LocallyOfFiniteType f
hfu : FormallyUnramified f
⊢ diagonal (@Etale) f

Tactic:
inferInstanceAs <| Etale (pullback.diagonal f)

Premises used: AlgebraicGeometry.Etale.instOfIsOpenImmersion, CategoryTheory.MorphismProperty.diagonal, CategoryTheory.Limits.pullback.diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hft : LocallyOfFiniteType f
hfu : FormallyUnramified f
⊢ diagonal (@Etale) f

Tactic:
exact inferInstanceAs <| Etale (pullback.diagonal f)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
inst : Etale (f ≫ g)
inst_1 : LocallyOfFiniteType g
inst_2 : FormallyUnramified g
⊢ Etale f

Tactic:
of_postcomp _ (W' := @LocallyOfFiniteType ⊓ @FormallyUnramified) f g ⟨‹_›, ‹_›⟩ ‹_›

Premises used: And.intro, CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
apply : @Etale ≤ @LocallyOfFiniteType ⊓ @FormallyUnramified
⊢ HasOfPostcompProperty @Etale @Etale

Tactic:
apply MorphismProperty.HasOfPostcompProperty.of_le (W := @Etale)
    (Q := (@LocallyOfFiniteType ⊓ @FormallyUnramified))

Premises used: CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_le, AlgebraicGeometry.FormallyUnramified, AlgebraicGeometry.LocallyOfFiniteType, AlgebraicGeometry.Etale, Min.min
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : Etale f
left : LocallyOfFiniteType f
right : FormallyUnramified f
⊢ (@LocallyOfFiniteType ⊓ @FormallyUnramified) f

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ LocallyOfFiniteType f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ FormallyUnramified f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
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
⊢ Etale f ↔ Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f

Tactic:
rw [etale_iff, flat_iff, formallyUnramified_iff, locallyOfFinitePresentation_iff]

Premises used: AlgebraicGeometry.formallyUnramified_iff, AlgebraicGeometry.etale_iff, AlgebraicGeometry.locallyOfFinitePresentation_iff, AlgebraicGeometry.flat_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {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:
grind [RingHom.Etale.iff_flat_and_formallyUnramified]

Premises used: RingHom.Etale.iff_flat_and_formallyUnramified
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : FormallyUnramified f
inst_2 : LocallyOfFinitePresentation f
rw : Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f
⊢ Etale f

Tactic:
rw [Etale.iff_flat_and_formallyUnramified]

Premises used: AlgebraicGeometry.Etale.iff_flat_and_formallyUnramified
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : FormallyUnramified f
inst_2 : LocallyOfFinitePresentation f
⊢ Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f

Tactic:
⟨inferInstance, inferInstance, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : FormallyUnramified f
inst_2 : LocallyOfFinitePresentation f
⊢ Flat f ∧ FormallyUnramified f ∧ LocallyOfFinitePresentation f

Tactic:
exact ⟨inferInstance, inferInstance, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Etale
Goal:
X : Scheme
Y : X.Etale
⊢ Etale Y.toComma (P := @Etale) (Q := ⊤) (W := ⊤).hom

Tactic:
Y.prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
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
⊢ HasAffineProperty (@IsFinite) (affineAnd fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Finite)

Tactic:
rw [HasAffineProperty.affineAnd_iff _ RingHom.finite_respectsIso
    RingHom.finite_localizationPreserves.away RingHom.finite_ofLocalizationSpan]

Premises used: RingHom.finite_localizationPreserves, RingHom.finite_respectsIso, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, RingHom.finite_ofLocalizationSpan, RingHom.LocalizationPreserves.away
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
⊢ ∀ {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:
simp [isFinite_iff]

Premises used: AlgebraicGeometry.isFinite_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
⊢ IsStableUnderComposition @IsFinite

Tactic:
HasAffineProperty.affineAnd_isStableUnderComposition inferInstance
    RingHom.finite_stableUnderComposition

Premises used: AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition, inferInstance, RingHom.finite_stableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
⊢ IsStableUnderBaseChange @IsFinite

Tactic:
HasAffineProperty.affineAnd_isStableUnderBaseChange inferInstance
    RingHom.finite_respectsIso RingHom.finite_isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange, inferInstance, RingHom.finite_respectsIso, RingHom.finite_isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
⊢ ContainsIdentities @IsFinite

Tactic:
HasAffineProperty.affineAnd_containsIdentities inferInstance
    RingHom.finite_respectsIso RingHom.finite_containsIdentities

Premises used: inferInstance, RingHom.finite_respectsIso, RingHom.finite_containsIdentities, AlgebraicGeometry.HasAffineProperty.affineAnd_containsIdentities
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ IsAffine.{u} (Spec S)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
rw₂ rw₃ :
  (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite
⊢ IsFinite (Spec.map f) ↔ (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)]

Premises used: and_iff_right, RingHom.finite_respectsIso, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, AlgebraicGeometry.arrowIsoΓSpecOfIsAffine, RingHom.RespectsIso.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ IsFinite f

Tactic:
of_isIso @IsFinite f

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

Tactic:
IsStableUnderComposition.comp_mem f g ‹IsFinite f› ‹IsFinite g›

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : IsFinite g
⊢ IsFinite (X := Limits.pullback f g) (Limits.pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst _ _ inferInstance

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

Tactic:
MorphismProperty.pullback_snd _ _ inferInstance

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

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Finite
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
wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsAffine Y), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType 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), IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType 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)) ↔
    (∀ (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)
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

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]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover