awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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 j : Discrete ι
h : i ≠ j
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
⊢ Functor.obj (C := Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
      (Opens.map (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
        Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v) ⥤
          Opens (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
      (Functor.obj (C := Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
          (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
            Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
              Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
          (Functor.obj (IsOpenEmbedding.functor ⋯) U) :
        Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v)) =
    ⊥
have h₁ : ∀ (x : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)),
  x ∈
      (↑(Functor.obj (C := Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
            (Opens.map (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
              Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v) ⥤
                Opens (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
            (Functor.obj (C := Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
                (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                  Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                    Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                (Functor.obj (IsOpenEmbedding.functor sorry) U) :
              Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))) :
        Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)) ↔
    x ∈ (↑⊥ : Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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 j : Discrete ι
h : i ≠ j
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
x : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)
⊢ x ∈
      (↑(Functor.obj (C := Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
            (Opens.map (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
              Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v) ⥤
                Opens (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
            (Functor.obj (C := Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
                (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                  Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                    Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                (Functor.obj (IsOpenEmbedding.functor ⋯) U) :
              Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))) :
        Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)) ↔
    x ∈ (↑⊥ : Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
have h₁ : x ∉
  (↑(Functor.obj (C := Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
        (Opens.map (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
          Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v) ⥤
            Opens (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
        (Functor.obj (C := Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
            (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
              Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
            (Functor.obj (IsOpenEmbedding.functor sorry) U) :
          Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))) :
    Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
Tactic: apply iff_false_intro
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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)
⊢ IsIso (X := (colimit F).presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor ⋯) U))) (Y :=
    Functor.obj (C := (Opens (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))ᵒᵖ)
      (Functor.obj (TopCat.Presheaf.pushforward C (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i))))
        (F.obj i).presheaf)
      (op (Functor.obj (IsOpenEmbedding.functor ⋯) U)))
    (NatTrans.app (PresheafedSpace.Hom.c (InducedCategory.Hom.hom (colimit.ι F i)))
      (op (Functor.obj (IsOpenEmbedding.functor ⋯) U)))
have 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))
Tactic: have h₁ := ι_preservesColimitIso_inv SheafedSpace.forgetToPresheafedSpace F i
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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))
⊢ IsIso (X := (colimit F).presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor ⋯) U))) (Y :=
    Functor.obj (C := (Opens (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))ᵒᵖ)
      (Functor.obj (TopCat.Presheaf.pushforward C (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i))))
        (F.obj i).presheaf)
      (op (Functor.obj (IsOpenEmbedding.functor ⋯) U)))
    (NatTrans.app (PresheafedSpace.Hom.c (InducedCategory.Hom.hom (colimit.ι F i)))
      (op (Functor.obj (IsOpenEmbedding.functor ⋯) U)))
have 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)) }
Tactic: have h₂ : colimit.ι F i =
      { hom := (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫
        (preservesColimitIso _ F).inv) } :=
      InducedCategory.hom_ext h₁.symm
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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))
have 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)))
Tactic: have := h₁.symm
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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)) }
⊢ IsIso (X := (colimit F).presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor ⋯) U))) (Y :=
    Functor.obj (C := (Opens (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))ᵒᵖ)
      (Functor.obj (TopCat.Presheaf.pushforward C (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i))))
        (F.obj i).presheaf)
      (op (Functor.obj (IsOpenEmbedding.functor ⋯) U)))
    (NatTrans.app (PresheafedSpace.Hom.c (InducedCategory.Hom.hom (colimit.ι F i)))
      (op (Functor.obj (IsOpenEmbedding.functor ⋯) U)))
have H : 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
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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
⊢ IsOpenImmersion (Y := colimit F) (colimit.ι F i)
have obtain : ∀ (ι' : Type v) (e : ι ≃ ι'), IsOpenImmersion (Y := colimit F) (colimit.ι F i)
Tactic: obtain ⟨ι', ⟨e⟩⟩ := Small.equiv_small (α := ι)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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
⊢ IsOpenImmersion (Y := colimit F) (colimit.ι F i)
have 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)))))
Tactic: have : colimit.ι F i = (colimit.ι F i ≫ (HasColimit.isoOfEquivalence f (Iso.refl _)).inv) ≫
      (HasColimit.isoOfEquivalence f (Iso.refl _)).hom := by
    simp
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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) (colimit.ι F i)
have 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)))))
Tactic: rw [this, HasColimit.ι_isoOfEquivalence_inv]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PullbackCone f g
have refine_1 : Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) sorry ⟶ X
Tactic: refine PullbackCone.mk ?_
      (Y.ofRestrict (TopCat.snd_isOpenEmbedding_of_left H.base_open g.base)) ?_
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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
⊢ PullbackCone f g
have refine_2 : Eq (α := Y.restrict (U := pullback (Hom.toShHom f).hom.base g.base) sorry ⟶ Z)
  ({ toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := sorry } ≫ f)
  (Y.ofRestrict sorry ≫ g)
Tactic: refine PullbackCone.mk ?_
      (Y.ofRestrict (TopCat.snd_isOpenEmbedding_of_left H.base_open g.base)) ?_
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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
⊢ m =
    {
      toHom :=
        PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
      prop := ⋯ }
have refine_2 : m ≫ (pullbackConeOfLeft f g).snd =
  {
      toHom :=
        PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
          (PullbackCone.mk s.fst.toHom s.snd.toHom sorry),
      prop := sorry } ≫
    (pullbackConeOfLeft f g).snd
Tactic: rw [← cancel_mono (pullbackConeOfLeft f g).snd]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (X := pullback f g) (limit.π (cospan f g) WalkingCospan.right)
have rw : IsOpenImmersion (X := pullback f g)
  (Iso.hom (limit.isoLimitCone { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g }) ≫
    { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) }.cone.π.app
      WalkingCospan.right)
Tactic: rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (X := pullback g f) (pullback.fst g f)
have rw : IsOpenImmersion (X := pullback g f) (Iso.hom (pullbackSymmetry g f) ≫ pullback.snd f g)
Tactic: rw [← pullbackSymmetry_hom_comp_snd]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)
have rw : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.left ≫ f)
Tactic: rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit (forgetToSheafedSpace.mapCone (pullbackConeOfLeft f g))
have apply : IsLimit
  (PullbackCone.mk
    (forgetToSheafedSpace.map
      { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := sorry :
        (Y.restrict sorry).Hom X })
    (forgetToSheafedSpace.map (Y.ofRestrict sorry)) sorry)
Tactic: apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit
    (PullbackCone.mk
      (forgetToSheafedSpace.map
        { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ :
          (Y.restrict ⋯).Hom X })
      (forgetToSheafedSpace.map (Y.ofRestrict ⋯)) ⋯)
have l : IsLimit (F :=
  cospan (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj X))
    (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map f))
    (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map g)))
  (PullbackCone.mk (W := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (Y.restrict sorry)))
    (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace
        (forgetToSheafedSpace.map
          { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := sorry }) :
      Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (Y.restrict sorry)) ⟶
        Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj X))
    (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map (Y.ofRestrict sorry)) :
      Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (Y.restrict sorry)) ⟶
        Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj Y))
    sorry)
Tactic: apply isLimitOfIsLimitPullbackConeMap SheafedSpace.forgetToPresheafedSpace
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).mapCone (pullbackConeOfLeft f g))
have apply : IsLimit
  (PullbackCone.mk
    ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map
      { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := sorry :
        (Y.restrict sorry).Hom X })
    ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map (Y.ofRestrict sorry)) sorry)
Tactic: apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g)
    ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) ⋙ PresheafedSpace.forget CommRingCat)
have inst : PreservesLimit (cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
  (PresheafedSpace.forget CommRingCat)
Tactic: apply +allowSynthFailures Limits.comp_preservesLimit