awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
f : R ⟶ S
h :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
x : ↥(Spec S)
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)).RespectsIso
apply :
  RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S) (X :=
    CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) x).asIdeal)) (Y :=
    CommRingCat.of (Localization.AtPrime x.asIdeal))
    (CommRingCat.ofHom
      (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) x).asIdeal x.asIdeal
        (CommRingCat.Hom.hom f) ⋯))
⊢ Function.Surjective (α := (↑((Spec R).presheaf.stalk ((Spec.map f) x)) : Type u_1)) (β :=
    (↑((Spec S).presheaf.stalk 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.stalkMap (Spec.map f) x)) :
      (a : (↑((Spec R).presheaf.stalk ((Spec.map f) x)) : Type u_1)) → (↑((Spec S).presheaf.stalk x) : Type u_1))

Tactic:
apply (MorphismProperty.arrow_mk_iso_iff
      (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f))
      (Scheme.arrowStalkMapSpecIso f x)).mpr

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.arrowStalkMapSpecIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, DFunLike.coe, Function.Surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
f : R ⟶ S
h :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
x : ↥(Spec S)
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)).RespectsIso
⊢ RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S) (X :=
    CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) x).asIdeal)) (Y :=
    CommRingCat.of (Localization.AtPrime x.asIdeal))
    (CommRingCat.ofHom
      (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) x).asIdeal x.asIdeal
        (CommRingCat.Hom.hom f) ⋯))

Tactic:
RingHom.surjective_localRingHom_of_surjective f.hom h x.asIdeal

Premises used: CommRingCat.Hom.hom, Set.Mem, OreLocalization, setOf, RingHom.surjective_localRingHom_of_surjective, Quotient, RingHom.toMorphismProperty, Ideal.comap, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R S : CommRingCat
f : R ⟶ S
h :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
x : ↥(Spec S)
this :
  (RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)).RespectsIso
⊢ RingHom.toMorphismProperty fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S) (X :=
    CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) x).asIdeal)) (Y :=
    CommRingCat.of (Localization.AtPrime x.asIdeal))
    (CommRingCat.ofHom
      (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) x).asIdeal x.asIdeal
        (CommRingCat.Hom.hom f) ⋯))

Tactic:
exact RingHom.surjective_localRingHom_of_surjective f.hom h x.asIdeal

Premises used: CommRingCat.Hom.hom, RingHom.surjective_localRingHom_of_surjective, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
R : CommRingCat
I : Ideal (↑R : Type u)
⊢ IsClosedImmersion (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

Tactic:
spec_of_surjective _ Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective, AlgebraicGeometry.IsClosedImmersion.spec_of_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
h :
  Function.Surjective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
rw : IsClosedImmersion (Spec.map (Scheme.Hom.appTop f))
⊢ IsClosedImmersion f

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff @IsClosedImmersion (arrowIsoSpecΓOfIsAffine f)]

Premises used: AlgebraicGeometry.arrowIsoSpecΓOfIsAffine, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.IsClosedImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
h h₁ :
  Function.Surjective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
⊢ IsClosedImmersion (Spec.map (Scheme.Hom.appTop f))

Tactic:
apply spec_of_surjective

Premises used: AlgebraicGeometry.IsClosedImmersion.spec_of_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
h :
  Function.Surjective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
⊢ Function.Surjective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))

Tactic:
h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
h :
  Function.Surjective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))
⊢ Function.Surjective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1))

Tactic:
exact h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
x : ↥X
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk 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.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
have h := (f ≫ g).stalkMap_surjective x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
x : ↥X
h :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk 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.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk 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.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
simp_rw [Scheme.Hom.stalkMap_comp] at h

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
x : ↥X
h :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk 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.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u_1)) (β := (↑(X.presheaf.stalk 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.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
Function.Surjective.of_comp h

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
x : ↥X
h :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk 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.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ Function.Surjective (α := (↑(Y.presheaf.stalk (f x)) : Type u_1)) (β := (↑(X.presheaf.stalk 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.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
exact Function.Surjective.of_comp h

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
⊢ IsClosedEmbedding (X := ↥X) (Y := ↥Z) ⇑(f ≫ g)

Tactic:
have h := (f ≫ g).isClosedEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (X := ↥X) (Y := ↥Z) (Function.comp (β := ↥Y) ⇑g ⇑f)
⊢ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
.of_continuous_injective_isClosedMap (Scheme.Hom.continuous f) h.injective.of_comp ?_

Premises used: Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap, Topology.IsEmbedding.injective, AlgebraicGeometry.Scheme.Hom.continuous, Function.Injective.of_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (X := ↥X) (Y := ↥Z) (Function.comp (β := ↥Y) ⇑g ⇑f)
refine : IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
refine .of_continuous_injective_isClosedMap (Scheme.Hom.continuous f) h.injective.of_comp ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z_1 : Scheme
f : X ⟶ Y
g : Y ⟶ Z_1
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (X := ↥X) (Y := ↥Z_1) (Function.comp (β := ↥Y) ⇑g ⇑f)
Z : Set ↥X
hZ : IsClosed Z
rw : IsClosed (X := ↥Z_1) (Function.comp (β := ↥Y) ⇑g ⇑f '' Z)
⊢ IsClosed (X := ↥Y) (⇑f '' Z)

Tactic:
rw [IsClosedEmbedding.isClosed_iff_image_isClosed g.isClosedEmbedding,
      ← Set.image_comp]

Premises used: Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, Set.image_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z_1 : Scheme
f : X ⟶ Y
g : Y ⟶ Z_1
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (X := ↥X) (Y := ↥Z_1) (Function.comp (β := ↥Y) ⇑g ⇑f)
Z : Set ↥X
hZ : IsClosed Z
⊢ IsClosed (X := ↥Z_1) (Function.comp (β := ↥Y) ⇑g ⇑f '' Z)

Tactic:
h.isClosedMap _ hZ

Premises used: Topology.IsClosedEmbedding.isClosedMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z_1 : Scheme
f : X ⟶ Y
g : Y ⟶ Z_1
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding (X := ↥X) (Y := ↥Z_1) (Function.comp (β := ↥Y) ⇑g ⇑f)
Z : Set ↥X
hZ : IsClosed Z
⊢ IsClosed (X := ↥Z_1) (Function.comp (β := ↥Y) ⇑g ⇑f '' Z)

Tactic:
exact h.isClosedMap _ hZ

Premises used: Topology.IsClosedEmbedding.isClosedMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X : Scheme
x : ↥X
⊢ IsClosedImmersion (Spec.map (X.residue x))

Tactic:
IsClosedImmersion.spec_of_surjective (X.residue x)
    Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective, AlgebraicGeometry.IsClosedImmersion.spec_of_surjective, AlgebraicGeometry.Scheme.residue
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
⊢ IsAffineHom f

Tactic:
isAffineHom_of_isInducing _ f.isClosedEmbedding.isInducing f.isClosedEmbedding.isClosed_range

Premises used: Topology.IsClosedEmbedding.isInducing, AlgebraicGeometry.isAffineHom_of_isInducing, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst rw : IsClosedImmersion f
⊢ IsClosedImmersion (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
rw [Scheme.Hom.toImage_imageι]

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_imageι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
⊢ IsClosedImmersion f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
⊢ IsClosedImmersion (Scheme.Hom.toImage f)

Tactic:
have := @of_comp_isClosedImmersion _ _ _ f.toImage f.imageι inferInstance
    (by rw [Scheme.Hom.toImage_imageι]; infer_instance)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
rw : Eq (α := Set ↥(Scheme.Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Scheme.Hom.toImage f))) Set.univ
⊢ Function.Surjective (α := ↥X) (β := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)

Tactic:
rw [← Set.range_eq_univ, ← f.toImage.isClosedEmbedding.isClosed_range.closure_eq]

Premises used: Set.range_eq_univ, IsClosed.closure_eq, AlgebraicGeometry.Scheme.Hom.toImage, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ Eq (α := Set ↥(Scheme.Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Scheme.Hom.toImage f))) Set.univ

Tactic:
f.toImage.denseRange.closure_eq

Premises used: AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.Scheme.Hom.toImage, Dense.closure_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ Eq (α := Set ↥(Scheme.Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Scheme.Hom.toImage f))) Set.univ

Tactic:
exact f.toImage.denseRange.closure_eq

Premises used: AlgebraicGeometry.Scheme.Hom.denseRange, AlgebraicGeometry.Scheme.Hom.toImage, Dense.closure_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)

Tactic:
have : IsHomeomorph f.toImage :=
    isHomeomorph_iff_isEmbedding_surjective.mpr ⟨f.toImage.isEmbedding, by
      rw [← Set.range_eq_univ, ← f.toImage.isClosedEmbedding.isClosed_range.closure_eq]
      exact f.toImage.denseRange.closure_eq⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
⊢ IsIso (Scheme.Hom.toImage f)

Tactic:
isomorphisms_eq_stalkwise.ge _ ⟨?_, ?_⟩

Premises used: Eq.ge, And.intro, AlgebraicGeometry.isomorphisms_eq_stalkwise
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
refine_1 :
  MorphismProperty.inverseImage (MorphismProperty.isomorphisms TopCat) Scheme.forgetToTop (Scheme.Hom.toImage f)
refine_2 :
  stalkwise
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S))
    (Scheme.Hom.toImage f)
⊢ IsIso (Scheme.Hom.toImage f)

Tactic:
refine isomorphisms_eq_stalkwise.ge _ ⟨?_, ?_⟩

Premises used: Eq.ge, And.intro, AlgebraicGeometry.isomorphisms_eq_stalkwise
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
⊢ MorphismProperty.inverseImage (MorphismProperty.isomorphisms TopCat) Scheme.forgetToTop (Scheme.Hom.toImage f)

Tactic:
inferInstanceAs (IsIso (TopCat.isoOfHomeo this.homeomorph).hom)

Premises used: IsHomeomorph.homeomorph, CategoryTheory.ConcreteCategory.hom, CategoryTheory.MorphismProperty.inverseImage, AlgebraicGeometry.Scheme.Hom.toImage, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', toContinuousMap, CategoryTheory.Iso.isIso_hom, TopCat.isoOfHomeo, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
⊢ MorphismProperty.inverseImage (MorphismProperty.isomorphisms TopCat) Scheme.forgetToTop (Scheme.Hom.toImage f)

Tactic:
exact inferInstanceAs (IsIso (TopCat.isoOfHomeo this.homeomorph).hom)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
x : ↥X
⊢ Function.Bijective (α := (↑((Scheme.Hom.image f).presheaf.stalk ((Scheme.Hom.toImage f) x)) : Type u)) (β :=
    (↑(X.presheaf.stalk x) : Type u))
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.toImage f) x)) :
      (a : (↑((Scheme.Hom.image f).presheaf.stalk ((Scheme.Hom.toImage f) x)) : Type u)) →
        (↑(X.presheaf.stalk x) : Type u))

Tactic:
⟨?_, f.toImage.stalkMap_surjective x⟩

Premises used: AlgebraicGeometry.Scheme.Hom.toImage, And.intro, Function.Bijective, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
x : ↥X
refine_2 :
  Function.Injective (α := (↑((Scheme.Hom.image f).presheaf.stalk ((Scheme.Hom.toImage f) x)) : Type u)) (β :=
    (↑(X.presheaf.stalk x) : Type u))
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.toImage f) x)) :
      (a : (↑((Scheme.Hom.image f).presheaf.stalk ((Scheme.Hom.toImage f) x)) : Type u)) →
        (↑(X.presheaf.stalk x) : Type u))
⊢ Function.Bijective (α := (↑((Scheme.Hom.image f).presheaf.stalk ((Scheme.Hom.toImage f) x)) : Type u)) (β :=
    (↑(X.presheaf.stalk x) : Type u))
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.toImage f) x)) :
      (a : (↑((Scheme.Hom.image f).presheaf.stalk ((Scheme.Hom.toImage f) x)) : Type u)) →
        (↑(X.presheaf.stalk x) : Type u))

Tactic:
refine ⟨?_, f.toImage.stalkMap_surjective x⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
x : ↥X
⊢ Function.Injective (α := (↑((Scheme.Hom.image f).presheaf.stalk ((Scheme.Hom.toImage f) x)) : Type u)) (β :=
    (↑(X.presheaf.stalk x) : Type u))
    (Function.comp (β :=
      (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base) X.presheaf).stalk
            ((Scheme.Hom.toImage f) x)) :
        Type u))
      (⇑(CommRingCat.Hom.hom (TopCat.Presheaf.stalkPushforward CommRingCat (Scheme.Hom.toImage f).base X.presheaf x)) :
        (a :
            (↑(((TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base).obj X.presheaf).stalk
                  ((Scheme.Hom.toImage f) x)) :
              Type u)) →
          (↑(X.presheaf.stalk x) : Type u))
      (⇑(CommRingCat.Hom.hom
            (CategoryTheory.Functor.map (TopCat.Presheaf.stalkFunctor CommRingCat ((Scheme.Hom.toImage f) x))
              (Scheme.Hom.toImage f).c)) :
        (a : (↑((Scheme.Hom.image f).presheaf.stalk ((Scheme.Hom.toImage f) x)) : Type u)) →
          (↑(((TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base).obj X.presheaf).stalk
                ((Scheme.Hom.toImage f) x)) :
            Type u)))

Tactic:
.comp ?_ (f.stalkFunctor_toImage_injective _)

Premises used: AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective, Function.Injective.comp