awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
⊢ IsIso (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (pullback f g)))
    (CategoryStruct.comp (Y :=
      pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))
      (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g))
      (pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g)))

Tactic:
exact IsIso.comp_isIso' inferInstance <|
    PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset _ _ H'

Premises used: inferInstance, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
⊢ lift f g H' ≫ f = g

Tactic:
simp [lift, pullback.condition]

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
l : Y ⟶ X
hl : l ≫ f = g
rw : l ≫ f = lift f g H' ≫ f
rw₁ : g = lift f g H' ≫ f
rw₂ rw₃ : g = g
⊢ l = lift f g H'

Tactic:
rw [← cancel_mono f, hl, lift_fac]

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac, CategoryTheory.cancel_mono
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
⊢ IsIso (X := pullback f g) (pullback.snd f g)

Tactic:
have := pullback_snd_isIso_of_range_subset f g H'
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
this : IsIso (X := pullback f g) (pullback.snd f g)
⊢ Eq (α := (↑(pullback f g).toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat))
    (CategoryStruct.comp (Y :=
      pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))
      (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g))
      (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)))
    (PresheafedSpace.Hom.base (Hom.toHom (pullback.fst f g)))

Tactic:
have : _ = (pullback.fst f g).base :=
    PreservesPullback.iso_hom_fst
      (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
this_1 : IsIso (X := pullback f g) (pullback.snd f g)
this :
  Eq (α := (↑(pullback f g).toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat))
    (CategoryStruct.comp (Y :=
      pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))
      (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g))
      (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)))
    (PresheafedSpace.Hom.base (Hom.toHom (pullback.fst f g)))
⊢ Epi (Y :=
    pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
      ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))
    (CategoryStruct.comp (Y := (↑(pullback f g).toPresheafedSpace : TopCat))
      (inv ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map (pullback.snd f g)))
      (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g)))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) (Y :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
          TopCat.carrier) f.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
stalk_iso : ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)), IsIso (Hom.stalkMap f x)
⊢ IsOpenImmersion f

Tactic:
SheafedSpace.IsOpenImmersion.of_stalk_iso _ hf (H := stalk_iso)

Premises used: AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
a :
  forgetToSheafedSpace.map
      (CategoryStruct.comp (Y := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
        (Iso.hom (isoRestrict f) :
          X ⟶ Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
        (Y.ofRestrict ⋯ : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯ ⟶ Y)) =
    forgetToSheafedSpace.map f
⊢ CategoryStruct.comp (Y := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
      (Iso.hom (isoRestrict f) :
        X ⟶ Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
      (Y.ofRestrict ⋯ : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯ ⟶ Y) =
    f

Tactic:
apply LocallyRingedSpace.forgetToSheafedSpace.map_injective

Premises used: AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ forgetToSheafedSpace.map
      (CategoryStruct.comp (Y := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
        (Iso.hom (isoRestrict f) :
          X ⟶ Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
        (Y.ofRestrict ⋯ : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯ ⟶ Y)) =
    forgetToSheafedSpace.map f

Tactic:
SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict f.toShHom

Premises used: Set.Mem, CategoryTheory.InducedCategory.homMk, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ forgetToSheafedSpace.map
      (CategoryStruct.comp (Y := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
        (Iso.hom (isoRestrict f) :
          X ⟶ Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯)
        (Y.ofRestrict ⋯ : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯ ⟶ Y)) =
    forgetToSheafedSpace.map f

Tactic:
exact SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict f.toShHom

Premises used: AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Eq (α := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯ ⟶ Y)
    (Iso.inv (isoRestrict f) ≫ f :
      Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯ ⟶ Y)
    (Y.ofRestrict ⋯ : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := (Hom.toShHom f).hom.base) ⋯ ⟶ Y)

Tactic:
simp only [← isoRestrict_hom_ofRestrict f, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑X.toTopCat : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
PresheafedSpace.IsOpenImmersion.inv_naturality f.1 i

Premises used: Set.Mem, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑X.toTopCat : Type u_1)
⊢ IsIso (Y := Y.presheaf.obj (op ((opensFunctor f).obj U)))
    (PresheafedSpace.IsOpenImmersion.invApp f.toHom U :
      X.presheaf.obj (op U) ⟶ Y.presheaf.obj (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toHom).obj U)))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑X.toTopCat : Type u_1)
⊢ Set.preimage (β := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (Hom.toShHom f).hom.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (Hom.toShHom f).hom.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ''
        U.carrier) =
    U.carrier

Tactic:
have := Set.preimage_image_eq U.1 H.base_open.injective
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑X.toTopCat : Type u_1)
this :
  Set.preimage (β := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) f.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ''
        (↑U : Set (↑X.toTopCat : Type u_1))) =
    (↑U : Set (↑X.toTopCat : Type u_1))
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
simp [Opens.map, this]

Premises used: TopologicalSpace.Opens.map
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑X.toTopCat : Type u_1)
⊢ Eq (α := Y.presheaf.obj (op ((opensFunctor f).obj U)) ⟶ X.presheaf.obj (op U)) (inv (invApp f U))
    (f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯))

Tactic:
PresheafedSpace.IsOpenImmersion.inv_invApp f.1 U

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑X.toTopCat : Type u_1)
this :
  Set.preimage (β := (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) f.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ''
        (↑U : Set (↑X.toTopCat : Type u_1))) =
    (↑U : Set (↑X.toTopCat : Type u_1))
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
simp [Opens.map, this]

Premises used: TopologicalSpace.Opens.map
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑X.toTopCat : Type u_1)
⊢ Eq (α :=
    X.presheaf.obj (op U) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward CommRingCat f.base) X.presheaf).obj (op ((opensFunctor f).obj U)))
    (invApp f U ≫ f.c.app (op ((opensFunctor f).obj U))) (X.presheaf.map (eqToHom ⋯))

Tactic:
PresheafedSpace.IsOpenImmersion.invApp_app f.1 U

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑Y.toTopCat : Type u_1)
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ Y.presheaf.obj (op ((opensFunctor f).obj ((Opens.map f.base).obj U))))
    (f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U))
    (Y.presheaf.map
      (Quiver.Hom.op (X :=
        Set.image (α := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) f.base) :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ⁻¹'
            U.carrier))
        (Y := U.carrier)
        (homOfLE (x :=
          Set.image (α := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) f.base) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ⁻¹'
              U.carrier))
          (y := U.carrier) ⋯)))

Tactic:
PresheafedSpace.IsOpenImmersion.app_invApp f.1 U

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑Y.toTopCat : Type u_1)
hU :
  (↑U : Set (↑Y.toTopCat : Type u_1)) ⊆
    Set.range (ι := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ Y.presheaf.obj (op ((opensFunctor f).obj ((Opens.map f.base).obj U))))
    (f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U))
    (Y.presheaf.map
      (Quiver.Hom.op (X :=
        Set.image (α := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) f.base) :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ⁻¹'
            U.carrier))
        (Y := U.carrier)
        (eqToHom (X :=
          Set.image (α := (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) f.base) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) ⁻¹'
              U.carrier))
          (Y := U.carrier) ⋯)))

Tactic:
PresheafedSpace.IsOpenImmersion.app_invApp f.1 U

Premises used: Eq.mpr, Set.Mem, CategoryTheory.eqToHom, setOf, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, Set.Subset, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, Set.image
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : LocallyRingedSpace
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : LocallyRingedSpace
f : X ⟶ (↑Y.toPresheafedSpace : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type w))
⊢ IsOpenImmersion (Y.ofRestrict hf)

Tactic:
PresheafedSpace.IsOpenImmersion.ofRestrict _ hf

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict, AlgebraicGeometry.PresheafedSpace.ofRestrict, AlgebraicGeometry.PresheafedSpace.restrict
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X : LocallyRingedSpace
Y : TopCat
f : Y ⟶ TopCat.of (↑(↑X.toPresheafedSpace : TopCat) : Type w)
h :
  IsOpenEmbedding (X := (↑Y : Type w)) (Y := (↑(TopCat.of (↑(↑X.toPresheafedSpace : TopCat) : Type w)) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑Y : Type w)) → (↑(TopCat.of (↑(↑X.toPresheafedSpace : TopCat) : Type w)) : Type w))
U : Opens (↑(↑(X.restrict h).toPresheafedSpace : TopCat) : Type w)
⊢ Eq (α := (X.restrict h).presheaf.obj (op U) ⟶ X.presheaf.obj (op ((opensFunctor (X.ofRestrict h)).obj U)))
    (invApp (X.ofRestrict h) U) (𝟙 ((X.restrict h).presheaf.obj (op U)))

Tactic:
PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ h U

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp, AlgebraicGeometry.PresheafedSpace.ofRestrict, AlgebraicGeometry.PresheafedSpace.restrict
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
x : (↑X.toTopCat : Type u_1)
⊢ IsIso (Hom.stalkMap f x)

Tactic:
PresheafedSpace.IsOpenImmersion.stalk_iso f.1 x

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst : Epi f.base
rw : IsIso (forgetToSheafedSpace.map f)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ LocallyRingedSpace.forgetToSheafedSpace]

Premises used: AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.isIso_iff_of_reflects_iso