awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.snd (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f_1 f g : X ⟶ Y
⊢ IsImmersion (X := equalizer f g) (equalizer.ι f g)

Tactic:
MorphismProperty.of_isPullback (P := @IsImmersion)
    (isPullback_equalizer_prod f g).flip inferInstance

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.isPullback_equalizer_prod, inferInstance, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
⊢ IsImmersion (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
⊢ Hom.liftCoborder f ≫ (Hom.coborderRange f).ι = Hom.toImage f ≫ Hom.imageι f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
refine : (Hom.ker (Hom.imageι f)).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
⊢ IsPullback (Hom.toImage f) (Hom.liftCoborder f) (Hom.imageι f) (Hom.coborderRange f).ι

Tactic:
refine (isPullback_of_isClosedImmersion _ _ _ _ (by simp) ?_).flip

Premises used: CategoryTheory.IsPullback.flip, AlgebraicGeometry.isPullback_of_isClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
rw : (Hom.ker f).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)
⊢ (Hom.ker (Hom.imageι f)).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)

Tactic:
rw [Hom.imageι, IdealSheafData.ker_subschemeι]

Premises used: AlgebraicGeometry.Scheme.Hom.imageι, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
h :
  ∀ (U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)),
    ((Hom.ker f).comap (Hom.coborderRange f).ι).ideal U = IdealSheafData.ideal (Hom.ker (Hom.liftCoborder f)) U
⊢ (Hom.ker f).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)

Tactic:
ext U : 2
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
h :
  Eq (α := Ideal (↑Γ((↑(Hom.coborderRange f) : Scheme), (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (RingHom.ker
      (CommRingCat.Hom.hom
        (𝟙 Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) ≫
          Hom.app f ((Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)))))
    (RingHom.ker (F :=
      (↑Γ((↑(Hom.coborderRange f) : Scheme), (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
⊢ ((Hom.ker f).comap (Hom.coborderRange f).ι).ideal U = IdealSheafData.ideal (Hom.ker (Hom.liftCoborder f)) U

Tactic:
simp only [IdealSheafData.ideal_comap_of_isOpenImmersion, Opens.ι_appIso, Iso.refl_inv,
    Hom.ker_apply, RingHom.comap_ker, ← CommRingCat.hom_comp]

Premises used: RingHom.comap_ker, AlgebraicGeometry.Scheme.Hom.ker_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.Opens.ι_appIso, CategoryTheory.Iso.refl_inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
h :
  Eq (α := Ideal (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (RingHom.ker (F :=
      (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (RingHom.comp
        (CommRingCat.Hom.hom (Hom.app f ((Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
        (RingHom.id (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))))
    (RingHom.ker (F :=
      (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
⊢ Eq (α := Ideal (↑Γ((↑(Hom.coborderRange f) : Scheme), (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (RingHom.ker
      (CommRingCat.Hom.hom
        (𝟙 Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) ≫
          Hom.app f ((Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)))))
    (RingHom.ker (F :=
      (↑Γ((↑(Hom.coborderRange f) : Scheme), (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))

Tactic:
dsimp [Opens.toScheme_presheaf_obj]

Premises used: AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
h :
  Function.Injective (α :=
    (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u)) (β :=
    (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) :
      (a : (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u)) →
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
⊢ Eq (α := Ideal (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (RingHom.ker (F :=
      (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (RingHom.comp
        (CommRingCat.Hom.hom (Hom.app f ((Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))
        (RingHom.id (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))))
    (RingHom.ker (F :=
      (↑Γ(Y, (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u) →+*
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
      (CommRingCat.Hom.hom (Hom.app (Hom.liftCoborder f) (↑U : (↑(Hom.coborderRange f) : Scheme).Opens))))

Tactic:
rw [RingHomCompTriple.comp_eq, liftCoborder_app,
    CommRingCat.hom_comp, RingHom.ker_comp_of_injective]

Premises used: RingHomCompTriple.comp_eq, AlgebraicGeometry.liftCoborder_app, CommRingCat.hom_comp, RingHom.ker_comp_of_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
h : Mono (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Function.Injective (α :=
    (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u)) (β :=
    (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))
    (⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) :
      (a : (↑Γ(X, f ⁻¹ᵁ (Hom.coborderRange f).ι ''ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u)) →
        (↑Γ(X, Hom.liftCoborder f ⁻¹ᵁ (↑U : (↑(Hom.coborderRange f) : Scheme).Opens)) : Type u))

Tactic:
rw [← ConcreteCategory.mono_iff_injective_of_preservesPullback]

Premises used: CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
U : (↑(↑(Hom.coborderRange f) : Scheme).affineOpens : Type u)
⊢ Mono (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : QuasiCompact f
⊢ IsOpenImmersion (Scheme.Hom.toImage f)

Tactic:
MorphismProperty.of_isPullback (IsImmersion.isPullback_toImage_liftCoborder f).flip inferInstance

Premises used: CategoryTheory.MorphismProperty.of_isPullback, AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, inferInstance, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ IsImmersion f ↔ ∃ (Z : Scheme.{u}) (g₁ : X ⟶ Z) (g₂ : Z ⟶ Y), IsOpenImmersion g₁ ∧ IsClosedImmersion g₂ ∧ g₁ ≫ g₂ = f

Tactic:
⟨fun _ ↦ ⟨_, f.toImage, f.imageι, inferInstance, inferInstance, f.toImage_imageι⟩,
    fun ⟨_, _, _, _, _, e⟩ ↦ e ▸ inferInstance⟩

Premises used: AlgebraicGeometry.Scheme.Hom.image, AlgebraicGeometry.Scheme.Hom.imageι, AlgebraicGeometry.Scheme.Hom.toImage_imageι, AlgebraicGeometry.Scheme.Hom.toImage, Eq.rec, inferInstance, AlgebraicGeometry.IsImmersion, And.intro, Iff.intro, Exists.intro, _private.0.AlgebraicGeometry.IsImmersion.isImmersion_iff_exists_of_quasiCompact.match_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y Z S : Scheme
rw :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y),
    IsIntegralHom f ↔
      IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral
⊢ HasAffineProperty (@IsIntegralHom) (affineAnd fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.IsIntegral)

Tactic:
rw [HasAffineProperty.affineAnd_iff _ RingHom.isIntegral_respectsIso
    RingHom.isIntegral_isStableUnderBaseChange.localizationPreserves.away
    RingHom.isIntegral_ofLocalizationSpan]

Premises used: RingHom.isIntegral_respectsIso, RingHom.isIntegral_isStableUnderBaseChange, RingHom.isIntegral_ofLocalizationSpan, RingHom.IsStableUnderBaseChange.localizationPreserves, AlgebraicGeometry.HasAffineProperty.affineAnd_iff, RingHom.LocalizationPreserves.away
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y Z S : Scheme
⊢ ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y),
    IsIntegralHom f ↔
      IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral

Tactic:
simp [isIntegralHom_iff]

Premises used: AlgebraicGeometry.isIntegralHom_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y Z S : Scheme
⊢ IsStableUnderComposition @IsIntegralHom

Tactic:
HasAffineProperty.affineAnd_isStableUnderComposition (Q := RingHom.IsIntegral) hasAffineProperty
    RingHom.isIntegral_stableUnderComposition

Premises used: AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition, AlgebraicGeometry.IsIntegralHom.hasAffineProperty, RingHom.isIntegral_stableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y Z S : Scheme
⊢ IsStableUnderBaseChange @IsIntegralHom

Tactic:
HasAffineProperty.affineAnd_isStableUnderBaseChange (Q := RingHom.IsIntegral) hasAffineProperty
    RingHom.isIntegral_respectsIso RingHom.isIntegral_isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange, RingHom.isIntegral_respectsIso, RingHom.isIntegral_isStableUnderBaseChange, AlgebraicGeometry.IsIntegralHom.hasAffineProperty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIntegralHom f
inst_1 : IsIntegralHom g
⊢ IsIntegralHom (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ _ _ ‹_› ‹_›

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

Tactic:
MorphismProperty.pullback_fst f g inferInstance

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

Tactic:
MorphismProperty.pullback_snd f g inferInstance

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

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y Z S : Scheme
⊢ HasOfPostcompProperty @IsIntegralHom @IsSeparated

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

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

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

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

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

Premises used: inferInstance, AlgebraicGeometry.IsIntegralHom.of_comp, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
⊢ (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral).RespectsIso

Tactic:
have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral).RespectsIso
rw :
  RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type u_1)) (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)) ↔
    (CommRingCat.Hom.hom φ).IsIntegral
rw₁ : IsAffine.{u_1} (Spec S)
⊢ IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom), and_iff_right]

Premises used: and_iff_right, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral).RespectsIso
⊢ RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type u_1)) (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)) ↔
    (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
    (arrowIsoΓSpecOfIsAffine φ).symm

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, CategoryTheory.Iso.symm, RingHom.IsIntegral, AlgebraicGeometry.arrowIsoΓSpecOfIsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral).RespectsIso
⊢ IsAffine.{u_1} (Spec S)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
R S : CommRingCat
φ : R ⟶ S
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦ f.IsIntegral).RespectsIso
⊢ RingHom.IsIntegral (R := (↑Γ(Spec R, ⊤) : Type u_1)) (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)) ↔
    (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
exacts [MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
    (arrowIsoΓSpecOfIsAffine φ).symm, inferInstance]

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, CategoryTheory.Iso.symm, RingHom.IsIntegral, AlgebraicGeometry.arrowIsoΓSpecOfIsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X_1 Y Z S U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsIntegralHom f
inst_1 : IsIntegralHom g
⊢ IsIntegralHom (X := U ⨿ V) (Limits.coprod.desc f g)

Tactic:
hasAffineProperty.coprodDesc_affineAnd RingHom.isIntegral_respectsIso ?_ _ _ ‹_› ‹_›

Premises used: RingHom.isIntegral_respectsIso, AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X_1 Y Z S U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsIntegralHom f
inst_1 : IsIntegralHom 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.IsIntegral → g.IsIntegral → (f.prod g).IsIntegral
⊢ IsIntegralHom (X := U ⨿ V) (Limits.coprod.desc f g)

Tactic:
refine hasAffineProperty.coprodDesc_affineAnd RingHom.isIntegral_respectsIso ?_ _ _ ‹_› ‹_›

Premises used: RingHom.isIntegral_respectsIso, AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X_1 Y Z S_1 U V X : Scheme
f_1 : U ⟶ X
g_1 : V ⟶ X
inst : IsIntegralHom f_1
inst_1 : IsIntegralHom 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.IsIntegral
h_1 : g.IsIntegral
⊢ let algInst := f.toAlgebra;
  Algebra.IsIntegral R S

Tactic:
algebraize [f, g]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X_1 Y Z S_1 U V X : Scheme
f_1 : U ⟶ X
g_1 : V ⟶ X
inst : IsIntegralHom f_1
inst_1 : IsIntegralHom 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.IsIntegral
h_1 : g.IsIntegral
algebraizeInst :
  let algInst := f.toAlgebra;
  Algebra.IsIntegral R S
⊢ let algInst := g.toAlgebra;
  Algebra.IsIntegral R T

Tactic:
algebraize [f, g]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X_1 Y Z S_1 U V X : Scheme
f_1 : U ⟶ X
g_1 : V ⟶ X
inst : IsIntegralHom f_1
inst_1 : IsIntegralHom 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.IsIntegral
h_1 : g.IsIntegral
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R T := g.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
algebraizeInst_1 : Algebra.IsIntegral R T
⊢ RingHom.IsIntegral.{u, u} (R := R) (A := S × T) (f.prod g)

Tactic:
algebraMap_isIntegral_iff.mpr inferInstance

Premises used: Iff.mpr, algebraMap_isIntegral_iff, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X_1 Y Z S_1 U V X : Scheme
f_1 : U ⟶ X
g_1 : V ⟶ X
inst : IsIntegralHom f_1
inst_1 : IsIntegralHom 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.IsIntegral
h_1 : g.IsIntegral
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra R T := g.toAlgebra
algebraizeInst : Algebra.IsIntegral R S
algebraizeInst_1 : Algebra.IsIntegral R T
⊢ RingHom.IsIntegral.{u, u} (R := R) (A := S × T) (f.prod g)

Tactic:
refine algebraMap_isIntegral_iff.mpr inferInstance

Premises used: Iff.mpr, algebraMap_isIntegral_iff, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
X Y Z S : Scheme
f : X ⟶ Y
inst : IsIntegralHom f
revert : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f], UniversallyClosed f
⊢ UniversallyClosed f

Tactic:
revert X Y f ‹IsIntegralHom f›

Premises used: AlgebraicGeometry.IsIntegralHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S : Scheme
rw : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [universally (@IsIntegralHom) f], (topologically @IsClosedMap).universally f
⊢ ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f], UniversallyClosed f

Tactic:
rw [universallyClosed_eq, ← IsStableUnderBaseChange.universally_eq (P := @IsIntegralHom)]

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq, AlgebraicGeometry.universallyClosed_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S : Scheme
a : @IsIntegralHom ≤ topologically @IsClosedMap
⊢ ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [universally (@IsIntegralHom) f], (topologically @IsClosedMap).universally f

Tactic:
apply universally_mono

Premises used: CategoryTheory.MorphismProperty.universally_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X Y : Scheme
f : X ⟶ Y
a :
  ∀
    (this :
      ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        IsIntegralHom f → topologically (@IsClosedMap) f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIntegralHom f → topologically (@IsClosedMap) f
wlog :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIntegralHom f → topologically (@IsClosedMap) f
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
wlog hY : ∃ R, Y = Spec R generalizing X Y
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Integral
Goal:
Z S X Y : Scheme
f : X ⟶ Y
this :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIntegralHom f → topologically (@IsClosedMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
a :
  (∀ (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),
      topologically @IsClosedMap (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)
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := topologically _) Y.affineCover]

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