awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit
    (cospan (X := Functor.obj forget X) (CategoryTheory.Functor.map forget f) (CategoryTheory.Functor.map forget g))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))

Tactic:
have : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl)
      ((cospan f g ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map f) ((forget).map g))
    infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
⊢ HasLimit (cospan f g ⋙ forget)

Tactic:
apply hasLimit_of_iso (diagramIsoCospan _).symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoCospan
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))

Tactic:
show HasLimit (cospan ((forget).map f) ((forget).map g)) from inferInstance

Premises used: inferInstance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
change :
  HasLimit
    (cospan (X := Functor.obj forget Y) (CategoryTheory.Functor.map forget g) (CategoryTheory.Functor.map forget f))
⊢ HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))

Tactic:
change HasLimit (cospan ((forget).map g) ((forget).map f))

Premises used: CategoryTheory.Limits.HasLimit, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Functor.map, CategoryTheory.Limits.cospan
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit
    (cospan (X := Functor.obj forget Y) (CategoryTheory.Functor.map forget g) (CategoryTheory.Functor.map forget f))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))

Tactic:
have : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl)
      ((cospan g f ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map g) ((forget).map f))
    infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))
⊢ HasLimit (cospan g f ⋙ forget)

Tactic:
apply hasLimit_of_iso (diagramIsoCospan _).symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoCospan
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))

Tactic:
show HasLimit (cospan ((forget).map g) ((forget).map f)) from inferInstance

Premises used: inferInstance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ pullback f.hom g.hom = pullback ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)

Tactic:
congr
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ pullback g.hom f.hom = pullback ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)

Tactic:
congr
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
dsimp : PreservesLimit (cospan f.hom g.hom) (PresheafedSpace.forget C)
⊢ PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    (PresheafedSpace.forget C)

Tactic:
dsimp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f.hom g.hom) (PresheafedSpace.forget C)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    (PresheafedSpace.forget C)

Tactic:
have : PreservesLimit
        (cospan ((cospan f g ⋙ forget).map Hom.inl)
          ((cospan f g ⋙ forget).map Hom.inr)) (PresheafedSpace.forget C) := by
        dsimp
        infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    (PresheafedSpace.forget C)
⊢ PreservesLimit (cospan f g ⋙ forget) (PresheafedSpace.forget C)

Tactic:
apply preservesLimit_of_iso_diagram _ (diagramIsoCospan _).symm

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoCospan
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan g f) («forget» C)

Tactic:
preservesPullback_symmetry _ _ _

Premises used: CategoryTheory.Limits.preservesPullback_symmetry
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasPullback f g

Tactic:
hasLimit_of_created (cospan f g) forget

Premises used: CategoryTheory.hasLimit_of_created, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Limits.cospan
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasPullback g f

Tactic:
hasLimit_of_created (cospan g f) forget

Premises used: CategoryTheory.hasLimit_of_created, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Limits.cospan
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))

Tactic:
have : _ = (pullback.snd f g).hom := preservesLimitIso_hom_π forget (cospan f g) right
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
rw :
  PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace) (InducedCategory.Hom.hom (pullback.snd f g))

Tactic:
rw [← this]
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
⊢ Eq (α :=
    limit (cospan f g ⋙ forget) ⟶
      (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)).obj right)
    (CategoryStruct.comp (Y := limit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))))
      (limit.π (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)) right))
    (limit.π (cospan f g ⋙ forget) right ≫ (diagramIsoCospan (cospan f g ⋙ forget)).hom.app right)

Tactic:
have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan f g ⋙ forget)) right
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
this :
  Eq (α := limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget)))) (limit.π (cospan f.hom g.hom) right))
    (limit.π (cospan f g ⋙ forget) right ≫ 𝟙 Y.toPresheafedSpace)
⊢ Eq (α := limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget)))) (limit.π (cospan f.hom g.hom) right))
    (limit.π (cospan f g ⋙ forget) right)

Tactic:
rw [Category.comp_id] at this

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
this :
  Eq (α := limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget)))) (limit.π (cospan f.hom g.hom) right))
    (limit.π (cospan f g ⋙ forget) right)
rw :
  PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
          (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))))
          (limit.π (cospan f.hom g.hom) right) :
        limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace))
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))

Tactic:
rw [← this]
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback f g).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (limit.π (cospan f g ⋙ forget) right : limit (cospan f g ⋙ forget) ⟶ (cospan f g ⋙ forget).obj right))
    (InducedCategory.Hom.hom (pullback.snd f g))
this :
  Eq (α := limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget)))) (limit.π (cospan f.hom g.hom) right))
    (limit.π (cospan f g ⋙ forget) right)
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback f g).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan f g ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan f g)) :
        Functor.obj forget (limit (cospan f g)) ⟶ limit (cospan f g ⋙ forget))
      (CategoryStruct.comp (Y := limit (cospan f.hom g.hom))
          (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan f g ⋙ forget))))
          (limit.π (cospan f.hom g.hom) right) :
        limit (cospan f g ⋙ forget) ⟶ Y.toPresheafedSpace))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))

Tactic:
have : _ = (pullback.fst g f).hom := preservesLimitIso_hom_π forget (cospan g f) left
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
rw :
  PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace) (InducedCategory.Hom.hom (pullback.fst g f))

Tactic:
rw [← this]
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
⊢ Eq (α :=
    limit (cospan g f ⋙ forget) ⟶
      (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)).obj left)
    (CategoryStruct.comp (Y := limit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))))
      (limit.π (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)) left))
    (limit.π (cospan g f ⋙ forget) left ≫ (diagramIsoCospan (cospan g f ⋙ forget)).hom.app left)

Tactic:
have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan g f ⋙ forget)) left
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
this :
  Eq (α := limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget)))) (limit.π (cospan g.hom f.hom) left))
    (limit.π (cospan g f ⋙ forget) left ≫ 𝟙 Y.toPresheafedSpace)
⊢ Eq (α := limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget)))) (limit.π (cospan g.hom f.hom) left))
    (limit.π (cospan g f ⋙ forget) left)

Tactic:
rw [Category.comp_id] at this

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
this :
  Eq (α := limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget)))) (limit.π (cospan g.hom f.hom) left))
    (limit.π (cospan g f ⋙ forget) left)
rw :
  PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
          (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))))
          (limit.π (cospan g.hom f.hom) left) :
        limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace))
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))

Tactic:
rw [← this]
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
this :
  Eq (α := limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget)))) (limit.π (cospan g.hom f.hom) left))
    (limit.π (cospan g f ⋙ forget) left)
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
          (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))))
          (limit.π (cospan g.hom f.hom) left) :
        limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
rw : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ f)
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) one)

Tactic:
rw [← limit.w (cospan f g) Hom.inl, cospan_map_inl]

Premises used: CategoryTheory.Limits.WalkingCospan.Hom.inl, CategoryTheory.Limits.cospan_map_inl, CategoryTheory.Limits.cospan, CategoryTheory.Limits.limit.w
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ f)

Tactic:
infer_instance