awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X_1 Y_1 Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
    IsAffine X ∧
      Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
ha : IsAffine Y
hsurj :
  Function.Surjective (α := (↑Γ(S, ⊤) : Type u_1)) (β := (↑Γ(Y, ⊤) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop g)) :
      (a : (↑Γ(S, ⊤) : Type u_1)) → (↑Γ(Y, ⊤) : Type u_1))
⊢ IsAffine.{u_1} (Limits.pullback f g) ∧
    Function.Surjective (α := (↑Γ(X, ⊤) : Type u_1)) (β := (↑Γ(Limits.pullback f g, ⊤) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := Γ(Limits.pullback f g, ⊤)) (Scheme.Hom.appTop (Limits.pullback.fst f g))) :
        (a : (↑Γ(X, ⊤) : Type u_1)) → (↑Γ(Limits.pullback f g, ⊤) : Type u_1))

Tactic:
⟨inferInstance, RingHom.surjective_isStableUnderBaseChange.pullback_fst_appTop _
    RingHom.surjective_respectsIso f _ hsurj⟩

Premises used: RingHom.IsStableUnderBaseChange.pullback_fst_appTop, inferInstance, And.intro, RingHom.surjective_respectsIso, RingHom.surjective_isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X_1 Y_1 Z : Scheme
this :
  AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (f : X ⟶ x) [IsAffine x] ↦
    IsAffine X ∧
      Function.Surjective (α := (↑Γ(x, ⊤) : Type u_1)) (β := (↑Γ(X, ⊤) : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(x, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
ha : IsAffine Y
hsurj :
  Function.Surjective (α := (↑Γ(S, ⊤) : Type u_1)) (β := (↑Γ(Y, ⊤) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop g)) :
      (a : (↑Γ(S, ⊤) : Type u_1)) → (↑Γ(Y, ⊤) : Type u_1))
⊢ IsAffine.{u_1} (Limits.pullback f g) ∧
    Function.Surjective (α := (↑Γ(X, ⊤) : Type u_1)) (β := (↑Γ(Limits.pullback f g, ⊤) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := Γ(Limits.pullback f g, ⊤)) (Scheme.Hom.appTop (Limits.pullback.fst f g))) :
        (a : (↑Γ(X, ⊤) : Type u_1)) → (↑Γ(Limits.pullback f g, ⊤) : Type u_1))

Tactic:
exact ⟨inferInstance, RingHom.surjective_isStableUnderBaseChange.pullback_fst_appTop _
    RingHom.surjective_respectsIso f _ hsurj⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : IsClosedImmersion g
⊢ IsClosedImmersion (X := Limits.pullback f g) (Limits.pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst _ _ ‹_›

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

Tactic:
MorphismProperty.pullback_snd _ _ ‹_›

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
V : Y.Opens
inst : IsClosedImmersion f
⊢ IsClosedImmersion (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X_1 Y_1 Z X Y : Scheme
f : X ⟶ Y
h : IsClosedImmersion f
rw : targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
⊢ LocallyOfFiniteType f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @LocallyOfFiniteType,
    ← and_iff_right (inferInstance : IsAffineHom f) (b := affineLocally _ _),
    ← targetAffineLocally_affineAnd_iff_affineLocally RingHom.finiteType_isLocal]

Premises used: inferInstance, AlgebraicGeometry.HasRingHomProperty.eq_affineLocally, RingHom.finiteType_isLocal, and_iff_right, AlgebraicGeometry.LocallyOfFiniteType, AlgebraicGeometry.targetAffineLocally_affineAnd_iff_affineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X_1 Y_1 Z X Y : Scheme
f : X ⟶ Y
h : IsClosedImmersion f
⊢ targetAffineLocally
    (fun (X x : Scheme.{u}) (f : X ⟶ x) [IsAffine x] ↦
      IsAffine X ∧
        Function.Surjective (α := (↑Γ(x, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f)) :
            (a : (↑Γ(x, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)))
    f

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion] at h

Premises used: AlgebraicGeometry.IsClosedImmersion, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X_1 Y_1 Z X Y : Scheme
f : X ⟶ Y
h :
  targetAffineLocally
    (fun (X x : Scheme.{u}) (f : X ⟶ x) [IsAffine x] ↦
      IsAffine X ∧
        Function.Surjective (α := (↑Γ(x, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f)) :
            (a : (↑Γ(x, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)))
    f
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
targetAffineLocally_affineAnd_le (RingHom.FiniteType.of_surjective _) _ h

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_le, RingHom.FiniteType.of_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X_1 Y_1 Z X Y : Scheme
f : X ⟶ Y
h :
  targetAffineLocally
    (fun (X x : Scheme.{u}) (f : X ⟶ x) [IsAffine x] ↦
      IsAffine X ∧
        Function.Surjective (α := (↑Γ(x, ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f)) :
            (a : (↑Γ(x, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)))
    f
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
exact targetAffineLocally_affineAnd_le (RingHom.FiniteType.of_surjective _) _ h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
inst_1 : Surjective f
inst_2 : IsReduced Y
rw : closure (Set.range (ι := ↥X) ⇑f) = (↑⊤ : Set ↥Y)
⊢ IsIso f

Tactic:
rw [IsClosedImmersion.isIso_iff_ker_eq_bot, ← Scheme.IdealSheafData.support_eq_top_iff,
    ← SetLike.coe_injective.eq_iff, Scheme.Hom.support_ker]

Premises used: Function.Injective.eq_iff, AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff, SetLike.coe_injective, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
inst_1 : Surjective f
inst_2 : IsReduced Y
⊢ closure (Set.range (ι := ↥X) ⇑f) = (↑⊤ : Set ↥Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
x : ↥X
rw :
  IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (X.residueField x))) ⇑(X.fromSpecResidueField x)) ↔
    IsClosedImmersion (X.fromSpecResidueField x)
⊢ IsClosed (X := ↥X) {x} ↔ IsClosedImmersion (X.fromSpecResidueField x)

Tactic:
rw [← Scheme.range_fromSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.range_fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
x : ↥X
⊢ IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (X.residueField x))) ⇑(X.fromSpecResidueField x)) ↔
    IsClosedImmersion (X.fromSpecResidueField x)

Tactic:
⟨fun H ↦ .of_isPreimmersion _ H,
    fun _ ↦ (X.fromSpecResidueField x).isClosedEmbedding.isClosed_range⟩

Premises used: AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion, AlgebraicGeometry.Scheme.fromSpecResidueField, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, Iff.intro, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
x : ↥X
⊢ IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (X.residueField x))) ⇑(X.fromSpecResidueField x)) ↔
    IsClosedImmersion (X.fromSpecResidueField x)

Tactic:
exact ⟨fun H ↦ .of_isPreimmersion _ H,
    fun _ ↦ (X.fromSpecResidueField x).isClosedEmbedding.isClosed_range⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
        (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g)
    (hX : ¬∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
wlog :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
⊢ IsClosedImmersion g

Tactic:
wlog hX : ∃ R, X = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
inr :
  ∀ (i : X.affineCover.toPreZeroHypercover.1),
    IsClosedImmersion (X := (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover g i :
        (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i ⟶ X.affineCover.X i)
⊢ IsClosedImmersion g

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) X.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
pos :
  ∀ (hxU : Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)),
    IsClosedImmersion (X := (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover g i :
        (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i ⟶ X.affineCover.X i)
neg :
  ∀ (hxU : ¬Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)),
    IsClosedImmersion (X := (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover g i :
        (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i ⟶ X.affineCover.X i)
⊢ IsClosedImmersion (X := (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover g i :
      (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i ⟶ X.affineCover.X i)

Tactic:
by_cases hxU : Set.range g ⊆ (X.affineCover.f i).opensRange

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
pos : IsClosedImmersion (IsOpenImmersion.lift (X.affineCover.f i) g hxU)
⊢ IsClosedImmersion (X := (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover g i :
      (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i ⟶ X.affineCover.X i)

Tactic:
rw [Scheme.Cover.pullbackHom,
        ← (IsOpenImmersion.isPullback_lift_id _ _ hxU).flip.isoPullback_inv_snd,
        MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, CategoryTheory.IsPullback.isoPullback_inv_snd, AlgebraicGeometry.IsOpenImmersion.isPullback_lift_id, CategoryTheory.IsPullback.flip, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, AlgebraicGeometry.IsClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
⊢ IsClosedImmersion (IsOpenImmersion.lift (X.affineCover.f i) g hxU)

Tactic:
this (X.affineCover.f i ≫ f) _ ?_ ⟨_, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
pos : IsOpenImmersion.lift (X.affineCover.f i) g hxU ≫ X.affineCover.f i ≫ f = 𝟙 Y
⊢ IsClosedImmersion (IsOpenImmersion.lift (X.affineCover.f i) g hxU)

Tactic:
refine this (X.affineCover.f i ≫ f) _ ?_ ⟨_, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
pos : g ≫ f = 𝟙 Y
pos₁ pos₂ : 𝟙 Y = 𝟙 Y
⊢ IsOpenImmersion.lift (X.affineCover.f i) g hxU ≫ X.affineCover.f i ≫ f = 𝟙 Y

Tactic:
rw [IsOpenImmersion.lift_fac_assoc, hg]

Premises used: AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
H : Disjoint (α := Set ↥X) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i))
⊢ IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)

Tactic:
apply Scheme.isEmpty_pullback

Premises used: AlgebraicGeometry.Scheme.isEmpty_pullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
H : Subset (α := Set ↥X) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i)) (Set.range (ι := ↥Y) ⇑g)ᶜ
⊢ Disjoint (α := Set ↥X) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i))

Tactic:
rw [← Set.subset_compl_iff_disjoint_left]

Premises used: Set.subset_compl_iff_disjoint_left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
x : ↥Y
hx : Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i)) (g x : ↥X)
H : Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
⊢ False

Tactic:
apply hxU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
x : ↥Y
hx : Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i)) (g x : ↥X)
y : ↥Y
⊢ Membership.mem (α := ↥X) (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X) (g y : ↥X)

Tactic:
Subsingleton.elim x y ▸ hx

Premises used: Eq.rec, Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
x : ↥Y
hx : Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i)) (g x : ↥X)
y : ↥Y
⊢ Membership.mem (α := ↥X) (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X) (g y : ↥X)

Tactic:
exact Subsingleton.elim x y ▸ hx
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
⊢ IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)

Tactic:
have : IsEmpty ((X.affineCover.pullback₁ g).X i) := by
        apply Scheme.isEmpty_pullback
        rw [← Set.subset_compl_iff_disjoint_left]
        rintro _ hx ⟨x, rfl⟩
        apply hxU
        rintro _ ⟨y, rfl⟩
        exact Subsingleton.elim x y ▸ hx
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this_1 :
  ∀ {X Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (f : X ⟶ Y) (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y)
    (hX : ∃ (R : CommRingCat.{u}), X = Spec R), IsClosedImmersion g
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
this : IsEmpty.{u + 1} ↥((Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)
⊢ IsClosedImmersion (X := (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover g i :
      (Precoverage.ZeroHypercover.pullback₁ g X.affineCover).X i ⟶ X.affineCover.X i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
hX : ∃ (R : CommRingCat.{u}), X = Spec R
obtain : ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R) (hg : g ≫ f = 𝟙 Y), IsClosedImmersion g
⊢ IsClosedImmersion g

Tactic:
obtain ⟨R, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
inr :
  ∀
    (this :
      ∀ {Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (R : CommRingCat.{u}) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R)
        (hg : g ≫ f = 𝟙 Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsClosedImmersion g)
    (hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S), IsClosedImmersion g
wlog :
  ∀ {Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (R : CommRingCat.{u}) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R)
    (hg : g ≫ f = 𝟙 Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsClosedImmersion g
⊢ IsClosedImmersion g

Tactic:
wlog hY : ∃ S, Y = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (R : CommRingCat.{u}) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R)
    (hg : g ≫ f = 𝟙 Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsClosedImmersion g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
⊢ Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))

Tactic:
have inst := (Scheme.isoSpec Y).inv.homeomorph.injective.subsingleton
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Y : Scheme
inst_1 : Subsingleton.{u + 1} ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme.{u}} [Subsingleton.{u + 1} ↥Y] (R : CommRingCat.{u}) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R)
    (hg : g ≫ f = 𝟙 Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), IsClosedImmersion g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inst : Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))
inr : IsClosedImmersion (Y.isoSpec.inv ≫ g)
⊢ IsClosedImmersion g

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (Scheme.isoSpec Y).inv]

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, AlgebraicGeometry.IsClosedImmersion, CategoryTheory.Iso.inv