awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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 ⋯ }
⊢ Membership.mem (γ := Set ↥X)
      (⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑R : Type u))))
      x ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑R : Type u))) ⊆
      (↑U : Set ↥X)

Tactic:
exact ⟨⟨_, hr, congr(($(e.hom_inv_id).base ⟨x, hxV⟩).1)⟩, Set.image_subset_iff.mpr hr'⟩
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
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
⊢ Scheme

Tactic:
apply LocallyRingedSpace.IsOpenImmersion.scheme (toLocallyRingedSpace _ f)

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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)
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' := ⋯ : 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
⊢ ∃ (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⟩

Premises used: AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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
refine_2 :
  LocallyRingedSpace.IsOpenImmersion (Y := toLocallyRingedSpace Y.toLocallyRingedSpace f)
    (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom' h₂)
⊢ ∃ (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:
refine ⟨R, LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom _ f) _ h₂, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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.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
⊢ 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:
rw [LocallyRingedSpace.IsOpenImmersion.lift_range]

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_range
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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.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:
h₁

Premises used: Set.Mem, setOf, Set.preimage, Set.range
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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.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:
exact h₁
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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)
⊢ LocallyRingedSpace.IsOpenImmersion.{u} (X := Spec.toLocallyRingedSpace.obj (op R)) (Y :=
    toLocallyRingedSpace Y.toLocallyRingedSpace f)
    (have this :
      IsIso (X :=
        pullback (X := toLocallyRingedSpace Y.toLocallyRingedSpace f) (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f)
          i.toLRSHom')
        (pullback.snd (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom') :=
      ⋯;
    CategoryStruct.comp (Y :=
      pullback (X := toLocallyRingedSpace Y.toLocallyRingedSpace f) (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f)
        i.toLRSHom')
      (inv (pullback.snd (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom'))
      (pullback.fst (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom'))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ (toScheme Y f).toLocallyRingedSpace = toLocallyRingedSpace Y.toLocallyRingedSpace f

Tactic:
rfl

Premises used: rfl, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ Hom.toPshHom (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (toSchemeHom Y f))) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ AlgebraicGeometry.IsOpenImmersion (X := toScheme Y f) (toSchemeHom Y f)

Tactic:
H
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace
mk :
  ∀ (toLocallyRingedSpace : LocallyRingedSpace.{u})
    (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
⊢ X = Y

Tactic:
cases X
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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
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 ⋯ ≅ 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 }
⊢ { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine : Scheme.{u} } = Y

Tactic:
cases Y
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
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))
toLocallyRingedSpace_1 : LocallyRingedSpace
local_affine_1 :
  ∀ (x : (↑toLocallyRingedSpace_1.toTopCat : Type u)),
    ∃ (U : OpenNhds x) (R : CommRingCat.{u}),
      Nonempty.{u + 1} (toLocallyRingedSpace_1.restrict ⋯ ≅ 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:
congr
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : AlgebraicGeometry.IsOpenImmersion f
H : (toScheme Y f.toPshHom).toLocallyRingedSpace = X.toLocallyRingedSpace
⊢ toScheme Y f.toPshHom = X

Tactic:
apply scheme_eq_of_locallyRingedSpace_eq

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_eq_of_locallyRingedSpace_eq
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : AlgebraicGeometry.IsOpenImmersion f
⊢ (toScheme Y f.toPshHom).toLocallyRingedSpace = X.toLocallyRingedSpace

Tactic:
locallyRingedSpace_toLocallyRingedSpace f.toLRSHom

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : AlgebraicGeometry.IsOpenImmersion f
⊢ (toScheme Y f.toPshHom).toLocallyRingedSpace = X.toLocallyRingedSpace

Tactic:
exact locallyRingedSpace_toLocallyRingedSpace f.toLRSHom

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.locallyRingedSpace_toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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))
⊢ (X.restrict h).toPresheafedSpace = X.restrict h

Tactic:
rfl

Premises used: AlgebraicGeometry.PresheafedSpace.restrict, rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
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
⊢ Hom.app (X.ofRestrict h) V = X.presheaf.map (⋯.adjunction.counit.app V).op

Tactic:
rfl

Premises used: Set.Mem, rfl