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, 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
⊢ 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))))

Tactic:
congr 1
-- 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
⊢ 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) =
    f

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

Premises used: CategoryTheory.NatTrans.ext, funext, AlgebraicGeometry.PresheafedSpace.Hom.ext, 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
refine :
  ∀ (x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ),
    ((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)).c ≫
            Functor.whiskerRight (eqToHom ⋯) X.presheaf).app
        x =
      f.c.app x
⊢ 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) =
    f

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

Premises used: CategoryTheory.NatTrans.ext, funext, AlgebraicGeometry.PresheafedSpace.Hom.ext, 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
simp :
  ((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)).c ≫
          𝟙
            ((Opens.map
                  (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).op ⋙
              X.presheaf)).app
      x =
    f.c.app x
⊢ ((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)).c ≫
          Functor.whiskerRight (eqToHom ⋯) X.presheaf).app
      x =
    f.c.app x

Tactic:
simp only [eqToHom_refl,
    Functor.whiskerRight_id']

Premises used: CategoryTheory.Functor.whiskerRight_id', CategoryTheory.eqToHom_refl
-- 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
erw :
  f.c.app x ≫
      X.presheaf.map
        (CategoryStruct.comp (Y :=
          (Opens.map f.base).op.obj
            (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          ((Opens.map f.base).op.map
              (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) (unop x))) :
            (Opens.map f.base).op.obj x ⟶
              (Opens.map f.base).op.obj
                (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          (Iso.hom (eqToIso ⋯) :
            (Opens.map f.base).op.obj
                (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))))) ⟶
              op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))) =
    f.c.app x
⊢ ((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)).c ≫
          𝟙
            ((Opens.map
                  (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).op ⋙
              X.presheaf)).app
      x =
    f.c.app x

Tactic:
erw [Category.comp_id, comp_c_app, f.c.naturality_assoc, ← X.presheaf.map_comp]

Premises used: AlgebraicGeometry.PresheafedSpace.comp_c_app, CategoryTheory.Category.comp_id, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.Functor.map_comp, 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
trans :
  f.c.app x ≫
      X.presheaf.map
        (CategoryStruct.comp (Y :=
          (Opens.map f.base).op.obj
            (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          ((Opens.map f.base).op.map
              (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) (unop x))) :
            (Opens.map f.base).op.obj x ⟶
              (Opens.map f.base).op.obj
                (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          (Iso.hom (eqToIso ⋯) :
            (Opens.map f.base).op.obj
                (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))))) ⟶
              op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))) =
    f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x))
trans₁ : f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x)) = f.c.app x
⊢ f.c.app x ≫
      X.presheaf.map
        (CategoryStruct.comp (Y :=
          (Opens.map f.base).op.obj
            (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          ((Opens.map f.base).op.map
              (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) (unop x))) :
            (Opens.map f.base).op.obj x ⟶
              (Opens.map f.base).op.obj
                (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          (Iso.hom (eqToIso ⋯) :
            (Opens.map f.base).op.obj
                (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))))) ⟶
              op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))) =
    f.c.app x

Tactic:
trans f.c.app x ≫ X.presheaf.map (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.NatTrans.app
-- 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ f.c.app x ≫
      X.presheaf.map
        (CategoryStruct.comp (Y :=
          (Opens.map f.base).op.obj
            (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          ((Opens.map f.base).op.map
              (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) (unop x))) :
            (Opens.map f.base).op.obj x ⟶
              (Opens.map f.base).op.obj
                (Functor.obj (Functor.op (IsOpenEmbedding.functor (f := f.base) ⋯)) ((Opens.map f.base).op.obj x)))
          (Iso.hom (eqToIso ⋯) :
            (Opens.map f.base).op.obj
                (op ((opensFunctor f).obj (unop (op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))))) ⟶
              op (Functor.obj (Opens.map (Hom.base (Y.ofRestrict ⋯))) (unop x)))) =
    f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x))

Tactic:
congr 1
-- 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
x : (Opens (↑(↑Y : TopCat) : Type u_1))ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x)) = f.c.app x

Tactic:
simp
-- 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
rw :
  f =
    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)
rw₁ rw₂ : f = f
⊢ Eq (α := Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
    (Iso.inv (isoRestrict f) ≫ f : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)
    (Y.ofRestrict ⋯ : Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯ ⟶ Y)

Tactic:
rw [Iso.inv_comp_eq, isoRestrict_hom_ofRestrict]

Premises used: CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
-- 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
rw :
  Mono
    (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))
⊢ Mono f

Tactic:
rw [← H.isoRestrict_hom_ofRestrict]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
-- 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
⊢ Mono
    (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))

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- 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
V : Opens (↑(↑Y : TopCat) : Type u_1)
U : Opens (↑(↑X : TopCat) : Type u_1)
h : V = (opensFunctor f).obj U
subst : IsIso (X := Y.presheaf.obj (op ((opensFunctor f).obj U))) (f.c.app (op ((opensFunctor f).obj U)))
⊢ IsIso (X := Y.presheaf.obj (op V)) (f.c.app (op V))

Tactic:
subst h
-- 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 (↑(↑X : TopCat) : Type u_1)
⊢ IsIso (X := Y.presheaf.obj (op ((opensFunctor f).obj U))) (f.c.app (op ((opensFunctor f).obj U)))

Tactic:
infer_instance
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
generalize_proofs :
  ∀
    (h :
      IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
          (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))),
    IsIso (X := Z.presheaf.obj (op (h.functor.obj U))) ((f ≫ g).c.app (op (h.functor.obj U)))
⊢ IsIso (X := Z.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := (f ≫ g).base) ⋯) U)))
    ((f ≫ g).c.app (op (Functor.obj (IsOpenEmbedding.functor (f := (f ≫ g).base) ⋯) U)))

Tactic:
generalize_proofs h
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
dsimp :
  IsIso (X := Z.presheaf.obj (op (h.functor.obj U)))
    (g.c.app (op (h.functor.obj U)) ≫ f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
⊢ IsIso (X := Z.presheaf.obj (op (h.functor.obj U))) ((f ≫ g).c.app (op (h.functor.obj U)))

Tactic:
dsimp only [AlgebraicGeometry.PresheafedSpace.comp_c_app, unop_op, Functor.op, comp_base,
      Opens.map_comp_obj]

Premises used: CategoryTheory.Functor.op, AlgebraicGeometry.PresheafedSpace.comp_c_app, AlgebraicGeometry.PresheafedSpace.comp_base, Opposite.unop_op, TopologicalSpace.Opens.map_comp_obj
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
x : IsIso (X := Z.presheaf.obj (op (h.functor.obj U))) (g.c.app (op (h.functor.obj U)))
x₁ :
  IsIso (X := (Functor.obj (TopCat.Presheaf.pushforward C g.base) Y.presheaf).obj (op (h.functor.obj U)))
    (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
⊢ IsIso (X := Z.presheaf.obj (op (h.functor.obj U)))
    (g.c.app (op (h.functor.obj U)) ≫ f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))

Tactic:
apply IsIso.comp_isIso'

Premises used: CategoryTheory.IsIso.comp_isIso'
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
h₁ :
  ∀ (x : (↑(↑Z : TopCat) : Type u_1)),
    x ∈ (↑(h.functor.obj U) : Set (↑(↑Z : TopCat) : Type u_1)) ↔
      x ∈ (↑((opensFunctor g).obj ((opensFunctor f).obj U)) : Set (↑(↑Z : TopCat) : Type u_1))
⊢ h.functor.obj U = (opensFunctor g).obj ((opensFunctor f).obj U)

Tactic:
ext
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
x : (↑(↑Z : TopCat) : Type u_1)
⊢ x ∈ (↑(h.functor.obj U) : Set (↑(↑Z : TopCat) : Type u_1)) ↔
    x ∈ (↑((opensFunctor g).obj ((opensFunctor f).obj U)) : Set (↑(↑Z : TopCat) : Type u_1))

Tactic:
simp
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
⊢ IsIso (X := Z.presheaf.obj (op (h.functor.obj U))) (g.c.app (op (h.functor.obj U)))

Tactic:
exact c_iso' g ((opensFunctor f).obj U) (by ext; simp)

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso', CategoryTheory.Functor.obj
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
x : (Opens.map g.base).obj (h.functor.obj U) = (opensFunctor f).obj U
⊢ IsIso (X := (Functor.obj (TopCat.Presheaf.pushforward C g.base) Y.presheaf).obj (op (h.functor.obj U)))
    (f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))

Tactic:
apply c_iso' f U

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso'
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
x :
  (↑((Opens.map g.base).obj (h.functor.obj U)) : Set (↑(↑Y : TopCat) : Type u_1)) =
    (↑((opensFunctor f).obj U) : Set (↑(↑Y : TopCat) : Type u_1))
⊢ (Opens.map g.base).obj (h.functor.obj U) = (opensFunctor f).obj U

Tactic:
ext1
-- 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
Z : PresheafedSpace.{v, u, u_1} C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens (↑(↑X : TopCat) : Type u_1)
h :
  IsOpenEmbedding (X := (↑(↑X : TopCat) : Type u_1)) (Y := (↑(↑Z : 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 ≫ g).base) :
      (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
x :
  Eq (α := Set (↑(↑Y : TopCat) : Type u_1))
    (Set.preimage (β := (↑(↑Z : 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 : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1))
      (Function.comp (β := (↑(↑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) g.base) :
            (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : 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 : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
        (↑U : Set (↑(↑X : 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 : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1)) ''
      (↑U : Set (↑(↑X : TopCat) : Type u_1)))
⊢ (↑((Opens.map g.base).obj (h.functor.obj U)) : Set (↑(↑Y : TopCat) : Type u_1)) =
    (↑((opensFunctor f).obj U) : Set (↑(↑Y : TopCat) : Type u_1))

Tactic:
dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj, comp_base, TopCat.coe_comp]

Premises used: TopologicalSpace.Opens.map_coe, AlgebraicGeometry.PresheafedSpace.comp_base, TopCat.coe_comp, IsOpenMap.coe_functor_obj
-- 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 (↑(↑X : TopCat) : Type u_1)
⊢ op U = (Opens.map f.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 : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
simp :
  (X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)
⊢ X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
simp only [invApp, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
-- 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 (↑(↑X : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
rw :
  X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))
⊢ (X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
      Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
rw [IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq