awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
inst_3 : HasStrictTerminalObjects.{v, u} C
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
h₁ :
  Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i))
h₂ :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    {
      hom :=
        CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
          (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
            (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
          (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
            colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)) }
⊢ Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i) :
      Functor.obj forgetToPresheafedSpace (F.obj i) ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))

Tactic:
have := h₁.symm
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
inst_3 : HasStrictTerminalObjects.{v, u} C
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
h₁ :
  Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i))
h₂ :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    {
      hom :=
        CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
          (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
            (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
          (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
            colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)) }
this :
  Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i) :
      Functor.obj forgetToPresheafedSpace (F.obj i) ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
⊢ IsOpenEmbedding (X := (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) (Y :=
    (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑(colimit F).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i)))) :
      (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) → (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))

Tactic:
sigma_ι_isOpenEmbedding F i

Premises used: AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
inst_3 : HasStrictTerminalObjects.{v, u} C
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
h₁ :
  Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i))
h₂ :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    {
      hom :=
        CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
          (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
            (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
          (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
            colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)) }
this :
  Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i) :
      Functor.obj forgetToPresheafedSpace (F.obj i) ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
⊢ IsOpenEmbedding (X := (↑(↑((F ⋙ forgetToPresheafedSpace).obj i) : TopCat) : Type v)) (Y :=
    (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
          (PresheafedSpace.Hom.base
            (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
              (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
                (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
              (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
                colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F))))) :
      (a : (↑(↑((F ⋙ forgetToPresheafedSpace).obj i) : TopCat) : Type v)) →
        (↑(↑(forgetToPresheafedSpace.obj (colimit F)) : TopCat) : Type v))

Tactic:
convert! sigma_ι_isOpenEmbedding F i

Premises used: AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
inst_3 : HasStrictTerminalObjects.{v, u} C
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
h₁ :
  Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i))
h₂ :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    {
      hom :=
        CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
          (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
            (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
          (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
            colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)) }
⊢ IsOpenEmbedding (X := (↑(↑((F ⋙ forgetToPresheafedSpace).obj i) : TopCat) : Type v)) (Y :=
    (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
          (PresheafedSpace.Hom.base
            (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
              (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
                (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
              (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
                colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F))))) :
      (a : (↑(↑((F ⋙ forgetToPresheafedSpace).obj i) : TopCat) : Type v)) →
        (↑(↑(forgetToPresheafedSpace.obj (colimit F)) : TopCat) : Type v))

Tactic:
have H :
      IsOpenEmbedding
        (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
            (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv).base := by
      have := h₁.symm
      convert! sigma_ι_isOpenEmbedding F i
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι_1 : Type v
F_1 : Discrete ι_1 ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F_1
i_1 : Discrete ι_1
ι : Type w
inst_3 : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_4 : HasColimit F
i : Discrete ι
inst_5 : HasStrictTerminalObjects.{v, u} C
obtain : ∀ (ι' : Type v) (e : ι ≃ ι'), IsOpenImmersion (Y := colimit F) (colimit.ι F i)
⊢ IsOpenImmersion (Y := colimit F) (colimit.ι F i)

Tactic:
obtain ⟨ι', ⟨e⟩⟩ := Small.equiv_small (α := ι)

Premises used: Small.equiv_small
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι_1 : Type v
F_1 : Discrete ι_1 ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F_1
i_1 : Discrete ι_1
ι : Type w
inst_3 : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_4 : HasColimit F
i : Discrete ι
inst_5 : HasStrictTerminalObjects.{v, u} C
ι' : Type v
e : ι ≃ ι'
f : CategoryTheory.Equivalence.{v, w, v, w} (Discrete ι') (Discrete ι) := Discrete.equivalence e.symm
⊢ Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    (CategoryStruct.comp (Y := colimit (f.functor ⋙ F))
      (CategoryStruct.comp (Y := colimit F) (colimit.ι F i)
        (Iso.inv (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))
      (Iso.hom (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι_1 : Type v
F_1 : Discrete ι_1 ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F_1
i_1 : Discrete ι_1
ι : Type w
inst_3 : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_4 : HasColimit F
i : Discrete ι
inst_5 : HasStrictTerminalObjects.{v, u} C
ι' : Type v
e : ι ≃ ι'
f : CategoryTheory.Equivalence.{v, w, v, w} (Discrete ι') (Discrete ι) := Discrete.equivalence e.symm
⊢ Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    (CategoryStruct.comp (Y := colimit (f.functor ⋙ F))
      (CategoryStruct.comp (Y := colimit F) (colimit.ι F i)
        (Iso.inv (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))
      (Iso.hom (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))

Tactic:
have : colimit.ι F i = (colimit.ι F i ≫ (HasColimit.isoOfEquivalence f (Iso.refl _)).inv) ≫
      (HasColimit.isoOfEquivalence f (Iso.refl _)).hom := by
    simp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι_1 : Type v
F_1 : Discrete ι_1 ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F_1
i_1 : Discrete ι_1
ι : Type w
inst_3 : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_4 : HasColimit F
i : Discrete ι
inst_5 : HasStrictTerminalObjects.{v, u} C
ι' : Type v
e : ι ≃ ι'
f : CategoryTheory.Equivalence.{v, w, v, w} (Discrete ι') (Discrete ι) := Discrete.equivalence e.symm
this :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    (CategoryStruct.comp (Y := colimit (f.functor ⋙ F))
      (CategoryStruct.comp (Y := colimit F) (colimit.ι F i)
        (Iso.inv (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))
      (Iso.hom (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))
rw :
  IsOpenImmersion (Y := colimit F)
    (CategoryStruct.comp (Y := colimit (f.functor ⋙ F))
      (F.map (f.counitInv.app i) ≫
        NatTrans.app (Iso.hom (Iso.refl (f.functor ⋙ F))) (f.inverse.obj i) ≫
          colimit.ι (f.functor ⋙ F) (f.inverse.obj i))
      (Iso.hom (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))
⊢ IsOpenImmersion (Y := colimit F) (colimit.ι F i)

Tactic:
rw [this, HasColimit.ι_isoOfEquivalence_inv]

Premises used: CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_inv
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι_1 : Type v
F_1 : Discrete ι_1 ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F_1
i_1 : Discrete ι_1
ι : Type w
inst_3 : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_4 : HasColimit F
i : Discrete ι
inst_5 : HasStrictTerminalObjects.{v, u} C
ι' : Type v
e : ι ≃ ι'
f : CategoryTheory.Equivalence.{v, w, v, w} (Discrete ι') (Discrete ι) := Discrete.equivalence e.symm
this :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    (CategoryStruct.comp (Y := colimit (f.functor ⋙ F))
      (CategoryStruct.comp (Y := colimit F) (colimit.ι F i)
        (Iso.inv (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))
      (Iso.hom (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))
⊢ IsOpenImmersion (Y := colimit F)
    (CategoryStruct.comp (Y := colimit (f.functor ⋙ F))
      (F.map (f.counitInv.app i) ≫
        NatTrans.app (Iso.hom (Iso.refl (f.functor ⋙ F))) (f.inverse.obj i) ≫
          colimit.ι (f.functor ⋙ F) (f.inverse.obj i))
      (Iso.hom (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F)))))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : LocallyRingedSpace
U : TopCat
f : U ⟶ X.toTopCat
hf :
  IsOpenEmbedding (X := (↑U : Type w)) (Y := (↑X.toTopCat : Type w))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type w)) → (↑X.toTopCat : Type w))
⊢ IsOpenImmersion (X.ofRestrict hf)

Tactic:
PresheafedSpace.IsOpenImmersion.ofRestrict X.toPresheafedSpace hf

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.ofRestrict, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.PresheafedSpace.restrict
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsIso g
⊢ IsOpenImmersion g

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g_1 : Y ⟶ Z
H : IsOpenImmersion f
g : Z ⟶ Y
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion (f ≫ g)

Tactic:
PresheafedSpace.IsOpenImmersion.comp f.1 g.1

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Mono (Hom.toShHom f)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ SheafedSpace.IsOpenImmersion (forgetToSheafedSpace.map f)

Tactic:
H
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
refine_1 : Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯ ⟶ X
refine_2 :
  Eq (α := Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯ ⟶ Z)
    ({ toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ } ≫ f)
    (Y.ofRestrict ⋯ ≫ g)
⊢ PullbackCone f g

Tactic:
refine PullbackCone.mk ?_
      (Y.ofRestrict (TopCat.snd_isOpenEmbedding_of_left H.base_open g.base)) ?_

Premises used: TopCat.snd_isOpenEmbedding_of_left, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, CategoryTheory.Limits.PullbackCone.mk, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open, AlgebraicGeometry.LocallyRingedSpace.ofRestrict
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Eq (α := Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯ ⟶ Z)
    ({ toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ } ≫ f)
    (Y.ofRestrict ⋯ ≫ g)

Tactic:
LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition _ _)

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition, AlgebraicGeometry.LocallyRingedSpace.Hom.ext'
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Eq (α := Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) ⋯ ⟶ Z)
    ({ toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ } ≫ f)
    (Y.ofRestrict ⋯ ≫ g)

Tactic:
exact LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullback_cone_of_left_condition _ _)

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.ext'
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion (Y.ofRestrict ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
x : (↑(↑s.pt.toPresheafedSpace : TopCat) : Type u_1)
⊢ Eq (α :=
    Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X :=
              (↑(Cone.pt (F := cospan f.toHom g.toHom) (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) : TopCat))
              (PresheafedSpace.Hom.base
                (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                    (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯) ≫
                  (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd)) :
            (a : (↑(↑(PullbackCone.mk s.fst.toHom s.snd.toHom ⋯).pt : TopCat) : Type u_1)) →
              (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
          x) ⟶
      TopCat.Presheaf.stalk
        (PresheafedSpace.presheaf (Cone.pt (F := cospan f.toHom g.toHom) (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)))
        x)
    (PresheafedSpace.Hom.stalkMap
      (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯) ≫
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f.toHom g.toHom).snd)
      x)
    (CategoryStruct.comp (Y :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X :=
              (↑(Cone.pt (F := cospan f.toHom g.toHom) (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) : TopCat)) (Y :=
              (↑Y.toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (PullbackCone.snd (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))) :
            (a : (↑(↑(PullbackCone.mk s.fst.toHom s.snd.toHom ⋯).pt : TopCat) : Type u_1)) →
              (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
          x))
      (eqToHom ⋯) (PresheafedSpace.Hom.stalkMap (PullbackCone.snd (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯)) x))

Tactic:
have :=
        PresheafedSpace.stalkMap.congr_hom _ _
          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1
            (PullbackCone.mk s.fst.1 s.snd.1
              (congr_arg LocallyRingedSpace.Hom.toHom s.condition)))
          x
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
refine_2 :
  m ≫ (pullbackConeOfLeft f g).fst = s.fst →
    m ≫ (pullbackConeOfLeft f g).snd = s.snd →
      m =
        {
          toHom :=
            PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
              (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
          prop := ⋯ }
⊢ m ≫ (pullbackConeOfLeft f g).fst = s.fst →
    m ≫ (pullbackConeOfLeft f g).snd = s.snd →
      m =
        {
          toHom :=
            PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
              (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
          prop := ⋯ }

Tactic:
_
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
h : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
refine_2 :
  m ≫ (pullbackConeOfLeft f g).snd =
    {
        toHom :=
          PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
            (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
        prop := ⋯ } ≫
      (pullbackConeOfLeft f g).snd
⊢ m =
    {
      toHom :=
        PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
      prop := ⋯ }

Tactic:
rw [← cancel_mono (pullbackConeOfLeft f g).snd]

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeft, CategoryTheory.cancel_mono, CategoryTheory.Limits.PullbackCone.snd