awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ 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))
have 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)
      sorry))
Tactic: apply (MorphismProperty.arrow_mk_iso_iff
      (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f))
      (Scheme.arrowStalkMapSpecIso f x)).mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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))
⊢ IsClosedImmersion f
have rw : IsClosedImmersion (Spec.map (Scheme.Hom.appTop f))
Tactic: rw [MorphismProperty.arrow_mk_iso_iff @IsClosedImmersion (arrowIsoSpecΓOfIsAffine f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
x : ↥X
⊢ 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))
have 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))
Tactic: have h := (f ≫ g).stalkMap_surjective x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
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 (α := (↑(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))
have 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))
Tactic: simp_rw [Scheme.Hom.stalkMap_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsClosedImmersion g
inst_1 : IsClosedImmersion (f ≫ g)
⊢ IsClosedEmbedding (X := ↥X) (Y := ↥Y) ⇑f
have h : IsClosedEmbedding (X := ↥X) (Y := ↥Z) ⇑(f ≫ g)
Tactic: have h := (f ≫ g).isClosedEmbedding
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
have refine : IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
Tactic: refine .of_continuous_injective_isClosedMap (Scheme.Hom.continuous f) h.injective.of_comp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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 := ↥Y) (⇑f '' Z)
have rw : IsClosed (X := ↥Z_1) (Function.comp (β := ↥Y) ⇑g ⇑f '' Z)
Tactic: rw [IsClosedEmbedding.isClosed_iff_image_isClosed g.isClosedEmbedding,
      ← Set.image_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
⊢ IsIso (Scheme.Hom.toImage f)
have this : IsClosedImmersion (Scheme.Hom.toImage f)
Tactic: have := @of_comp_isClosedImmersion _ _ _ f.toImage f.imageι inferInstance
    (by rw [Scheme.Hom.toImage_imageι]; infer_instance)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ Function.Surjective (α := ↥X) (β := ↥(Scheme.Hom.image f)) ⇑(Scheme.Hom.toImage f)
have rw : Eq (α := Set ↥(Scheme.Hom.image f)) (closure (Set.range (ι := ↥X) ⇑(Scheme.Hom.toImage f))) Set.univ
Tactic: rw [← Set.range_eq_univ, ← f.toImage.isClosedEmbedding.isClosed_range.closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
this : IsClosedImmersion (Scheme.Hom.toImage f)
⊢ IsIso (Scheme.Hom.toImage f)
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
have refine_1 : MorphismProperty.inverseImage (MorphismProperty.isomorphisms TopCat) Scheme.forgetToTop (Scheme.Hom.toImage f)
Tactic: refine isomorphisms_eq_stalkwise.ge _ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
⊢ IsIso (Scheme.Hom.toImage f)
have 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)
Tactic: refine isomorphisms_eq_stalkwise.ge _ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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))
have 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))
Tactic: refine ⟨?_, f.toImage.stalkMap_surjective x⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)))
have 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))
Tactic: refine .comp ?_ (f.stalkFunctor_toImage_injective _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
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 (α :=
    (↑((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))
have 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)
Tactic: have := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing CommRingCat
      (f := f.toImage.base) f.toImage.isEmbedding.isInducing X.presheaf x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
⊢ IsIso f ↔ Scheme.Hom.ker f = ⊥
have refine : ∀ (H : Scheme.Hom.ker f = ⊥), IsIso f
Tactic: refine ⟨fun _ ↦ f.ker_eq_bot_of_isIso, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
H : Scheme.Hom.ker f = ⊥
⊢ IsIso f
have this : IsIso (Scheme.Hom.imageι f)
Tactic: have : IsIso f.imageι := by simpa [Scheme.Hom.imageι, Scheme.Hom.image] using H ▸ inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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 ≫ f = g
have nth_rw : lift f g H ≫ Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f = g
Tactic: nth_rw 2 [← f.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ IsIso f
have rwa : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ IsIso f
have 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
Tactic: rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),
      ← isIso_iff_of_reflects_iso _ (Over.forget _)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ IsIso f
have 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
Tactic: rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),
      ← isIso_iff_of_reflects_iso _ (Over.forget _)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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 f
have suffices : IsIso f'.op
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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 f'.op
have rw : IsIso ((overEquivIdealSheafData X).functor.map f'.op)
Tactic: rw [← isIso_iff_of_reflects_iso _ (IsClosedImmersion.overEquivIdealSheafData X).functor]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
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))
⊢ IsDominant f
have this : 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])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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))
have 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))
Tactic: refine stalkMap_injective_of_isAffine _ _ (fun (g : Γ(Y, ⊤)) h ↦ ?_)