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 (↑(↑X : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
simp :
  X.presheaf.map (i ≫ eqToHom ⋯) =
    X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map f.base).map ((opensFunctor f).map i.unop)).op)
⊢ 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)))

Tactic:
simp only [Functor.op_obj, op_unop, ← X.presheaf.map_comp, Functor.op_map, Category.assoc,
    NatTrans.naturality, Quiver.Hom.unop_op, IsIso.inv_hom_id_assoc,
    TopCat.Presheaf.pushforward_obj_map]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, Opposite.op_unop, TopCat.Presheaf.pushforward_obj_map, CategoryTheory.NatTrans.naturality, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.op_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
U V : (Opens (↑(↑X : TopCat) : Type u_1))ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map (i ≫ eqToHom ⋯) =
    X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map f.base).map ((opensFunctor f).map i.unop)).op)

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
U : Opens (↑(↑X : TopCat) : Type u_1)
delta :
  IsIso (Y := Y.presheaf.obj (op ((opensFunctor f).obj U)))
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U))))
⊢ IsIso (Y := Y.presheaf.obj (op ((opensFunctor f).obj U))) (invApp f U)

Tactic:
delta invApp

Premises used: 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 : Opens (↑(↑X : TopCat) : Type u_1)
⊢ IsIso (Y := Y.presheaf.obj (op ((opensFunctor f).obj U)))
    (X.presheaf.map (eqToHom ⋯) ≫ inv (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
U : Opens (↑(↑X : TopCat) : Type u_1)
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

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

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

Tactic:
rw [← cancel_epi (H.invApp _ U), IsIso.hom_inv_id]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.cancel_epi
-- 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)
delta :
  𝟙 (X.presheaf.obj (op U)) =
    CategoryStruct.comp (Y := Y.presheaf.obj (op ((opensFunctor f).obj U)))
      (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U))))
      (f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯))
⊢ 𝟙 (X.presheaf.obj (op U)) =
    CategoryStruct.comp (Y := Y.presheaf.obj (op ((opensFunctor f).obj U))) (invApp f U)
      (f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯))

Tactic:
delta invApp

Premises used: 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 : Opens (↑(↑X : TopCat) : Type u_1)
⊢ 𝟙 (X.presheaf.obj (op U)) =
    CategoryStruct.comp (Y := Y.presheaf.obj (op ((opensFunctor f).obj U)))
      (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U))))
      (f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_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
U : Opens (↑(↑Y : TopCat) : Type u_1)
⊢ Eq (α :=
    Y.presheaf.obj (op U) ⟶
      X.presheaf.obj ((Opens.map f.base).op.obj (op ((opensFunctor f).obj ((Opens.map f.base).obj U)))))
    (f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯))
    (f.c.app (op U) ≫
      (Functor.obj (TopCat.Presheaf.pushforward C f.base) X.presheaf).map
        (Quiver.Hom.op (X :=
          Set.image (α := (↑(↑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))
            ((⇑(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.carrier))
          (Y := U.carrier)
          (homOfLE (x :=
            Set.image (α := (↑(↑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))
              ((⇑(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.carrier))
            (y := U.carrier) ⋯)))

Tactic:
congr
-- 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 : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑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))
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ Y.presheaf.obj (op ((opensFunctor f).obj ((Opens.map f.base).obj U))))
    (Y.presheaf.map
      (Quiver.Hom.op (X :=
        Set.image (α := (↑(↑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))
          ((⇑(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 (↑(↑Y : TopCat) : Type u_1))))
        (Y := (↑U : Set (↑(↑Y : TopCat) : Type u_1)))
        (homOfLE (x :=
          Set.image (α := (↑(↑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))
            ((⇑(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 (↑(↑Y : TopCat) : Type u_1))))
          (y := (↑U : Set (↑(↑Y : TopCat) : Type u_1))) ⋯)))
    (Y.presheaf.map (eqToHom ⋯))

Tactic:
tauto
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.59719} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsOpenImmersion f

Tactic:
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso (asIso f)

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIso, CategoryTheory.asIso
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
dsimp :
  IsIso (X := Y.presheaf.obj (op (hf.functor.obj U)))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U))) ((Y.ofRestrict hf).c.app (op (hf.functor.obj U)))

Tactic:
dsimp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
h : (↑((Opens.map f).obj (hf.functor.obj U)) : Set (↑X : Type w)) = (↑U : Set (↑X : Type w))
⊢ (Opens.map f).obj (hf.functor.obj U) = U

Tactic:
ext1
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
⊢ (↑((Opens.map f).obj (hf.functor.obj U)) : Set (↑X : Type w)) = (↑U : Set (↑X : Type w))

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.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
⊢ (↑((Opens.map f).obj (hf.functor.obj U)) : Set (↑X : Type w)) = (↑U : Set (↑X : Type w))

Tactic:
exact Set.preimage_image_eq _ hf.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
⊢ (Opens.map f).obj (hf.functor.obj U) = U

Tactic:
have : (Opens.map f).obj (hf.functor.obj U) = U := by
      ext1
      exact Set.preimage_image_eq _ hf.injective
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
h : Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
h₁ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U)) →
    HEq (α :=
      Y.presheaf.obj (op (hf.functor.obj U)) ⟶
        Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))))
      (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
      (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
convert_2 : IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U)))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))

Tactic:
convert_to IsIso (Y.presheaf.map (𝟙 _))

Premises used: CategoryTheory.IsIso, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.presheaf
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))

Tactic:
congr
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4 :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
h : ⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) = unop (op (hf.functor.obj U))
h₁ :
  HEq (α := ⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U)
    (⋯.adjunction.counit.app (hf.functor.obj U)) (β := unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
    (𝟙 (unop (op (hf.functor.obj U))))
⊢ HEq (α :=
    Y.presheaf.obj (op (hf.functor.obj U)) ⟶
      Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))))
    (Y.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (hf.functor.obj U))))
    (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))

Tactic:
congr
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4 :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ ⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) = hf.functor.obj U

Tactic:
congr
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4 :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
h :
  (⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U) =
    (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
⊢ HEq (α := ⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U)
    (⋯.adjunction.counit.app (hf.functor.obj U)) (β := unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
    (𝟙 (unop (op (hf.functor.obj U))))

Tactic:
apply Subsingleton.helim

Premises used: Subsingleton.helim
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4 :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
h h₁ : (⋯.functor.obj U ⟶ hf.functor.obj U) = (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))
⊢ (⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) ⟶ hf.functor.obj U) =
    (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))

Tactic:
rw [this]
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : PresheafedSpace.{v, u, ?u.60852} C
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X : TopCat
Y : PresheafedSpace.{v, u, w} C
f : X ⟶ (↑Y : TopCat)
hf :
  IsOpenEmbedding (X := (↑X : Type w)) (Y := (↑(↑Y : TopCat) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type w)) → (↑(↑Y : TopCat) : Type w))
U : Opens (↑(↑(Y.restrict hf) : TopCat) : Type w)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, w} C
Y : TopCat
f : Y ⟶ TopCat.of (↑(↑X : TopCat) : Type w)
h :
  IsOpenEmbedding (X := (↑Y : Type w)) (Y := (↑(TopCat.of (↑(↑X : TopCat) : Type w)) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑Y : Type w)) → (↑(TopCat.of (↑(↑X : TopCat) : Type w)) : Type w))
U : Opens (↑(↑(X.restrict h) : TopCat) : Type w)
delta :
  Eq (α := (X.restrict h).presheaf.obj (op U) ⟶ X.presheaf.obj (op ((opensFunctor (X.ofRestrict h)).obj U)))
    ((X.restrict h).presheaf.map (eqToHom ⋯) ≫
      inv ((X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))))
    (𝟙 ((X.restrict h).presheaf.obj (op U)))
⊢ Eq (α := (X.restrict h).presheaf.obj (op U) ⟶ X.presheaf.obj (op ((opensFunctor (X.ofRestrict h)).obj U)))
    (invApp (X.ofRestrict h) U) (𝟙 ((X.restrict h).presheaf.obj (op U)))

Tactic:
delta invApp

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, w} C
Y : TopCat
f : Y ⟶ TopCat.of (↑(↑X : TopCat) : Type w)
h :
  IsOpenEmbedding (X := (↑Y : Type w)) (Y := (↑(TopCat.of (↑(↑X : TopCat) : Type w)) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑Y : Type w)) → (↑(TopCat.of (↑(↑X : TopCat) : Type w)) : Type w))
U : Opens (↑(↑(X.restrict h) : TopCat) : Type w)
rw : (X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))
⊢ Eq (α := (X.restrict h).presheaf.obj (op U) ⟶ X.presheaf.obj (op ((opensFunctor (X.ofRestrict h)).obj U)))
    ((X.restrict h).presheaf.map (eqToHom ⋯) ≫
      inv ((X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))))
    (𝟙 ((X.restrict h).presheaf.obj (op U)))

Tactic:
rw [IsIso.comp_inv_eq, Category.id_comp]

Premises used: CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Category.id_comp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, w} C
Y : TopCat
f : Y ⟶ TopCat.of (↑(↑X : TopCat) : Type w)
h :
  IsOpenEmbedding (X := (↑Y : Type w)) (Y := (↑(TopCat.of (↑(↑X : TopCat) : Type w)) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑Y : Type w)) → (↑(TopCat.of (↑(↑X : TopCat) : Type w)) : Type w))
U : Opens (↑(↑(X.restrict h) : TopCat) : Type w)
change :
  X.presheaf.map (h.functor.op.map (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop (op ((opensFunctor (X.ofRestrict h)).obj U)))))
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))

Tactic:
change X.presheaf.map _ = X.presheaf.map _

Premises used: CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.presheaf
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, w} C
Y : TopCat
f : Y ⟶ TopCat.of (↑(↑X : TopCat) : Type w)
h :
  IsOpenEmbedding (X := (↑Y : Type w)) (Y := (↑(TopCat.of (↑(↑X : TopCat) : Type w)) : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑Y : Type w)) → (↑(TopCat.of (↑(↑X : TopCat) : Type w)) : Type w))
U : Opens (↑(↑(X.restrict h) : TopCat) : Type w)
⊢ X.presheaf.map (h.functor.op.map (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (⋯.adjunction.counit.app (unop (op ((opensFunctor (X.ofRestrict h)).obj U)))))

Tactic:
congr 1