awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
this : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
change :
  IsIso (X := (↑(pullback f g) : TopCat))
    (Hom.base
        (Iso.hom
          (limit.isoLimitCone
            { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) })) ≫
      pullback.snd f.base g.base)
⊢ IsIso (X := (↑(pullback f g) : TopCat))
    (Hom.base
      (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:
change IsIso (_ ≫ pullback.snd _ _)

Premises used: CategoryTheory.IsIso, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
this : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
⊢ IsIso (X := (↑(pullback f g) : TopCat))
    (Hom.base
        (Iso.hom
          (limit.isoLimitCone
            { cone := pullbackConeOfLeft f g, isLimit := pullbackConeOfLeftIsLimit f g : LimitCone (cospan f g) })) ≫
      pullback.snd f.base g.base)

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
this : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
⊢ IsIso (X := (↑(pullback f g) : TopCat)) (Hom.base (pullback.snd f g))

Tactic:
have : IsIso (pullback.snd f g).base := by
    delta pullback.snd
    rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right]
    change IsIso (_ ≫ pullback.snd _ _)
    infer_instance
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
this_1 : IsIso (X := pullback f.base g.base) (pullback.snd f.base g.base)
this : IsIso (X := (↑(pullback f g) : TopCat)) (Hom.base (pullback.snd f g))
⊢ IsIso (X := pullback f g) (pullback.snd f g)

Tactic:
apply to_iso

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
⊢ lift f g H ≫ f = g

Tactic:
simp [AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift,
    CategoryTheory.Limits.pullback.condition]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H :
  Subset (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
l : Y ⟶ X
hl : l ≫ f = g
rw : l ≫ f = lift f g H ≫ f
rw₁ : g = lift f g H ≫ f
rw₂ rw₃ : g = g
⊢ l = lift f g H

Tactic:
rw [← cancel_mono f, hl, lift_fac]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst_1 : IsOpenImmersion g
e :
  Eq (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
rw : (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f
⊢ lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X

Tactic:
rw [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst_1 : IsOpenImmersion g
e :
  Eq (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst_1 : IsOpenImmersion g
e :
  Eq (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
rw : (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g
⊢ lift f g ⋯ ≫ lift g f ⋯ = 𝟙 Y

Tactic:
rw [← cancel_mono g]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst_1 : IsOpenImmersion g
e :
  Eq (α := Set (↑(↑Z : TopCat) : Type u_1))
    (Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
    (Set.range (ι := (↑(↑Y : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) g.base) :
        (a : (↑(↑Y : TopCat) : Type u_1)) → (↑(↑Z : TopCat) : Type u_1)))
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
apply :
  (Functor.obj
      (TopCat.Presheaf.pushforward C (Hom.base (Iso.hom (Iso.symm (isoRestrict f)))) :
        TopCat.Presheaf.{u_1, v, u} C (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) ⥤
          TopCat.Presheaf.{u_1, v, u} C (↑X : TopCat))
      (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf).IsSheaf
⊢ X.presheaf.IsSheaf

Tactic:
apply TopCat.Presheaf.isSheaf_of_iso (sheafIsoOfIso (isoRestrict f).symm).symm

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict, TopCat.Presheaf.isSheaf_of_iso, CategoryTheory.Iso.symm, AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
h : (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.IsSheaf
⊢ (Functor.obj
      (TopCat.Presheaf.pushforward C (Hom.base (Iso.hom (Iso.symm (isoRestrict f)))) :
        TopCat.Presheaf.{u_1, v, u} C (↑(Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯) : TopCat) ⥤
          TopCat.Presheaf.{u_1, v, u} C (↑X : TopCat))
      (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf).IsSheaf

Tactic:
apply TopCat.Sheaf.pushforward_sheaf_of_sheaf

Premises used: TopCat.Sheaf.pushforward_sheaf_of_sheaf
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.IsSheaf

Tactic:
(Y.restrict H.base_open).IsSheaf

Premises used: AlgebraicGeometry.SheafedSpace.restrict, AlgebraicGeometry.SheafedSpace.IsSheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ (Y.restrict (U := (↑X : TopCat)) (f := f.base) ⋯).presheaf.IsSheaf

Tactic:
exact (Y.restrict H.base_open).IsSheaf

Premises used: AlgebraicGeometry.SheafedSpace.restrict, AlgebraicGeometry.SheafedSpace.IsSheaf, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ (toSheafedSpace Y f).toPresheafedSpace = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ Hom.base (InducedCategory.Hom.hom (toSheafedSpaceHom Y f)) = f.base

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ Hom.c (InducedCategory.Hom.hom (toSheafedSpaceHom Y f)) = f.c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace.{v, u, u_1} C
Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ SheafedSpace.IsOpenImmersion (X := toSheafedSpace Y f) (toSheafedSpaceHom Y f)

Tactic:
H
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
inst_1 : SheafedSpace.IsOpenImmersion f
mk :
  ∀ (toPresheafedSpace : PresheafedSpace.{v, u, u_1} C) (IsSheaf : toPresheafedSpace.presheaf.IsSheaf)
    (f : { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf : SheafedSpace.{u, v, u_1} C } ⟶ Y)
    [inst_2 : SheafedSpace.IsOpenImmersion f],
    toSheafedSpace Y f.hom = { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf }
⊢ toSheafedSpace Y f.hom = X

Tactic:
cases X
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
Y : SheafedSpace.{u, v, u_1} C
toPresheafedSpace : PresheafedSpace.{v, u, u_1} C
IsSheaf : toPresheafedSpace.presheaf.IsSheaf
f : { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf : SheafedSpace.{u, v, u_1} C } ⟶ Y
inst_1 : SheafedSpace.IsOpenImmersion f
⊢ toSheafedSpace Y f.hom = { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf }

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X : PresheafedSpace CommRingCat
Y : LocallyRingedSpace
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ (toLocallyRingedSpace Y f).toSheafedSpace = toSheafedSpace Y.toSheafedSpace f

Tactic:
rfl

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace, rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X : PresheafedSpace CommRingCat
Y : LocallyRingedSpace
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ Eq (α := (toLocallyRingedSpace Y f).toSheafedSpace ⟶ Y.toSheafedSpace)
    (LocallyRingedSpace.Hom.toShHom (toLocallyRingedSpaceHom Y f)) (InducedCategory.homMk f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : LocallyRingedSpace
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
⊢ LocallyRingedSpace.IsOpenImmersion (X := toLocallyRingedSpace Y f) (toLocallyRingedSpaceHom Y f)

Tactic:
H
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
inst : LocallyRingedSpace.IsOpenImmersion f
⊢ toLocallyRingedSpace Y f.toHom = X

Tactic:
rfl

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace, rfl, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
h :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) =
    (↑(Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U)) :
      Set (↑(↑Y : TopCat) : Type u_1))
⊢ U = Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U)

Tactic:
ext1
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
⊢ (↑U : Set (↑(↑Y : TopCat) : Type u_1)) =
    (↑(Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U)) :
      Set (↑(↑Y : TopCat) : Type u_1))

Tactic:
(Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm

Premises used: Set.inter_eq_left, Iff.mpr, Set.image_preimage_eq_inter_range, Eq.symm, Eq.trans
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
⊢ (↑U : Set (↑(↑Y : TopCat) : Type u_1)) =
    (↑(Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U)) :
      Set (↑(↑Y : TopCat) : Type u_1))

Tactic:
exact (Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm

Premises used: Set.inter_eq_left, Iff.mpr, Set.image_preimage_eq_inter_range, Eq.symm, Eq.trans
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
⊢ U = Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U)

Tactic:
have : U = H.base_open.functor.obj ((Opens.map f.base).obj U) := by
    ext1
    exact (Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
this : U = Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U)
⊢ IsIso (X := Y.presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U))))
    (f.c.app (op (Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U))))

Tactic:
H.c_iso ((Opens.map f.base).obj U)

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : PresheafedSpace.{v, u, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens (↑(↑Y : TopCat) : Type u_1)
hU :
  (↑U : Set (↑(↑Y : TopCat) : Type u_1)) ⊆
    Set.range (ι := (↑(↑X : TopCat) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) f.base) :
        (a : (↑(↑X : TopCat) : Type u_1)) → (↑(↑Y : TopCat) : Type u_1))
this : U = Functor.obj (IsOpenEmbedding.functor (f := f.base) ⋯) ((Opens.map f.base).obj U)
⊢ IsIso (X := Y.presheaf.obj (op U)) (f.c.app (op U))

Tactic:
convert! H.c_iso ((Opens.map f.base).obj U)

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsOpenImmersion f

Tactic:
@PresheafedSpace.IsOpenImmersion.ofIsIso _ _ _ _ f.hom
    (SheafedSpace.forgetToPresheafedSpace.map_isIso _)

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofIsIso, CategoryTheory.InducedCategory.Hom.hom
-- 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 ⟶ Y
g : Y ⟶ Z
inst_1 : IsOpenImmersion f
inst_2 : IsOpenImmersion g
⊢ IsOpenImmersion (f ≫ g)

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

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp, CategoryTheory.InducedCategory.Hom.hom
-- 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
⊢ Mono f.hom

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
⊢ PresheafedSpace.IsOpenImmersion (X := Functor.obj forget X) (CategoryTheory.Functor.map forget f)

Tactic:
⟨H.base_open, H.c_iso⟩

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mk, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- 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 X) (CategoryTheory.Functor.map forget f) (CategoryTheory.Functor.map forget g))
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))

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

Premises used: CategoryTheory.Limits.HasLimit, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Functor.map, CategoryTheory.Limits.cospan