awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
X_1 Y_1 Z X Y : Scheme
f : X ⟶ Y
h : IsClosedImmersion f
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
have 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
Tactic: rw [HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
inst_1 : Surjective f
inst_2 : IsReduced Y
⊢ IsIso f
have rw : closure (Set.range (ι := ↥X) ⇑f) = (↑⊤ : Set ↥Y)
Tactic: rw [IsClosedImmersion.isIso_iff_ker_eq_bot, ← Scheme.IdealSheafData.support_eq_top_iff,
    ← SetLike.coe_injective.eq_iff, Scheme.Hom.support_ker]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X : Scheme
x : ↥X
⊢ IsClosed (X := ↥X) {x} ↔ IsClosedImmersion (X.fromSpecResidueField x)
have rw : IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (X.residueField x))) ⇑(X.fromSpecResidueField x)) ↔
  IsClosedImmersion (X.fromSpecResidueField x)
Tactic: rw [← Scheme.range_fromSpecResidueField]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
X Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ IsClosedImmersion g
have 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
Tactic: wlog hX : ∃ R, X = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ IsClosedImmersion g
have 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
Tactic: wlog hX : ∃ R, X = Spec R
Cleared hypotheses: X, Y, inst, f, g, hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ IsClosedImmersion g
have 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)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) X.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hxU : Set.range g ⊆ (X.affineCover.f i).opensRange
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hxU : Set.range g ⊆ (X.affineCover.f i).opensRange
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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 (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)
have pos : IsClosedImmersion (IsOpenImmersion.lift (X.affineCover.f i) g hxU)
Tactic: rw [Scheme.Cover.pullbackHom,
        ← (IsOpenImmersion.isPullback_lift_id _ _ hxU).flip.isoPullback_inv_snd,
        MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
have pos : IsOpenImmersion.lift (X.affineCover.f i) g hxU ≫ X.affineCover.f i ≫ f = 𝟙 Y
Tactic: refine this (X.affineCover.f i ≫ f) _ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ IsOpenImmersion.lift (X.affineCover.f i) g hxU ≫ X.affineCover.f i ≫ f = 𝟙 Y
have pos₁ : 𝟙 Y = 𝟙 Y
Tactic: rw [IsOpenImmersion.lift_fac_assoc, hg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
have H : Disjoint (α := Set ↥X) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i))
Tactic: apply Scheme.isEmpty_pullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
⊢ Disjoint (α := Set ↥X) (Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i))
have H : Subset (α := Set ↥X) (Set.range (ι := ↥(X.affineCover.X i)) ⇑(X.affineCover.f i)) (Set.range (ι := ↥Y) ⇑g)ᶜ
Tactic: rw [← Set.subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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)
⊢ False
have H : Set.range (ι := ↥Y) ⇑g ⊆ (↑(Scheme.Hom.opensRange (X.affineCover.f i)) : Set ↥X)
Tactic: apply hxU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
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 (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)
have this₁ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ IsClosedImmersion g
have obtain : ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R) (hg : g ≫ f = 𝟙 Y), IsClosedImmersion g
Tactic: obtain ⟨R, rfl⟩ := hX
Cleared hypotheses: X, f, g, hg, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
⊢ IsClosedImmersion g
have 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
Tactic: wlog hY : ∃ S, Y = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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
⊢ IsClosedImmersion g
have 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
Tactic: wlog hY : ∃ S, Y = Spec S
Cleared hypotheses: Y, inst, R, f, g, hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
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
⊢ IsClosedImmersion g
have inst : Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))
Tactic: have inst := (Scheme.isoSpec Y).inv.homeomorph.injective.subsingleton
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
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, ⊤))
⊢ IsClosedImmersion g
have inr : IsClosedImmersion (Y.isoSpec.inv ≫ g)
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (Scheme.isoSpec Y).inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
Y : Scheme
inst : Subsingleton.{u + 1} ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
hY : ∃ (S : CommRingCat.{u}), Y = Spec S
⊢ IsClosedImmersion g
have obtain : ∀ (S : CommRingCat.{u}) [Subsingleton.{u + 1} ↥(Spec S)] (f : Spec R ⟶ Spec S) (g : Spec S ⟶ Spec R)
  (hg : g ≫ f = 𝟙 (Spec S)), IsClosedImmersion g
Tactic: obtain ⟨S, rfl⟩ := hY
Cleared hypotheses: Y, inst, f, g, hg, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
f : Spec R ⟶ Spec S
g : Spec S ⟶ Spec R
hg : g ≫ f = 𝟙 (Spec S)
⊢ IsClosedImmersion g
have obtain : ∀ (φ : S ⟶ R) (hg : g ≫ Spec.map φ = 𝟙 (Spec S)), IsClosedImmersion g
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
g : Spec S ⟶ Spec R
φ : S ⟶ R
hg : g ≫ Spec.map φ = 𝟙 (Spec S)
⊢ IsClosedImmersion g
have obtain : ∀ (ψ : R ⟶ S) (hg : Spec.map ψ ≫ Spec.map φ = 𝟙 (Spec S)), IsClosedImmersion (Spec.map ψ)
Tactic: obtain ⟨ψ, rfl⟩ := Spec.map_surjective g
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (hypothesis)
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : Spec.map ψ ≫ Spec.map φ = 𝟙 (Spec S)
⊢ IsClosedImmersion (Spec.map ψ)
have hg₁ : φ ≫ ψ = 𝟙 S
Tactic: rw [← Spec.map_comp, ← Spec.map_id, Spec.map_injective.eq_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : φ ≫ ψ = 𝟙 S
⊢ IsClosedImmersion (Spec.map ψ)
have h : Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) ψ) :
    (a : (↑R : Type u)) → (↑S : Type u))
Tactic: apply IsClosedImmersion.spec_of_surjective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion (goal)
Goal:
R S : CommRingCat
inst : Subsingleton.{u + 1} ↥(Spec S)
φ : S ⟶ R
ψ : R ⟶ S
hg : φ ≫ ψ = 𝟙 S
⊢ Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) ψ) :
      (a : (↑R : Type u)) → (↑S : Type u))
have h : Function.LeftInverse (α := (↑S : Type u)) (β := (↑R : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) ψ) :
    (a : (↑R : Type u)) → (↑S : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) φ) :
    (a : (↑S : Type u)) → (↑R : Type u))
Tactic: apply Function.LeftInverse.surjective (g := φ)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
⊢ (toProperty fun {X x : Scheme.{u_1}} (f : X ⟶ x) (x_1 : IsAffine x) ↦
      ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)).RespectsIso
have h₁ : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z],
  (∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
      [IsOpenImmersion f₁] [IsOpenImmersion f₂],
      P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)) →
    ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
      [IsOpenImmersion f₁] [IsOpenImmersion f₂],
      P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ e.hom ≫ f) (f₂ ≫ e.hom ≫ f)) (pullback.mapDesc f₁ f₂ (e.hom ≫ f))
Tactic: apply AffineTargetMorphismProperty.respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
h₁ :
  ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z],
    (∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ e.hom ≫ f) (f₂ ≫ e.hom ≫ f)) (pullback.mapDesc f₁ f₂ (e.hom ≫ f))
⊢ (toProperty fun {X x : Scheme.{u_1}} (f : X ⟶ x) (x_1 : IsAffine x) ↦
      ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
        [IsOpenImmersion f₁] [IsOpenImmersion f₂],
        P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)).RespectsIso
have h₂ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
  (∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
      [IsOpenImmersion f₁] [IsOpenImmersion f₂],
      P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)) →
    ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
      [IsOpenImmersion f₁] [IsOpenImmersion f₂],
      P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f ≫ e.hom) (f₂ ≫ f ≫ e.hom)) (pullback.mapDesc f₁ f₂ (f ≫ e.hom))
Tactic: apply AffineTargetMorphismProperty.respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
inst_1 : IsAffine Z
H :
  ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst : IsAffine U₁] [inst_6 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_2 : IsAffine U₁
inst_3 : IsAffine U₂
inst_4 : IsOpenImmersion f₁
inst_5 : IsOpenImmersion f₂
⊢ P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ e.hom ≫ f) (f₂ ≫ e.hom ≫ f)) (pullback.mapDesc f₁ f₂ (e.hom ≫ f))
have h₁ : P (X := pullback (f₁ ≫ e.hom) (f₂ ≫ e.hom)) (Y := pullback ((f₁ ≫ e.hom) ≫ f) ((f₂ ≫ e.hom) ≫ f))
  (pullback.mapDesc (f₁ ≫ e.hom) (f₂ ≫ e.hom) f)
Tactic: rw [pullback.mapDesc_comp, P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : AffineTargetMorphismProperty
inst : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
inst_1 : IsAffine Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u_1}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_6 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_2 : IsAffine U₁
inst_3 : IsAffine U₂
inst_4 : IsOpenImmersion f₁
inst_5 : IsOpenImmersion f₂
⊢ P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f ≫ e.hom) (f₂ ≫ f ≫ e.hom)) (pullback.mapDesc f₁ f₂ (f ≫ e.hom))
have h₂ : P (X := pullback f₁ f₂) (Y := pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f)
Tactic: rw [pullback.mapDesc_comp, P.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : 𝒱.I₀
⊢ IsAffine.{u} (𝒱.X i)
have dsimp : IsAffine.{u}
  (pullback
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰' (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
        i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀).1 ≫
      pullback.snd f (𝒰.f (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰' (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀))))
        i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀).2 ≫
      pullback.snd f (𝒰.f (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒰' i).I₀ × (𝒰' i).I₀)))))
Tactic: dsimp [𝒱]