awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
f : X ⟶ Y
H : IsOpenImmersion f
inst_1 : HasColimits.{v, u} C
x : (↑(↑X : TopCat) : Type v)
rw :
  IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
                (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
                (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)).base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x))
    (Hom.stalkMap (Y.ofRestrict ⋯)
          (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (Y := (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat))
                  (Hom.base (Iso.hom (isoRestrict f)) :
                    (↑X : TopCat) ⟶ (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat)) :
                C((↑(↑X : TopCat) : Type v),
                  (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type v))) :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑(Y.restrict ⋯) : TopCat) : Type v))
            x) ≫
        Hom.stalkMap (Iso.hom (isoRestrict f)) x :
      Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (X := (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat)) (Hom.base (Y.ofRestrict ⋯)) :
              (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (Y := (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat))
                      (Hom.base (Iso.hom (isoRestrict f)) :
                        (↑X : TopCat) ⟶ (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat)) :
                    C((↑(↑X : TopCat) : Type v),
                      (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type v))) :
                  (a : (↑(↑X : TopCat) : Type v)) → (↑(↑(Y.restrict ⋯) : TopCat) : Type v))
                x :
              (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type v))) ⟶
        X.presheaf.stalk x)
⊢ IsIso (X :=
    Y.presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            f.base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x))
    (Hom.stalkMap f x)

Tactic:
rw [← H.isoRestrict_hom_ofRestrict, PresheafedSpace.stalkMap.comp]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict, AlgebraicGeometry.PresheafedSpace.stalkMap.comp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, v} C
f : X ⟶ Y
H : IsOpenImmersion f
inst_1 : HasColimits.{v, u} C
x : (↑(↑X : 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)
            (CategoryStruct.comp (Y := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
                (Iso.hom (isoRestrict f) : X ⟶ Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯)
                (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)).base :
          (a : (↑(↑X : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
        x))
    (Hom.stalkMap (Y.ofRestrict ⋯)
          (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (Y := (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat))
                  (Hom.base (Iso.hom (isoRestrict f)) :
                    (↑X : TopCat) ⟶ (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat)) :
                C((↑(↑X : TopCat) : Type v),
                  (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type v))) :
              (a : (↑(↑X : TopCat) : Type v)) → (↑(↑(Y.restrict ⋯) : TopCat) : Type v))
            x) ≫
        Hom.stalkMap (Iso.hom (isoRestrict f)) x :
      Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (X := (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat)) (Hom.base (Y.ofRestrict ⋯)) :
              (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type v)) → (↑(↑Y : TopCat) : Type v))
            (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (Y := (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat))
                      (Hom.base (Iso.hom (isoRestrict f)) :
                        (↑X : TopCat) ⟶ (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat)) :
                    C((↑(↑X : TopCat) : Type v),
                      (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type v))) :
                  (a : (↑(↑X : TopCat) : Type v)) → (↑(↑(Y.restrict ⋯) : TopCat) : Type v))
                x :
              (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type v))) ⟶
        X.presheaf.stalk x)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
simp :
  {
      carrier :=
        (⇑(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 : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ⁻¹'
          (↑{
                carrier :=
                  (⇑(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 : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ''
                    (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
                is_open' := ⋯ : Opens (↑(↑Z : TopCat) : Type u_1) } :
            Set (↑(↑Z : TopCat) : Type u_1)),
      is_open' := ⋯ : Opens (↑(↑Y : TopCat) : Type u_1) } =
    {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) (X := pullback f.base g.base) (pullback.snd f.base g.base)) :
            (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
          (↑{
                carrier :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                          TopCat.carrier) (X := (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat))
                          (pullback.fst f.base g.base)) :
                      (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑X : TopCat) : Type u_1)) ⁻¹'
                    (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
                is_open' := ⋯ : Opens (↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1) } :
            Set (↑(pullback f.base g.base) : Type u_1)),
      is_open' := ⋯ }
⊢ (Opens.map g.base).op.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) =
    Functor.obj (Functor.op (IsOpenEmbedding.functor ⋯))
      (Functor.obj (Functor.op (Opens.map (pullback.fst f.base g.base))) U)

Tactic:
simp only [IsOpenMap.functor, op_inj_iff, Opens.map,
                    Functor.op_obj]

Premises used: IsOpenMap.functor, TopologicalSpace.Opens.map, CategoryTheory.Functor.op_obj, Opposite.op_inj_iff
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
x : (↑(pullback f.base g.base) : Type u_1)
h₁ :
  x ∈
    (↑{
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) (X := (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat))
                    (pullback.fst f.base g.base)) :
                (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑X : TopCat) : Type u_1)) ⁻¹'
              (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
          is_open' := ⋯ : Opens (↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1) } :
      Set (↑(pullback f.base g.base) : Type u_1))
⊢ Membership.mem (α := (↑(↑Y : TopCat) : Type u_1))
    {
      carrier :=
        (⇑(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 : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ⁻¹'
          (↑{
                carrier :=
                  (⇑(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 : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ''
                    (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
                is_open' := ⋯ : Opens (↑(↑Z : TopCat) : Type u_1) } :
            Set (↑(↑Z : TopCat) : Type u_1)),
      is_open' := ⋯ : Opens (↑(↑Y : 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)
            (X := pullback f.base g.base) (pullback.snd f.base g.base) :
          (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
        x :
      (↑(↑Y : TopCat) : Type u_1))

Tactic:
⟨_, h₁, CategoryTheory.congr_fun pullback.condition x⟩

Premises used: Set.Mem, setOf, CategoryTheory.congr_fun, Set.preimage, And.intro, Exists.intro, Set.image, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
x : (↑(pullback f.base g.base) : Type u_1)
h₁ :
  x ∈
    (↑{
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    TopCat.carrier) (X := (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat))
                    (pullback.fst f.base g.base)) :
                (a : (↑(↑(Y.restrict ⋯) : TopCat) : Type u_1)) → (↑(↑X : TopCat) : Type u_1)) ⁻¹'
              (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
          is_open' := ⋯ : Opens (↑(↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) : Type u_1) } :
      Set (↑(pullback f.base g.base) : Type u_1))
⊢ Membership.mem (α := (↑(↑Y : TopCat) : Type u_1))
    {
      carrier :=
        (⇑(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 : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ⁻¹'
          (↑{
                carrier :=
                  (⇑(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 : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)) ''
                    (↑(unop U) : Set (↑(↑X : TopCat) : Type u_1)),
                is_open' := ⋯ : Opens (↑(↑Z : TopCat) : Type u_1) } :
            Set (↑(↑Z : TopCat) : Type u_1)),
      is_open' := ⋯ : Opens (↑(↑Y : 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)
            (X := pullback f.base g.base) (pullback.snd f.base g.base) :
          (a : (↑(pullback f.base g.base) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
        x :
      (↑(↑Y : TopCat) : Type u_1))

Tactic:
exact ⟨_, h₁, CategoryTheory.congr_fun pullback.condition x⟩
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U V : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
op :
  ∀ (unop : Opens (↑(↑X : TopCat) : Type u_1)) (i : Opposite.op unop ⟶ V),
    X.presheaf.map i ≫
        CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop V))))
          (invApp f (Opposite.unop V))
          (g.c.app (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop V))) ≫
            Y.presheaf.map (eqToHom ⋯)) =
      CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop (Opposite.op unop)))))
          (invApp f (Opposite.unop (Opposite.op unop)))
          (g.c.app
              (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop (Opposite.op unop)))) ≫
            Y.presheaf.map (eqToHom ⋯)) ≫
        (Functor.obj (TopCat.Presheaf.pushforward C (pullback.fst f.base g.base))
              (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).map
          i
⊢ X.presheaf.map i ≫
      CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (unop V)))) (invApp f (unop V))
        (g.c.app (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop V))) ≫
          Y.presheaf.map (eqToHom ⋯)) =
    CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (unop U)))) (invApp f (unop U))
        (g.c.app (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ≫
          Y.presheaf.map (eqToHom ⋯)) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C (pullback.fst f.base g.base))
            (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).map
        i

Tactic:
induction U
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
V : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
unop : Opens (↑(↑X : TopCat) : Type u_1)
i : Opposite.op unop ⟶ V
op :
  ∀ (unop_1 : Opens (↑(↑X : TopCat) : Type u_1)) (i : Opposite.op unop ⟶ Opposite.op unop_1),
    X.presheaf.map i ≫
        CategoryStruct.comp (Y :=
          Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop (Opposite.op unop_1)))))
          (invApp f (Opposite.unop (Opposite.op unop_1)))
          (g.c.app
              (Opposite.op
                (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop (Opposite.op unop_1)))) ≫
            Y.presheaf.map (eqToHom ⋯)) =
      CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop (Opposite.op unop)))))
          (invApp f (Opposite.unop (Opposite.op unop)))
          (g.c.app
              (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop (Opposite.op unop)))) ≫
            Y.presheaf.map (eqToHom ⋯)) ≫
        (Functor.obj (TopCat.Presheaf.pushforward C (pullback.fst f.base g.base))
              (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).map
          i
⊢ X.presheaf.map i ≫
      CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop V))))
        (invApp f (Opposite.unop V))
        (g.c.app (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop V))) ≫
          Y.presheaf.map (eqToHom ⋯)) =
    CategoryStruct.comp (Y := Z.presheaf.obj (Opposite.op ((opensFunctor f).obj (Opposite.unop (Opposite.op unop)))))
        (invApp f (Opposite.unop (Opposite.op unop)))
        (g.c.app
            (Opposite.op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (Opposite.unop (Opposite.op unop)))) ≫
          Y.presheaf.map (eqToHom ⋯)) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C (pullback.fst f.base g.base))
            (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).map
        i

Tactic:
induction V
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
unop unop_1 : Opens (↑(↑X : TopCat) : Type u_1)
i : op unop ⟶ op unop_1
⊢ Eq (α :=
    X.presheaf.obj (op unop) ⟶
      Y.presheaf.obj
        (op (Functor.obj (IsOpenEmbedding.functor ⋯) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))
    (CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj unop))) (invApp f unop)
        (g.c.app (op ((opensFunctor f).obj unop)) ≫
          Y.presheaf.map (((Opens.map g.base).map ((opensFunctor f).map i.unop)).op ≫ eqToHom ⋯)) :
      X.presheaf.obj (op unop) ⟶
        Y.presheaf.obj
          (op (Functor.obj (IsOpenEmbedding.functor ⋯) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))
    (CategoryStruct.comp (Y := Z.presheaf.obj (op ((opensFunctor f).obj unop))) (invApp f unop)
        (g.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) unop)) ≫
          Y.presheaf.map
            (CategoryStruct.comp (Y :=
              op (Functor.obj (IsOpenEmbedding.functor ⋯) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)))
              (eqToHom ⋯ :
                op ((Opens.map g.base).obj (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) unop)) ⟶
                  op
                    (Functor.obj (IsOpenEmbedding.functor ⋯)
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)))
              (Quiver.Hom.op
                  (CategoryTheory.Functor.map (IsOpenEmbedding.functor ⋯)
                    (CategoryTheory.Functor.map (Opens.map (pullback.fst f.base g.base)) i.unop)) :
                op
                    (Functor.obj (IsOpenEmbedding.functor ⋯)
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop)) ⟶
                  op
                    (Functor.obj (IsOpenEmbedding.functor ⋯)
                      (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))) :
      X.presheaf.obj (op unop) ⟶
        Y.presheaf.obj
          (op (Functor.obj (IsOpenEmbedding.functor ⋯) (Functor.obj (Opens.map (pullback.fst f.base g.base)) unop_1))))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
⊢ Eq (α := Y.restrict (U := pullback f.base g.base) ⋯ ⟶ Z)
    (pullbackConeOfLeftFst f g ≫ f : Y.restrict (U := pullback f.base g.base) ⋯ ⟶ Z)
    (Y.ofRestrict ⋯ ≫ g : Y.restrict (U := pullback f.base g.base) ⋯ ⟶ Z)

Tactic:
PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun U => ?_

Premises used: CategoryTheory.NatTrans.ext, funext, AlgebraicGeometry.PresheafedSpace.Hom.ext
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
refine_1 :
  Eq (α := (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z : TopCat))
    (Hom.base (pullbackConeOfLeftFst f g ≫ f) :
      (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z : TopCat))
    (Hom.base (Y.ofRestrict ⋯ ≫ g) : (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z : TopCat))
refine_2 :
  ∀ (U : (Opens (↑(↑Z : TopCat) : Type u_1))ᵒᵖ),
    Eq (α :=
      Z.presheaf.obj U ⟶
        (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
              (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
          U)
      (NatTrans.app
          (CategoryStruct.comp (Y :=
            Functor.obj
              (TopCat.Presheaf.pushforward C (Hom.base (pullbackConeOfLeftFst f g ≫ f)) :
                TopCat.Presheaf.{u_1, v, u} C (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⥤
                  TopCat.Presheaf.{u_1, v, u} C (↑Z : TopCat))
              (Y.restrict (U := pullback f.base g.base) ⋯).presheaf)
            (Hom.c (pullbackConeOfLeftFst f g ≫ f) :
              Z.presheaf ⟶
                Functor.obj
                  (TopCat.Presheaf.pushforward C (Hom.base (pullbackConeOfLeftFst f g ≫ f)) :
                    TopCat.Presheaf.{u_1, v, u} C (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⥤
                      TopCat.Presheaf.{u_1, v, u} C (↑Z : TopCat))
                  (Y.restrict (U := pullback f.base g.base) ⋯).presheaf)
            (Functor.whiskerRight (eqToHom ⋯) (Y.restrict (U := pullback f.base g.base) ⋯).presheaf :
              Functor.op (Opens.map (Hom.base (pullbackConeOfLeftFst f g ≫ f))) ⋙
                  (Y.restrict (U := pullback f.base g.base) ⋯).presheaf ⟶
                Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
                  (Y.restrict (U := pullback f.base g.base) ⋯).presheaf))
          U :
        Z.presheaf.obj U ⟶
          (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
                (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
            U)
      (NatTrans.app (Hom.c (Y.ofRestrict ⋯ ≫ g)) U :
        Z.presheaf.obj U ⟶
          (Functor.op (Opens.map (Hom.base (Y.ofRestrict ⋯ ≫ g))) ⋙
                (Y.restrict (U := pullback f.base g.base) ⋯).presheaf).obj
            U)
⊢ Eq (α := Y.restrict (U := pullback f.base g.base) ⋯ ⟶ Z)
    (pullbackConeOfLeftFst f g ≫ f : Y.restrict (U := pullback f.base g.base) ⋯ ⟶ Z)
    (Y.ofRestrict ⋯ ≫ g : Y.restrict (U := pullback f.base g.base) ⋯ ⟶ Z)

Tactic:
refine PresheafedSpace.Hom.ext _ _ ?_ <| NatTrans.ext <| funext fun U => ?_

Premises used: CategoryTheory.NatTrans.ext, funext, AlgebraicGeometry.PresheafedSpace.Hom.ext
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
⊢ Eq (α := (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z : TopCat))
    (Hom.base (pullbackConeOfLeftFst f g ≫ f) :
      (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z : TopCat))
    (Hom.base (Y.ofRestrict ⋯ ≫ g) : (↑(Y.restrict (U := pullback f.base g.base) ⋯) : TopCat) ⟶ (↑Z : TopCat))

Tactic:
simpa using pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition