awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (hypothesis)
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens (↑X.toTopCat : Type u)
hxV : x ∈ V
R : CommRingCat
e :
  X.restrict (U :=
      Functor.obj (Opens.toTopCat X.toTopCat)
        (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
          TopologicalSpace.Opens (↑X.toTopCat : Type u)))
      ⋯ ≅
    Spec.toLocallyRingedSpace.obj (op R)
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
have this : Membership.mem (α := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
  ((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          e.hom.base :
        (a : (↑(↑(X.restrict sorry).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
      (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
        x_1 ∈
          (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
            TopologicalSpace.Opens (↑X.toTopCat : Type u)))
        x hxV) :
    (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
Tactic: have : e.hom.base ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U :=
    show ((e.hom ≫ e.inv).base ⟨x, hxV⟩).1 ∈ U from e.hom_inv_id ▸ hxU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens (↑X.toTopCat : Type u)
hxV : x ∈ V
R : CommRingCat
e :
  X.restrict (U :=
      Functor.obj (Opens.toTopCat X.toTopCat)
        (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
          TopologicalSpace.Opens (↑X.toTopCat : Type u)))
      ⋯ ≅
    Spec.toLocallyRingedSpace.obj (op R)
this :
  Membership.mem (α := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
    ((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            e.hom.base :
          (a : (↑(↑(X.restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
        (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
          x_1 ∈
            (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
              TopologicalSpace.Opens (↑X.toTopCat : Type u)))
          x hxV) :
      (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
have obtain : ∀ (r : (↑R : Type u))
  (hr :
    Membership.mem (α := PrimeSpectrum (↑(unop (op R)) : Type u))
      (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(unop (op R)) : Type u)))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              e.hom.base :
            (a : (↑(↑(X.restrict sorry).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
            x_1 ∈
              (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
                TopologicalSpace.Opens (↑X.toTopCat : Type u)))
            x hxV) :
        (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)))
  (hr' :
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(unop (op R)) : Type u))) ⊆
      (↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U) :
        Set (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))),
  ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
Tactic: obtain ⟨_, ⟨_, ⟨r : R, rfl⟩, rfl⟩, hr, hr'⟩ :=
    PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open this (Opens.is_open' _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens (↑X.toTopCat : Type u)
hxV : x ∈ V
R : CommRingCat
e :
  X.restrict (U :=
      Functor.obj (Opens.toTopCat X.toTopCat)
        (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
          TopologicalSpace.Opens (↑X.toTopCat : Type u)))
      ⋯ ≅
    Spec.toLocallyRingedSpace.obj (op R)
this :
  Membership.mem (α := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
    ((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            e.hom.base :
          (a : (↑(↑(X.restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
        (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
          x_1 ∈
            (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
              TopologicalSpace.Opens (↑X.toTopCat : Type u)))
          x hxV) :
      (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
r : (↑R : Type u)
hr :
  Membership.mem (α := PrimeSpectrum (↑(unop (op R)) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(unop (op R)) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            e.hom.base :
          (a : (↑(↑(X.restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
        (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
          x_1 ∈
            (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
              TopologicalSpace.Opens (↑X.toTopCat : Type u)))
          x hxV) :
      (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
hr' :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(unop (op R)) : Type u))) ⊆
    (↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U) :
      Set (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  CategoryStruct.comp (Y := Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))))
    { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
have refine : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away r)))) ⇑f) x ∧
  Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away r)))) ⇑f ⊆ (↑U : Set ↥X)
Tactic: refine ⟨.of (Localization.Away r), f, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ Scheme
have apply : ∀ (x : (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat : Type u)),
  ∃ (R : CommRingCat.{u}) (f_1 : Spec.toLocallyRingedSpace.obj (op R) ⟶ toLocallyRingedSpace Y.toLocallyRingedSpace f),
    Membership.mem (γ := Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f_1.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)))
        x ∧
      LocallyRingedSpace.IsOpenImmersion f_1
Tactic: apply LocallyRingedSpace.IsOpenImmersion.scheme (toLocallyRingedSpace _ f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat : Type u)
⊢ ∃ (R : CommRingCat.{u}) (f_1 : Spec.toLocallyRingedSpace.obj (op R) ⟶ toLocallyRingedSpace Y.toLocallyRingedSpace f),
    Membership.mem (γ := Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f_1.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)))
        x ∧
      LocallyRingedSpace.IsOpenImmersion f_1
have obtain : ∀ (R : CommRingCat.{u}) (i : Spec R ⟶ Y),
  AlgebraicGeometry.IsOpenImmersion i →
    ∀
      (h₁ :
        Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.range (ι := ↥(Spec R)) ⇑i)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  f.base :
                (a : (↑(↑X : TopCat) : Type u)) → ↥Y)
              x :
            ↥Y))
      (h₂ :
        Set.range (ι := ↥(Spec R)) ⇑i ⊆
          (↑{
                carrier :=
                  Set.range (ι := (↑(↑X : TopCat) : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) f.base) :
                      (a : (↑(↑X : TopCat) : Type u)) → ↥Y),
                is_open' := sorry : Opens ↥Y } :
            Set ↥Y)),
      ∃ (R : CommRingCat.{u}) (f_1 :
        Spec.toLocallyRingedSpace.obj (op R) ⟶ toLocallyRingedSpace Y.toLocallyRingedSpace f),
        Membership.mem (γ :=
            Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
            (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f_1.base) :
                (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)))
            x ∧
          LocallyRingedSpace.IsOpenImmersion f_1
Tactic: obtain ⟨R, i, _, h₁, h₂⟩ :=
    Scheme.exists_affine_mem_range_and_range_subset (U := ⟨_, H.base_open.isOpen_range⟩) ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat : Type u)
R : CommRingCat
i : Spec R ⟶ Y
left : AlgebraicGeometry.IsOpenImmersion i
h₁ :
  Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.range (ι := ↥(Spec R)) ⇑i)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base :
          (a : (↑(↑X : TopCat) : Type u)) → ↥Y)
        x :
      ↥Y)
h₂ :
  Set.range (ι := ↥(Spec R)) ⇑i ⊆
    (↑{
          carrier :=
            Set.range (ι := (↑(↑X : TopCat) : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base) :
                (a : (↑(↑X : TopCat) : Type u)) → ↥Y),
          is_open' := ⋯ : Opens ↥Y } :
      Set ↥Y)
⊢ ∃ (R : CommRingCat.{u}) (f_1 : Spec.toLocallyRingedSpace.obj (op R) ⟶ toLocallyRingedSpace Y.toLocallyRingedSpace f),
    Membership.mem (γ := Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f_1.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)))
        x ∧
      LocallyRingedSpace.IsOpenImmersion f_1
have refine_1 : Membership.mem (γ := Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
  (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (Y := (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat))
          (Hom.base
            (LocallyRingedSpace.Hom.toHom
              (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom'
                h₂)))) :
      (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
        (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)))
  x
Tactic: refine ⟨R, LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom _ f) _ h₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat : Type u)
R : CommRingCat
i : Spec R ⟶ Y
left : AlgebraicGeometry.IsOpenImmersion i
h₁ :
  Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.range (ι := ↥(Spec R)) ⇑i)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base :
          (a : (↑(↑X : TopCat) : Type u)) → ↥Y)
        x :
      ↥Y)
h₂ :
  Set.range (ι := ↥(Spec R)) ⇑i ⊆
    (↑{
          carrier :=
            Set.range (ι := (↑(↑X : TopCat) : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base) :
                (a : (↑(↑X : TopCat) : Type u)) → ↥Y),
          is_open' := ⋯ : Opens ↥Y } :
      Set ↥Y)
refine_1 :
  Membership.mem (γ := Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Y := (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat))
            (Hom.base
              (LocallyRingedSpace.Hom.toHom
                (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom'
                  h₂)))) :
        (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)))
    x
⊢ ∃ (R : CommRingCat.{u}) (f_1 : Spec.toLocallyRingedSpace.obj (op R) ⟶ toLocallyRingedSpace Y.toLocallyRingedSpace f),
    Membership.mem (γ := Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f_1.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)))
        x ∧
      LocallyRingedSpace.IsOpenImmersion f_1
have refine_2 : LocallyRingedSpace.IsOpenImmersion (Y := toLocallyRingedSpace Y.toLocallyRingedSpace f)
  (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom' h₂)
Tactic: refine ⟨R, LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom _ f) _ h₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat : Type u)
R : CommRingCat
i : Spec R ⟶ Y
left : AlgebraicGeometry.IsOpenImmersion i
h₁ :
  Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.range (ι := ↥(Spec R)) ⇑i)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base :
          (a : (↑(↑X : TopCat) : Type u)) → ↥Y)
        x :
      ↥Y)
h₂ :
  Set.range (ι := ↥(Spec R)) ⇑i ⊆
    (↑{
          carrier :=
            Set.range (ι := (↑(↑X : TopCat) : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base) :
                (a : (↑(↑X : TopCat) : Type u)) → ↥Y),
          is_open' := ⋯ : Opens ↥Y } :
      Set ↥Y)
⊢ Membership.mem (γ := Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Y := (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat))
            (Hom.base
              (LocallyRingedSpace.Hom.toHom
                (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom'
                  h₂)))) :
        (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)))
    x
have refine_1 : Membership.mem (γ := Set (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u))
  (Set.preimage (β := ↥Y)
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat))
          (Hom.base (LocallyRingedSpace.Hom.toHom (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f)))) :
      (a : (↑(↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toPresheafedSpace : TopCat) : Type u)) → ↥Y)
    (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) ⇑i))
  x
Tactic: rw [LocallyRingedSpace.IsOpenImmersion.lift_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace
⊢ X = Y
have mk : ∀ (toLocallyRingedSpace : LocallyRingedSpace.{u})
  (local_affine :
    ∀ (x : (↑toLocallyRingedSpace.toTopCat : Type u)),
      ∃ (U : OpenNhds x) (R : CommRingCat.{u}),
        Nonempty.{u + 1} (toLocallyRingedSpace.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
  (H :
    { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine : Scheme.{u} }.toLocallyRingedSpace =
      Y.toLocallyRingedSpace),
  { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine : Scheme.{u} } = Y
Tactic: cases X
Cleared hypotheses: X, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
Y : Scheme
toLocallyRingedSpace : LocallyRingedSpace
local_affine :
  ∀ (x : (↑toLocallyRingedSpace.toTopCat : Type u)),
    ∃ (U : OpenNhds x) (R : CommRingCat.{u}),
      Nonempty.{u + 1} (toLocallyRingedSpace.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine : Scheme.{u} }.toLocallyRingedSpace =
    Y.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine : Scheme.{u} } = Y
have mk : ∀ (toLocallyRingedSpace_1 : LocallyRingedSpace.{u})
  (local_affine_1 :
    ∀ (x : (↑toLocallyRingedSpace_1.toTopCat : Type u)),
      ∃ (U : OpenNhds x) (R : CommRingCat.{u}),
        Nonempty.{u + 1} (toLocallyRingedSpace_1.restrict sorry ≅ Spec.toLocallyRingedSpace.obj (op R)))
  (H :
    { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine : Scheme.{u} }.toLocallyRingedSpace =
      { toLocallyRingedSpace := toLocallyRingedSpace_1, local_affine := local_affine_1 }.toLocallyRingedSpace),
  { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine : Scheme.{u} } =
    { toLocallyRingedSpace := toLocallyRingedSpace_1, local_affine := local_affine_1 }
Tactic: cases Y
Cleared hypotheses: Y, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : AlgebraicGeometry.IsOpenImmersion f
⊢ toScheme Y f.toPshHom = X
have H : (toScheme Y f.toPshHom).toLocallyRingedSpace = X.toLocallyRingedSpace
Tactic: apply scheme_eq_of_locallyRingedSpace_eq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑(TopCat.of ↥X) : Type u))
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))
have dsimp : X.presheaf.map (sorry.adjunction.counit.app V).op ≫ (X.restrict h).presheaf.map (homOfLE e).op =
  X.presheaf.map (Quiver.Hom.op (homOfLE sorry))
Tactic: dsimp [Hom.appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
U_1 : TopCat
X : Scheme
f : U_1 ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U_1 : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U_1 : Type u)) → (↑(TopCat.of ↥X) : Type u))
U : (X.restrict h).Opens
⊢ Hom.appIso (X.ofRestrict h) U = Iso.refl Γ(X, X.ofRestrict h ''ᵁ U)
have w : Iso.hom (Hom.appIso (X.ofRestrict h) U) = Iso.hom (Iso.refl Γ(X, X.ofRestrict h ''ᵁ U))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion g
inst_1 : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)
have rw : IsIso (Scheme.Hom.stalkMap (f ≫ g) x)
Tactic: rw [← Scheme.Hom.stalkMap_comp]