awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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

Tactic:
h₂.trans <| LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 <|
          PullbackCone.mk s.fst.1 s.snd.1 <| congr_arg
            LocallyRingedSpace.Hom.toHom s.condition).symm

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.PullbackCone.fst, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, congr_arg, CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.PullbackCone.snd, Eq.symm, Eq.trans, 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
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 ≫ (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

Tactic:
exact h₂.trans <| LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 <|
          PullbackCone.mk s.fst.1 s.snd.1 <| congr_arg
            LocallyRingedSpace.Hom.toHom s.condition).symm

Premises used: Eq.trans, 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
⊢ HasPullback f g

Tactic:
⟨⟨⟨_, pullbackConeOfLeftIsLimit f g⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit
-- 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
⊢ HasPullback g f

Tactic:
hasPullback_symmetry f g

Premises used: CategoryTheory.Limits.hasPullback_symmetry
-- 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
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)
⊢ IsOpenImmersion (X := pullback f g) (limit.π (cospan f g) WalkingCospan.right)

Tactic:
rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]

Premises used: CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.limit.isoLimitCone_hom_π, CategoryTheory.Limits.LimitCone.mk, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit
-- 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
⊢ 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:
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
rw : IsOpenImmersion (X := pullback g f) (Iso.hom (pullbackSymmetry g f) ≫ pullback.snd f g)
⊢ IsOpenImmersion (X := pullback g f) (pullback.fst g f)

Tactic:
rw [← pullbackSymmetry_hom_comp_snd]

Premises used: CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd
-- 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
⊢ IsOpenImmersion (X := pullback g f) (Iso.hom (pullbackSymmetry g f) ≫ pullback.snd f 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 : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
rw : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.left ≫ f)
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)

Tactic:
rw [← limit.w (cospan f g) WalkingCospan.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 : 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.left ≫ 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
apply :
  IsLimit
    (PullbackCone.mk
      (forgetToSheafedSpace.map
        { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ :
          (Y.restrict ⋯).Hom X })
      (forgetToSheafedSpace.map (Y.ofRestrict ⋯)) ⋯)
⊢ IsLimit (forgetToSheafedSpace.mapCone (pullbackConeOfLeft f g))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.toFun, Equiv.symm
-- 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
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 ⋯)))
      (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace
          (forgetToSheafedSpace.map
            { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ }) :
        Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (Y.restrict ⋯)) ⟶
          Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj X))
      (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map (Y.ofRestrict ⋯)) :
        Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (Y.restrict ⋯)) ⟶
          Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj Y))
      ⋯)
⊢ IsLimit
    (PullbackCone.mk
      (forgetToSheafedSpace.map
        { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ :
          (Y.restrict ⋯).Hom X })
      (forgetToSheafedSpace.map (Y.ofRestrict ⋯)) ⋯)

Tactic:
apply isLimitOfIsLimitPullbackConeMap SheafedSpace.forgetToPresheafedSpace

Premises used: CategoryTheory.Limits.isLimitOfIsLimitPullbackConeMap, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
-- 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
⊢ 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 ⋯)))
      (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace
          (forgetToSheafedSpace.map
            { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ }) :
        Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (Y.restrict ⋯)) ⟶
          Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj X))
      (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map (Y.ofRestrict ⋯)) :
        Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (Y.restrict ⋯)) ⟶
          Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj Y))
      ⋯)

Tactic:
exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit
-- 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
apply :
  IsLimit
    (PullbackCone.mk
      ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map
        { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ :
          (Y.restrict ⋯).Hom X })
      ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map (Y.ofRestrict ⋯)) ⋯)
⊢ IsLimit ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).mapCone (pullbackConeOfLeft f g))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm.toFun

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.toFun, Equiv.symm
-- 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
⊢ IsLimit
    (PullbackCone.mk
      ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map
        { toHom := PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom, prop := ⋯ :
          (Y.restrict ⋯).Hom X })
      ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map (Y.ofRestrict ⋯)) ⋯)

Tactic:
exact PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit f.1 g.1

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftIsLimit
-- 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 ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)

Tactic:
H
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst_1 : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst :
  PreservesLimit (cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
    (PresheafedSpace.forget CommRingCat)
⊢ PreservesLimit (cospan f g)
    ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) ⋙ PresheafedSpace.forget CommRingCat)

Tactic:
apply +allowSynthFailures Limits.comp_preservesLimit

Premises used: CategoryTheory.Limits.comp_preservesLimit
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst_1 : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst :
  cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr) ≅
    cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
inst₁ :
  PreservesLimit
    (cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr))
    (PresheafedSpace.forget CommRingCat)
inst₂ : WalkingCospan ⥤ PresheafedSpace CommRingCat
⊢ PreservesLimit (cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
    (PresheafedSpace.forget CommRingCat)

Tactic:
apply +allowSynthFailures preservesLimit_of_iso_diagram

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram
-- 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
⊢ cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr) ≅
    cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace

Tactic:
exact (diagramIsoCospan _).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoCospan
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst_1 : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst : PreservesLimit (C := PresheafedSpace CommRingCat) (cospan f.toHom g.toHom) (PresheafedSpace.forget CommRingCat)
⊢ PreservesLimit
    (cospan ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inl)
      ((cospan f g ⋙ forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map WalkingCospan.Hom.inr))
    (PresheafedSpace.forget CommRingCat)

Tactic:
dsimp
-- 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
⊢ PreservesLimit (C := PresheafedSpace CommRingCat) (cospan f.toHom g.toHom) (PresheafedSpace.forget CommRingCat)

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
⊢ ReflectsLimit (cospan f g) forgetToSheafedSpace

Tactic:
reflectsLimit_of_reflectsIsomorphisms _ _

Premises used: CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms
-- 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
⊢ PreservesLimit (cospan g f) forgetToSheafedSpace

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 : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan g f) (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)

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 : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ReflectsLimit (cospan g f) forgetToSheafedSpace

Tactic:
reflectsLimit_of_reflectsIsomorphisms _ _

Premises used: CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms
-- 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
⊢ ReflectsLimit (cospan f g) (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)

Tactic:
reflectsLimit_of_reflectsIsomorphisms _ _

Premises used: CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms
-- 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
⊢ ReflectsLimit (cospan g f) (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)

Tactic:
reflectsLimit_of_reflectsIsomorphisms _ _

Premises used: CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
inst : IsIso (X := forgetToSheafedSpace.obj (pullback f g)) (forgetToSheafedSpace.map (pullback.snd f g))
⊢ IsIso (X := pullback f g) (pullback.snd f g)

Tactic:
apply +allowSynthFailures Functor.ReflectsIsomorphisms.reflects
    (F := LocallyRingedSpace.forgetToSheafedSpace)

Premises used: CategoryTheory.Functor.ReflectsIsomorphisms.reflects, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
inst :
  IsIso (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (pullback f g)))
    (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map (pullback.snd f g)))
⊢ IsIso (X := forgetToSheafedSpace.obj (pullback f g)) (forgetToSheafedSpace.map (pullback.snd f g))

Tactic:
apply +allowSynthFailures Functor.ReflectsIsomorphisms.reflects
    (F := SheafedSpace.forgetToPresheafedSpace)

Premises used: CategoryTheory.Functor.ReflectsIsomorphisms.reflects, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
inst :
  IsIso (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (pullback f g)))
    (CategoryStruct.comp (Y :=
      pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))
      (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g))
      (pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g)))
⊢ IsIso (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (pullback f g)))
    (CategoryTheory.Functor.map SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.map (pullback.snd f g)))

Tactic:
erw [← PreservesPullback.iso_hom_snd
      (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g]

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Limits.PreservesPullback.iso_hom_snd
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' :
  Subset (α := Set (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y.toPresheafedSpace : 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) g.base) :
        (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X.toPresheafedSpace : 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.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)))
⊢ IsIso (X := Functor.obj SheafedSpace.forgetToPresheafedSpace (forgetToSheafedSpace.obj (pullback f g)))
    (CategoryStruct.comp (Y :=
      pullback ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))
      (Iso.hom (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g))
      (pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g)))

Tactic:
IsIso.comp_isIso' inferInstance <|
    PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset _ _ H'

Premises used: inferInstance, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset, CategoryTheory.IsIso.comp_isIso'