awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α :=
    (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base) X.presheaf).stalk
          ((Scheme.Hom.toImage f) x)) :
      Type u))
    (β := (↑(X.presheaf.stalk 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))
⊢ 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:
refine .comp ?_ (f.stalkFunctor_toImage_injective _)
-- 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
⊢ IsIso (X :=
    (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base) X.presheaf).stalk
      ((Scheme.Hom.toImage f) x))
    (TopCat.Presheaf.stalkPushforward CommRingCat (Scheme.Hom.toImage f).base X.presheaf x)

Tactic:
have := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing CommRingCat
      (f := f.toImage.base) f.toImage.isEmbedding.isInducing X.presheaf x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this_2 : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
x : ↥X
this :
  IsIso (X :=
    (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base) X.presheaf).stalk
      ((Scheme.Hom.toImage f) x))
    (TopCat.Presheaf.stalkPushforward CommRingCat (Scheme.Hom.toImage f).base X.presheaf x)
⊢ Function.Injective (α :=
    (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base) X.presheaf).stalk
          ((Scheme.Hom.toImage f) x)) :
      Type u))
    (β := (↑(X.presheaf.stalk 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))

Tactic:
((ConcreteCategory.isIso_iff_bijective _).mp this).1

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective, And.left, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this_1 : IsClosedImmersion (Scheme.Hom.toImage f)
this_2 : IsHomeomorph (X := ↥X) (Y := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
x : ↥X
this :
  IsIso (X :=
    (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base) X.presheaf).stalk
      ((Scheme.Hom.toImage f) x))
    (TopCat.Presheaf.stalkPushforward CommRingCat (Scheme.Hom.toImage f).base X.presheaf x)
⊢ Function.Injective (α :=
    (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Scheme.Hom.toImage f).base) X.presheaf).stalk
          ((Scheme.Hom.toImage f) x)) :
      Type u))
    (β := (↑(X.presheaf.stalk 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))

Tactic:
exact ((ConcreteCategory.isIso_iff_bijective _).mp this).1

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective, And.left, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
⊢ IsIso f ↔ Scheme.Hom.ker f = ⊥

Tactic:
⟨fun _ ↦ f.ker_eq_bot_of_isIso, fun H ↦ ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
refine : ∀ (H : Scheme.Hom.ker f = ⊥), IsIso f
⊢ IsIso f ↔ Scheme.Hom.ker f = ⊥

Tactic:
refine ⟨fun _ ↦ f.ker_eq_bot_of_isIso, fun H ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
⊢ IsIso (Scheme.Hom.imageι f)

Tactic:
simpa [Scheme.Hom.imageι, Scheme.Hom.image] using H ▸ inferInstance

Premises used: AlgebraicGeometry.Scheme.Hom.image, AlgebraicGeometry.Scheme.Hom.imageι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
⊢ IsIso (Scheme.Hom.imageι f)

Tactic:
have : IsIso f.imageι := by simpa [Scheme.Hom.imageι, Scheme.Hom.image] using H ▸ inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
this : IsIso (Scheme.Hom.imageι f)
⊢ IsIso f

Tactic:
f.toImage_imageι ▸ inferInstance

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_imageι, Eq.rec, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
this : IsIso (Scheme.Hom.imageι f)
⊢ IsIso f

Tactic:
exact f.toImage_imageι ▸ inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : IsClosedImmersion f
H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g
nth_rw : lift f g H ≫ Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f = g
⊢ lift f g H ≫ f = g

Tactic:
nth_rw 2 [← f.toImage_imageι]

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_imageι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : IsClosedImmersion f
H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g
⊢ lift f g H ≫ Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f = g

Tactic:
simp [lift, -Scheme.Hom.toImage_imageι, g.toImage_imageι]

Premises used: AlgebraicGeometry.Scheme.Hom.toImage_imageι, AlgebraicGeometry.IsClosedImmersion.lift
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst : IsClosedImmersion i₁
inst_1 : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h_1 : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : Quiver.Hom (V := MorphismProperty.Over @IsClosedImmersion ⊤ X)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₁ inst)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₂ inst_1) :=
  MorphismProperty.Over.homMk (P := @IsClosedImmersion) (Q := ⊤) f h_1 True.intro
h : IsIso f'.op
rwa : ∀ (h : IsIso f'), IsIso f
rwa₁ :
  ∀
    (h :
      IsIso (X :=
        Functor.obj (C := MorphismProperty.Over @IsClosedImmersion ⊤ X)
          (MorphismProperty.Over.forget @IsClosedImmersion ⊤ X)
          (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₁ inst))
        (CategoryTheory.Functor.map (MorphismProperty.Over.forget @IsClosedImmersion ⊤ X) f')),
    IsIso f
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (h :
      IsIso (X :=
        Functor.obj (Over.forget X)
          (Functor.obj (C := MorphismProperty.Over @IsClosedImmersion ⊤ X)
            (MorphismProperty.Over.forget @IsClosedImmersion ⊤ X)
            (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₁ inst)))
        (CategoryTheory.Functor.map (Over.forget X)
          (CategoryTheory.Functor.map (MorphismProperty.Over.forget @IsClosedImmersion ⊤ X) f'))),
    IsIso f
⊢ IsIso f

Tactic:
rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),
      ← isIso_iff_of_reflects_iso _ (Over.forget _)] at h

Premises used: CategoryTheory.Over.forget, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.MorphismProperty.Over.forget, CategoryTheory.isIso_op_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst : IsClosedImmersion i₁
inst_1 : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : Quiver.Hom (V := MorphismProperty.Over @IsClosedImmersion ⊤ X)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₁ inst)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₂ inst_1) :=
  MorphismProperty.Over.homMk (P := @IsClosedImmersion) (Q := ⊤) f h True.intro
suffices : IsIso f'.op
⊢ IsIso f

Tactic:
suffices h : IsIso f'.op by
    rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),
      ← isIso_iff_of_reflects_iso _ (Over.forget _)] at h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst : IsClosedImmersion i₁
inst_1 : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : Quiver.Hom (V := MorphismProperty.Over @IsClosedImmersion ⊤ X)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₁ inst)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₂ inst_1) :=
  MorphismProperty.Over.homMk (P := @IsClosedImmersion) (Q := ⊤) f h True.intro
rw : IsIso ((overEquivIdealSheafData X).functor.map f'.op)
⊢ IsIso f'.op

Tactic:
rw [← isIso_iff_of_reflects_iso _ (IsClosedImmersion.overEquivIdealSheafData X).functor]

Premises used: AlgebraicGeometry.IsClosedImmersion.overEquivIdealSheafData, CategoryTheory.Equivalence.functor, CategoryTheory.isIso_iff_of_reflects_iso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst : IsClosedImmersion i₁
inst_1 : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : Quiver.Hom (V := MorphismProperty.Over @IsClosedImmersion ⊤ X)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₁ inst)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₂ inst_1) :=
  MorphismProperty.Over.homMk (P := @IsClosedImmersion) (Q := ⊤) f h True.intro
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = 𝟙 (Scheme.Hom.ker i₂)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst : IsClosedImmersion i₁
inst_1 : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : Quiver.Hom (V := MorphismProperty.Over @IsClosedImmersion ⊤ X)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₁ inst)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₂ inst_1) :=
  MorphismProperty.Over.homMk (P := @IsClosedImmersion) (Q := ⊤) f h True.intro
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = 𝟙 (Scheme.Hom.ker i₁)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst : IsClosedImmersion i₁
inst_1 : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : Quiver.Hom (V := MorphismProperty.Over @IsClosedImmersion ⊤ X)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₁ inst)
  (MorphismProperty.Over.mk (P := @IsClosedImmersion) ⊤ i₂ inst_1) :=
  MorphismProperty.Over.homMk (P := @IsClosedImmersion) (Q := ⊤) f h True.intro
⊢ IsIso ((overEquivIdealSheafData X).functor.map f'.op)

Tactic:
simpa [IsClosedImmersion.overEquivIdealSheafData] using ⟨homOfLE h'.le, by simp, by simp⟩

Premises used: AlgebraicGeometry.IsClosedImmersion.overEquivIdealSheafData
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst : IsClosedImmersion i₁
inst_1 : IsClosedImmersion i₂
h : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
⊢ lift i₁ i₂ ⋯ ≫ i₁ = i₂

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfinj :
  Function.Injective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
⊢ (Scheme.Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) =
    Scheme.IdealSheafData.ideal ⊥ (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)

Tactic:
simpa [f.ker_apply ⟨⊤, isAffineOpen_top Y⟩, ← RingHom.injective_iff_ker_eq_bot]

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Scheme.Hom.ker_apply, Subtype.mk, RingHom.injective_iff_ker_eq_bot, Top.top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfinj :
  Function.Injective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
⊢ Scheme.Hom.ker f = ⊥

Tactic:
have : f.ker = ⊥ := Scheme.IdealSheafData.ext_of_isAffine
    (by simpa [f.ker_apply ⟨⊤, isAffineOpen_top Y⟩, ← RingHom.injective_iff_ker_eq_bot])
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfinj :
  Function.Injective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
this : Scheme.Hom.ker f = ⊥
⊢ DenseRange (X := ↥Y) (α := ↥X) ⇑f

Tactic:
simpa only [Scheme.Hom.support_ker, Scheme.IdealSheafData.support_bot,
    Closeds.coe_top, ← dense_iff_closure_eq] using (congr((↑($this).support : Set Y)) :)

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, congrArg, dense_iff_closure_eq, id, TopologicalSpace.Closeds.coe_top, SetLike.coe, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.Scheme.IdealSheafData.support_bot
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfinj :
  Function.Injective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
this : Scheme.Hom.ker f = ⊥
⊢ IsDominant f

Tactic:
exact ⟨by simpa only [Scheme.Hom.support_ker, Scheme.IdealSheafData.support_bot,
    Closeds.coe_top, ← dense_iff_closure_eq] using (congr((↑($this).support : Set Y)) :)⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
⊢ Function.Injective (α := (↑Γ(Spec Γ(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 X.toSpecΓ)) :
      (a : (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))

Tactic:
simpa only [Scheme.toSpecΓ_appTop] using
      (ConcreteCategory.bijective_of_isIso (Scheme.ΓSpecIso Γ(X, ⊤)).hom).1

Premises used: AlgebraicGeometry.Scheme.ΓSpecIso, AlgebraicGeometry.Scheme.toSpecΓ_appTop, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, And.left, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Top.top, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfopen : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
hfinj₁ : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hfinj₂ :
  Function.Injective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun (i : 𝒰.I₀) ↦ Scheme.Hom.appTop (𝒰.f i)
⊢ Function.Injective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
stalkMap_injective_of_isAffine _ _ (fun (g : Γ(Y, ⊤)) h ↦ ?_)

Premises used: AlgebraicGeometry.stalkMap_injective_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfopen : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
hfinj₁ : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hfinj₂ :
  Function.Injective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun (i : 𝒰.I₀) ↦ Scheme.Hom.appTop (𝒰.f i)
refine :
  ∀ (g : (↑Γ(Y, ⊤) : Type u))
    (h :
      Eq (α := (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
              (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.Γgerm (f x)) :
                  (a : (↑(Y.presheaf.obj (op ⊤)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
                g :
              (↑(Y.presheaf.stalk (f x)) : Type u)) :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u))),
    Eq (α := (↑(Y.presheaf.stalk (f x)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.Γgerm (f x)) :
            (a : (↑(Y.presheaf.obj (op ⊤)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
          g :
        (↑(Y.presheaf.stalk (f x)) : Type u))
      (0 : (↑(Y.presheaf.stalk (f x)) : Type u))
⊢ Function.Injective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
refine stalkMap_injective_of_isAffine _ _ (fun (g : Γ(Y, ⊤)) h ↦ ?_)

Premises used: AlgebraicGeometry.stalkMap_injective_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
hfopen : IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f
hfinj₁ : Function.Injective (α := ↥X) (β := ↥Y) ⇑f
hfinj₂ :
  Function.Injective (α := (↑Γ(Y, ⊤) : 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 : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun (i : 𝒰.I₀) ↦ Scheme.Hom.appTop (𝒰.f i)
g : (↑Γ(Y, ⊤) : Type u)
h :
  Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
          (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.Γgerm (f x)) :
              (a : (↑(Y.presheaf.obj (op ⊤)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
            g :
          (↑(Y.presheaf.stalk (f x)) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro) :
          (a : (↑(X.presheaf.obj (op (f ⁻¹ᵁ ⊤))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
            g :
          (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))

Tactic:
rw [TopCat.Presheaf.Γgerm, Scheme.Hom.germ_stalkMap_apply] at h

Premises used: AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, TopCat.Presheaf.Γgerm