awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : HasColimits.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_4 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_5 : Functor.ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_7 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
H :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    IsIso (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type v)
inst :
  ∀ (x : ↥(hf.functor.obj U)),
    IsIso (X :=
      Functor.obj (TopCat.Presheaf.stalkFunctor C (↑x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        (Y.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
      (Y :=
      Functor.obj (TopCat.Presheaf.stalkFunctor C (↑x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        ((Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf).obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
      (CategoryTheory.Functor.map (TopCat.Presheaf.stalkFunctor C (↑x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
        (InducedCategory.Hom.hom
          (have this : Y.sheaf ⟶ Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf := { hom := f.hom.c };
          this)))
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U))) (f.hom.c.app (op (hf.functor.obj U)))

Tactic:
apply +allowSynthFailures TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso
          (show Y.sheaf ⟶ (TopCat.Sheaf.pushforward _ f.hom.base).obj X.sheaf from ⟨f.hom.c⟩)

Premises used: TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso, CategoryTheory.InducedCategory.Hom.mk, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
inst_2 : HasColimits.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_3 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : Functor.ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
H :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    IsIso (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type v)
y : (↑(↑X.toPresheafedSpace : TopCat) : Type v)
hy : y ∈ (↑U : Set (↑(↑X.toPresheafedSpace : TopCat) : Type v))
⊢ IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    (PresheafedSpace.Hom.stalkMap f.hom y)

Tactic:
specialize H y
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
inst_2 : HasColimits.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_3 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : Functor.ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type v)
y : (↑(↑X.toPresheafedSpace : TopCat) : Type v)
hy : y ∈ (↑U : Set (↑(↑X.toPresheafedSpace : TopCat) : Type v))
H :
  IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    (CategoryTheory.Functor.map
        (TopCat.Presheaf.stalkFunctor C
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            y))
        f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
⊢ IsIso (X :=
    (Functor.obj (TopCat.Presheaf.pushforward C f.hom.base) X.presheaf).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)

Tactic:
haveI H' := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing C
        hf.toIsInducing X.presheaf y
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
inst_2 : HasColimits.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_3 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : Functor.ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type v)
y : (↑(↑X.toPresheafedSpace : TopCat) : Type v)
hy : y ∈ (↑U : Set (↑(↑X.toPresheafedSpace : TopCat) : Type v))
H :
  IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    (CategoryTheory.Functor.map
        (TopCat.Presheaf.stalkFunctor C
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            y))
        f.hom.c ≫
      TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
H' :
  IsIso (X :=
    (Functor.obj (TopCat.Presheaf.pushforward C f.hom.base) X.presheaf).stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y)
⊢ IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        y))
    ((CategoryTheory.Functor.map
          (TopCat.Presheaf.stalkFunctor C
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) f.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
              y))
          f.hom.c ≫
        TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y) ≫
      inv (TopCat.Presheaf.stalkPushforward C f.hom.base X.presheaf y))

Tactic:
have := IsIso.comp_isIso' H (@IsIso.inv_isIso _ _ _ _ _ H')
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ CategoryStruct.comp (Y := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := f.hom.base) ⋯)
      (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := f.hom.base) ⋯)
      (Y.ofRestrict ⋯ : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := f.hom.base) ⋯ ⟶ Y) =
    f

Tactic:
InducedCategory.hom_ext
    (PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict f.hom)

Premises used: CategoryTheory.InducedCategory.hom_ext, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Eq (α := Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := f.hom.base) ⋯ ⟶ Y)
    (Iso.inv (isoRestrict f) ≫ f : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := f.hom.base) ⋯ ⟶ Y)
    (Y.ofRestrict ⋯ : Y.restrict (U := (↑X.toPresheafedSpace : TopCat)) (f := f.hom.base) ⋯ ⟶ Y)

Tactic:
InducedCategory.hom_ext
    (PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict f.hom)

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict, CategoryTheory.InducedCategory.hom_ext, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑(↑X.toPresheafedSpace : TopCat) : 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.hom i

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

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
⊢ (Opens.map f.hom.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq, TopologicalSpace.Opens.map, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
⊢ Eq (α := Y.presheaf.obj (op ((opensFunctor f).obj U)) ⟶ X.presheaf.obj (op U)) (inv (invApp f U))
    (f.hom.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯))

Tactic:
PresheafedSpace.IsOpenImmersion.inv_invApp f.hom U

Premises used: AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp, CategoryTheory.InducedCategory.Hom.hom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_invApp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
⊢ op U = (Opens.map f.hom.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq, TopologicalSpace.Opens.map, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
⊢ Eq (α :=
    X.presheaf.obj (op U) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C f.hom.base) X.presheaf).obj (op ((opensFunctor f).obj U)))
    (invApp f U ≫ f.hom.c.app (op ((opensFunctor f).obj U))) (X.presheaf.map (eqToHom ⋯))

Tactic:
PresheafedSpace.IsOpenImmersion.invApp_app f.hom U

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ Y.presheaf.obj (op ((opensFunctor f).obj ((Opens.map f.hom.base).obj U))))
    (f.hom.c.app (op U) ≫ invApp f ((Opens.map f.hom.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.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) f.hom.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.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) f.hom.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.hom U

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y.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.hom.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.hom.base).obj U))))
    (f.hom.c.app (op U) ≫ invApp f ((Opens.map f.hom.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.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) f.hom.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.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) f.hom.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.hom U

Premises used: Eq.mpr, Set.Mem, CategoryTheory.eqToHom, setOf, Set.Subset, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp, Set.image, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : SheafedSpace.{u, v, ?u.314403} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : SheafedSpace.{u, v, w} C
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:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SheafedSpace.{u_1, v_1, w} C
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.PresheafedSpace.ofRestrict, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp, AlgebraicGeometry.PresheafedSpace.restrict
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.hom.base
⊢ IsIso (X := Functor.obj forgetToPresheafedSpace X) (CategoryTheory.Functor.map forgetToPresheafedSpace f)

Tactic:
haveI : IsIso (forgetToPresheafedSpace.map f) := PresheafedSpace.IsOpenImmersion.to_iso f.hom
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.hom.base
this : IsIso (X := Functor.obj forgetToPresheafedSpace X) (CategoryTheory.Functor.map forgetToPresheafedSpace f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso _ (SheafedSpace.forgetToPresheafedSpace)

Premises used: CategoryTheory.isIso_of_reflects_iso, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
H : IsOpenImmersion f
inst_1 : HasColimits.{v, u} C
x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)
⊢ IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
        x))
    (PresheafedSpace.Hom.stalkMap f.hom x)

Tactic:
PresheafedSpace.IsOpenImmersion.stalk_iso f.hom x

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso, CategoryTheory.InducedCategory.Hom.hom