awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : PresheafedSpace.{v_1, u_1, u_2} C
H : X ≅ Y
U : Opens (↑(↑Y : TopCat) : Type u_2)
eq₁ :
  Eq (α :=
    X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶
      (obj (Presheaf.pushforward C (H.hom ≫ H.inv).base) X.presheaf).obj (op ((Opens.map H.hom.base).obj U)))
    (H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
        H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) :
      X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶
        (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj
          (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))))
    (eqToHom ⋯ :
      X.presheaf.obj ((Opens.map (Hom.base (𝟙 X))).op.obj (op ((Opens.map H.hom.base).obj U))) ⟶
        X.presheaf.obj ((Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U))))
eq₂ :
  Eq (α :=
    Y.presheaf.obj (op (obj (Opens.map (map (forget C) (H.inv ≫ H.hom))) U)) ⟶
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op (obj (Opens.map (map (forget C) (𝟙 Y))) U)))
    (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ H.hom.c.app (op (obj (Opens.map (map (forget C) (𝟙 Y))) U)))
    (H.hom.c.app (op (obj (Opens.map (map (forget C) (H.inv ≫ H.hom))) U)) ≫
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).map (Quiver.Hom.op (eqToHom ⋯)))
⊢ Eq (α :=
    Y.presheaf.obj (op (obj (Opens.map (map (forget C) (H.inv ≫ H.hom))) U)) ⟶
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op (obj (Opens.map (map (forget C) (𝟙 Y))) U)))
    (eqToHom ⋯ ≫ H.hom.c.app (op (obj (Opens.map (map (forget C) (𝟙 Y))) U)))
    (H.hom.c.app (op (obj (Opens.map (map (forget C) (H.inv ≫ H.hom))) U)) ≫
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).map (eqToHom ⋯))

Tactic:
rw [eqToHom_op, eqToHom_map] at eq₂

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_op
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : PresheafedSpace.{v_1, u_1, u_2} C
H : X ≅ Y
U : Opens (↑(↑Y : TopCat) : Type u_2)
eq₁ :
  Eq (α :=
    X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶
      (obj (Presheaf.pushforward C (H.hom ≫ H.inv).base) X.presheaf).obj (op ((Opens.map H.hom.base).obj U)))
    (H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
        H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) :
      X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶
        (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj
          (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))))
    (eqToHom ⋯ :
      X.presheaf.obj ((Opens.map (Hom.base (𝟙 X))).op.obj (op ((Opens.map H.hom.base).obj U))) ⟶
        X.presheaf.obj ((Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U))))
eq₂ :
  Eq (α :=
    Y.presheaf.obj (op (obj (Opens.map (map (forget C) (H.inv ≫ H.hom))) U)) ⟶
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op (obj (Opens.map (map (forget C) (𝟙 Y))) U)))
    (eqToHom ⋯ ≫ H.hom.c.app (op (obj (Opens.map (map (forget C) (𝟙 Y))) U)))
    (H.hom.c.app (op (obj (Opens.map (map (forget C) (H.inv ≫ H.hom))) U)) ≫
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).map (eqToHom ⋯))
w :
  Eq.{v_1 + 1} (α :=
    X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶ X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
    (CategoryStruct.comp (Y :=
        (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj
          (op ((Opens.map H.inv.base).obj ((Opens.map H.hom.base).obj U))))
        (eqToHom ⋯) ((obj (Presheaf.pushforward C H.hom.base) X.presheaf).map (eqToHom ⋯)) :
      X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶ X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
    (𝟙 ((obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op U)) :
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op U) ⟶
        (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op U))
⊢ H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫ eqToHom ⋯ ≫ H.hom.c.app (op U) =
    𝟙 ((obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op U))

Tactic:
erw [eq₂, reassoc_of% eq₁]
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : PresheafedSpace.{v_1, u_1, u_2} C
H : X ≅ Y
U : Opens (↑(↑Y : TopCat) : Type u_2)
eq₁ :
  Eq (α :=
    X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶
      (obj (Presheaf.pushforward C (H.hom ≫ H.inv).base) X.presheaf).obj (op ((Opens.map H.hom.base).obj U)))
    (H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
        H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) :
      X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶
        (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj
          (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))))
    (eqToHom ⋯ :
      X.presheaf.obj ((Opens.map (Hom.base (𝟙 X))).op.obj (op ((Opens.map H.hom.base).obj U))) ⟶
        X.presheaf.obj ((Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U))))
eq₂ :
  Eq (α :=
    Y.presheaf.obj (op (obj (Opens.map (map (forget C) (H.inv ≫ H.hom))) U)) ⟶
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op (obj (Opens.map (map (forget C) (𝟙 Y))) U)))
    (eqToHom ⋯ ≫ H.hom.c.app (op (obj (Opens.map (map (forget C) (𝟙 Y))) U)))
    (H.hom.c.app (op (obj (Opens.map (map (forget C) (H.inv ≫ H.hom))) U)) ≫
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).map (eqToHom ⋯))
⊢ Eq.{v_1 + 1} (α :=
    X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶ X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
    (CategoryStruct.comp (Y :=
        (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj
          (op ((Opens.map H.inv.base).obj ((Opens.map H.hom.base).obj U))))
        (eqToHom ⋯) ((obj (Presheaf.pushforward C H.hom.base) X.presheaf).map (eqToHom ⋯)) :
      X.presheaf.obj (op ((Opens.map H.hom.base).obj U)) ⟶ X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
    (𝟙 ((obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op U)) :
      (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op U) ⟶
        (obj (Presheaf.pushforward C H.hom.base) X.presheaf).obj (op U))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : PresheafedSpace.{v_1, u_1, u_2} C
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsIso f.base

Tactic:
((forget _).mapIso (asIso f)).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, AlgebraicGeometry.PresheafedSpace.forget, CategoryTheory.Functor.mapIso, CategoryTheory.asIso
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : PresheafedSpace.{v_1, u_1, u_2} C
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsIso f.c

Tactic:
(sheafIsoOfIso (asIso f)).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso, CategoryTheory.asIso
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : PresheafedSpace.{v_1, u_1, u_2} C
f : X ⟶ Y
inst_1 : IsIso f.base
inst_2 : IsIso f.c
⊢ IsIso f

Tactic:
(isoOfComponents (asIso f.base) (asIso f.c).symm).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Iso.symm, AlgebraicGeometry.PresheafedSpace.isoOfComponents, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.asIso
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U_1 : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f_1 : U_1 ⟶ (↑X : TopCat)
h :
  IsOpenEmbedding (X := (↑U_1 : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f_1) :
      (a : (↑U_1 : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
U V : (Opens (↑(↑X : TopCat) : Type u_2))ᵒᵖ
f : U ⟶ V
rw :
  X.presheaf.map (f ≫ Quiver.Hom.op (⋯.adjunction.counit.app (unop V))) =
    X.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop U)) ≫ h.functor.op.map ((Opens.map f_1).op.map f))
⊢ X.presheaf.map f ≫ X.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop V))) =
    X.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop U))) ≫
      X.presheaf.map (h.functor.op.map ((Opens.map f_1).op.map f))

Tactic:
rw [← map_comp, ← map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U_1 : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f_1 : U_1 ⟶ (↑X : TopCat)
h :
  IsOpenEmbedding (X := (↑U_1 : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f_1) :
      (a : (↑U_1 : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
U V : (Opens (↑(↑X : TopCat) : Type u_2))ᵒᵖ
f : U ⟶ V
⊢ X.presheaf.map (f ≫ Quiver.Hom.op (⋯.adjunction.counit.app (unop V))) =
    X.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop U)) ≫ h.functor.op.map ((Opens.map f_1).op.map f))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
⊢ Mono f

Tactic:
haveI : Mono f := (TopCat.mono_iff_injective _).mpr hf.injective
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
right_cancellation :
  ∀ {Z : PresheafedSpace.{v_1, u_1, u_2} C} (g h : Z ⟶ X.restrict hf), g ≫ X.ofRestrict hf = h ≫ X.ofRestrict hf → g = h
⊢ Mono (X.ofRestrict hf)

Tactic:
constructor
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
right_cancellation : g₁.base = g₂.base
right_cancellation₁ : g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf = g₂.c
⊢ g₁ = g₂

Tactic:
ext1
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
⊢ (g₁ ≫ X.ofRestrict hf).base = (g₂ ≫ X.ofRestrict hf).base

Tactic:
have := congr_arg PresheafedSpace.Hom.base eq
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : g₁.base ≫ f = g₂.base ≫ f
⊢ g₁.base = g₂.base

Tactic:
rw [cancel_mono] at this

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : g₁.base = g₂.base
⊢ g₁.base = g₂.base

Tactic:
this
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : g₁.base = g₂.base
⊢ g₁.base = g₂.base

Tactic:
exact this
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
right_cancellation :
  ∀ (V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)),
    Eq (α := (X.restrict hf).presheaf.obj (op V) ⟶ ((Opens.map g₂.base).op ⋙ Z.presheaf).obj (op V))
      ((g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V)) (g₂.c.app (op V))
⊢ g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf = g₂.c

Tactic:
ext V
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
h :
  (↑((Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V)) : Set (↑(↑(X.restrict hf) : TopCat) : Type u_2)) =
    (↑V : Set (↑(↑(X.restrict hf) : TopCat) : Type u_2))
⊢ (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V

Tactic:
ext1
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
⊢ (↑((Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V)) : Set (↑(↑(X.restrict hf) : TopCat) : Type u_2)) =
    (↑V : Set (↑(↑(X.restrict hf) : TopCat) : Type u_2))

Tactic:
Set.preimage_image_eq _ hf.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Set.Mem, setOf, Set.preimage, Topology.IsEmbedding.injective, Set.preimage_image_eq, Set.image
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
⊢ (↑((Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V)) : Set (↑(↑(X.restrict hf) : TopCat) : Type u_2)) =
    (↑V : Set (↑(↑(X.restrict hf) : TopCat) : Type u_2))

Tactic:
exact Set.preimage_image_eq _ hf.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
⊢ (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V

Tactic:
have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V := by
      ext1
      exact Set.preimage_image_eq _ hf.injective
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
⊢ IsIso (X := (Opens.map f ⋙ ⋯.functor).obj (unop (op (hf.functor.obj V))))
    (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))

Tactic:
haveI :
      IsIso (hf.isOpenMap.adjunction.counit.app (unop (op (hf.functor.obj V)))) :=
        NatIso.isIso_app_of_isIso
          (whiskerLeft hf.functor hf.isOpenMap.adjunction.counit) V
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this :
  IsIso (X := (Opens.map f ⋙ ⋯.functor).obj (unop (op (hf.functor.obj V))))
    (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
⊢ Eq (α :=
    X.presheaf.obj (op (hf.functor.obj V)) ⟶
      (obj (Presheaf.pushforward C (g₁ ≫ X.ofRestrict hf).base) Z.presheaf).obj (op (hf.functor.obj V)))
    ((g₁ ≫ X.ofRestrict hf).c.app (op (hf.functor.obj V)))
    ((g₂ ≫ X.ofRestrict hf).c.app (op (hf.functor.obj V)) ≫ Z.presheaf.map (eqToHom ⋯))

Tactic:
have := PresheafedSpace.congr_app eq (op (hf.functor.obj V))
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this_2 :
  IsIso (X := (Opens.map f ⋙ ⋯.functor).obj (unop (op (hf.functor.obj V))))
    (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  Eq (α :=
    X.presheaf.obj (op (hf.functor.obj V)) ⟶
      (obj (Presheaf.pushforward C (g₁ ≫ X.ofRestrict hf).base) Z.presheaf).obj (op (hf.functor.obj V)))
    ((g₁ ≫ X.ofRestrict hf).c.app (op (hf.functor.obj V)))
    ((g₂ ≫ X.ofRestrict hf).c.app (op (hf.functor.obj V)) ≫ Z.presheaf.map (eqToHom ⋯))
⊢ Eq (α :=
    (obj (Presheaf.pushforward C (X.ofRestrict hf).base) (X.restrict hf).presheaf).obj (op (hf.functor.obj V)) ⟶
      (obj (Presheaf.pushforward C g₁.base) Z.presheaf).obj
        (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯))

Tactic:
rw [PresheafedSpace.comp_c_app, PresheafedSpace.comp_c_app,
      PresheafedSpace.ofRestrict_c_app, Category.assoc, cancel_epi] at this

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.PresheafedSpace.comp_c_app, CategoryTheory.cancel_epi, AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app