awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens (↑Y.toTopCat : Type u)
s : (↑(Y.presheaf.obj (op U)) : Type u)
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x)
            (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op ((Opens.map f.base).obj U))) : Type u)) →
            (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Y.presheaf.obj (op U)) (f.c.app (op U)) :
              (a : (↑(Y.presheaf.obj (op U)) : Type u)) →
                (↑(((Presheaf.pushforward CommRingCat f.base).obj X.presheaf).obj (op U)) : Type u))
            s :
          (↑((obj (Presheaf.pushforward CommRingCat f.base) X.presheaf).obj (op U)) : Type u)) :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u))
h :
  Membership.mem (α := (↑(↑Y.toPresheafedSpace : TopCat) : Type u)) (RingedSpace.basicOpen Y.toSheafedSpace s)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
⊢ x ∈ (↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) : Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))

Tactic:
simp only [Opens.map_coe, Set.mem_preimage, SetLike.mem_coe, toRingedSpace] at hx ⊢

Premises used: TopologicalSpace.Opens.map_coe, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, SetLike.mem_coe, Set.mem_preimage
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑X.toTopCat : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
V : Opens (↑U : Type u)
x : (↑U : Type u)
hx : x ∈ V
⊢ (X.restrict h).presheaf.germ V x hx ≫ (X.restrictStalkIso h x).hom =
    X.presheaf.germ (h.functor.obj V)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
        x)
      ⋯

Tactic:
PresheafedSpace.restrictStalkIso_hom_eq_germ X.toPresheafedSpace h V x hx

Premises used: AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑X.toTopCat : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
V : Opens (↑U : Type u)
x : (↑U : Type u)
hx : x ∈ V
⊢ X.presheaf.germ (h.functor.obj V)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
          x)
        ⋯ ≫
      (X.restrictStalkIso h x).inv =
    (X.restrict h).presheaf.germ V x hx

Tactic:
PresheafedSpace.restrictStalkIso_inv_eq_germ X.toPresheafedSpace h V x hx

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑X.toTopCat : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
V : Opens (↑U : Type u)
x : (↑U : Type u)
hx : x ∈ V
y : (↑(X.presheaf.obj (op (h.functor.obj V))) : Type u)
⊢ Eq (α := (↑((X.restrict h).presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.restrictStalkIso h x).inv :
          (a :
              (↑(X.presheaf.stalk ((ConcreteCategory.hom f : (a : (↑U : Type u)) → (↑X.toTopCat : Type u)) x)) :
                Type u)) →
            (↑((X.restrict h).presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := X.presheaf.obj (op (h.functor.obj V))) (Y :=
                X.presheaf.stalk
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) f :
                      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
                    x))
                (X.presheaf.germ (h.functor.obj V)
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) f :
                      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
                    x)
                  ⋯) :
              (a : (↑(X.presheaf.obj (op (h.functor.obj V))) : Type u)) →
                (↑(X.presheaf.stalk ((ConcreteCategory.hom f : (a : (↑U : Type u)) → (↑X.toTopCat : Type u)) x)) :
                  Type u))
            y :
          (↑(X.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
                  x)) :
            Type u)) :
      (↑((X.restrict h).presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := (X.restrict h).presheaf.stalk x) ((X.restrict h).presheaf.germ V x hx) :
          (a : (↑((X.restrict h).presheaf.obj (op V)) : Type u)) → (↑((X.restrict h).presheaf.stalk x) : Type u))
        y :
      (↑((X.restrict h).presheaf.stalk x) : Type u))

Tactic:
PresheafedSpace.restrictStalkIso_inv_eq_germ_apply X.toPresheafedSpace h V x hx y

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.SheafedSpace.toPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑X.toTopCat : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
x : (↑U : Type u)
⊢ (X.restrictStalkIso h x).inv = Hom.stalkMap (X.ofRestrict h) x

Tactic:
PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict X.toPresheafedSpace h x

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.ofRestrict, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.PresheafedSpace.restrict, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X_2 Y Z : LocallyRingedSpace
f_1 : X_2 ⟶ Y
g : Y ⟶ Z
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑X.toTopCat : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑U : Type u)) → (↑X.toTopCat : Type u))
V : Opens (↑U : Type u)
x : (↑U : Type u)
hx : x ∈ V
⊢ IsIso (Hom.stalkMap (X.ofRestrict h) x)

Tactic:
PresheafedSpace.ofRestrict_stalkMap_isIso X.toPresheafedSpace h x

Premises used: AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.ofRestrict, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.PresheafedSpace.restrict, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- 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
⊢ IsOpenImmersion f ↔ PresheafedSpace.IsOpenImmersion f.hom

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
inst_1 : LocallyRingedSpace.IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion f.toHom

Tactic:
assumption
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
symm :
  (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf ≅
    Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf
⊢ Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf ≅
    (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf

Tactic:
symm
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
app :
  (X_1 : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ) →
    (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.obj X_1 ≅
      (Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf).obj X_1
naturality :
  autoParam
    (∀ {X_1 Y_1 : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ}
      (f_1 : X_1 ⟶ Y_1),
      (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.map f_1 ≫
          Iso.hom (asIso (f.c.app (op ((opensFunctor f).obj (unop Y_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)) =
        Iso.hom (asIso (f.c.app (op ((opensFunctor f).obj (unop X_1)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)) ≫
          (Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf).map f_1)
    NatIso.ofComponents._auto_1
⊢ (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf ≅
    Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf

Tactic:
fapply NatIso.ofComponents

Premises used: CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
app : (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop U))) = U
⊢ (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.obj U ≅
    (Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf).obj U

Tactic:
refine asIso (f.c.app (op (opensFunctor f |>.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso ?_)

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor, CategoryTheory.eqToIso, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.Functor.mapIso, Opposite.unop, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U

Tactic:
?_
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
app :
  ∀ (U : Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)),
    (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop U))) = U

Tactic:
induction U with | op U => ?_

Premises used: Opposite.op
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
app :
  ∀ (carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))
    (is_open' : IsOpen carrier),
    (Opens.map f.base).op.obj
        (op
          ((opensFunctor f).obj
            (unop
              (op
                { carrier := carrier, is_open' := is_open' :
                  Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) })))) =
      op { carrier := carrier, is_open' := is_open' }
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj (unop (op U)))) = op U

Tactic:
cases U
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
is_open' : IsOpen carrier
app :
  op
      {
        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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
            (↑((opensFunctor f).obj
                  { carrier := carrier, is_open' := is_open' :
                    Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) }) :
              Set (↑(↑Y : TopCat) : Type u_1)),
        is_open' := ⋯ : Opens (↑(↑X : TopCat) : Type u_1) } =
    op { carrier := carrier, is_open' := is_open' }
⊢ (Opens.map f.base).op.obj
      (op
        ((opensFunctor f).obj
          (unop
            (op
              { carrier := carrier, is_open' := is_open' :
                Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) })))) =
    op { carrier := carrier, is_open' := is_open' }

Tactic:
dsimp only [IsOpenMap.functor, Functor.op, Opens.map]

Premises used: CategoryTheory.Functor.op, IsOpenMap.functor, TopologicalSpace.Opens.map
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
is_open' : IsOpen carrier
app :
  (⇑(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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
      (↑((opensFunctor f).obj
            { carrier := carrier, is_open' := is_open' :
              Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) }) :
        Set (↑(↑Y : TopCat) : Type u_1)) =
    carrier
⊢ op
      {
        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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
            (↑((opensFunctor f).obj
                  { carrier := carrier, is_open' := is_open' :
                    Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) }) :
              Set (↑(↑Y : TopCat) : Type u_1)),
        is_open' := ⋯ : Opens (↑(↑X : TopCat) : Type u_1) } =
    op { carrier := carrier, is_open' := is_open' }

Tactic:
congr 2
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
is_open' : IsOpen carrier
app :
  (↑{ carrier := carrier, is_open' := is_open' :
          Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) } :
      Set (↑(↑X : 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)) → (↑(↑Y : TopCat) : Type u_1)) ⁻¹'
      (↑((opensFunctor f).obj
            { carrier := carrier, is_open' := is_open' :
              Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) }) :
        Set (↑(↑Y : TopCat) : Type u_1)) =
    carrier

Tactic:
erw [Set.preimage_image_eq _ H.base_open.injective]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
carrier : Set (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1)
is_open' : IsOpen carrier
⊢ (↑{ carrier := carrier, is_open' := is_open' :
          Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1) } :
      Set (↑(↑X : TopCat) : Type u_1)) =
    carrier

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
naturality :
  Eq (α :=
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (Y.presheaf.map (Quiver.Hom.op (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) ⋯) i.unop)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V))) ≫ X.presheaf.map (eqToHom ⋯))
    ((f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom ⋯)) ≫
      X.presheaf.map ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op)
⊢ (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.map i ≫
      Iso.hom (asIso (f.c.app (op ((opensFunctor f).obj (unop V)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)) =
    Iso.hom (asIso (f.c.app (op ((opensFunctor f).obj (unop U)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C (Iso.hom (Iso.refl (↑X : TopCat)))) X.presheaf).map i

Tactic:
dsimp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
naturality :
  Eq (α :=
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (f.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ≫
        X.presheaf.map
            (Quiver.Hom.op
              ((Opens.map f.base).map (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) ⋯) i.unop))) ≫
          X.presheaf.map (eqToHom ⋯) :
      Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
        X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (f.c.app (op ((opensFunctor f).obj (unop U))) ≫
        X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op :
      Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
        X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
⊢ Eq (α :=
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (Y.presheaf.map (Quiver.Hom.op (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) ⋯) i.unop)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V))) ≫ X.presheaf.map (eqToHom ⋯))
    ((f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom ⋯)) ≫
      X.presheaf.map ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op)

Tactic:
simp only [NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_obj,
        TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op, Category.assoc]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, TopCat.Presheaf.pushforward_obj_obj, TopCat.Presheaf.pushforward_obj_map, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑(↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
naturality :
  Eq (α :=
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (f.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ≫
        X.presheaf.map
          (Quiver.Hom.op
              ((Opens.map f.base).map (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) ⋯) i.unop)) ≫
            eqToHom ⋯) :
      Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
        X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (f.c.app (op ((opensFunctor f).obj (unop U))) ≫
        X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op) :
      Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
        X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
⊢ Eq (α :=
    Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
      X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (f.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ≫
        X.presheaf.map
            (Quiver.Hom.op
              ((Opens.map f.base).map (CategoryTheory.Functor.map (IsOpenEmbedding.functor (f := f.base) ⋯) i.unop))) ≫
          X.presheaf.map (eqToHom ⋯) :
      Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
        X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))
    (f.c.app (op ((opensFunctor f).obj (unop U))) ≫
        X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map ((Opens.map (𝟙 (↑X : TopCat))).map i.unop).op :
      Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) (unop U))) ⟶
        X.presheaf.obj (op ((Opens.map (𝟙 (↑X : TopCat))).obj (unop V))))

Tactic:
rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]

Premises used: AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp