awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑(TopCat.of ↥X) : Type u))
⊢ PresheafedSpace.IsOpenImmersion (X.ofRestrict h)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑(TopCat.of ↥X) : Type u))
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ X.ofRestrict h ''ᵁ unop (op W) ≤ V

Tactic:
Set.image_subset_iff.mpr e

Premises used: Iff.mpr, Set.Mem, setOf, Set.Subset, Set.image, Set.image_subset_iff
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑(TopCat.of ↥X) : Type u))
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ X.ofRestrict h ''ᵁ unop (op W) ≤ V

Tactic:
exact Set.image_subset_iff.mpr e

Premises used: Iff.mpr, Set.image_subset_iff
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑(TopCat.of ↥X) : Type u))
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
dsimp :
  X.presheaf.map (⋯.adjunction.counit.app V).op ≫ (X.restrict h).presheaf.map (homOfLE e).op =
    X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))
⊢ Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
dsimp [Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑(TopCat.of ↥X) : Type u))
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ X.presheaf.map (⋯.adjunction.counit.app V).op ≫ (X.restrict h).presheaf.map (homOfLE e).op =
    X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
(X.presheaf.map_comp _ _).symm

Premises used: Set.Mem, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑(TopCat.of ↥X) : Type u))
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ X.presheaf.map (⋯.adjunction.counit.app V).op ≫ (X.restrict h).presheaf.map (homOfLE e).op =
    X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
exact (X.presheaf.map_comp _ _).symm

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U_1 : TopCat
X : Scheme
f : U_1 ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U_1 : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U_1 : Type u)) → (↑(TopCat.of ↥X) : Type u))
U : (X.restrict h).Opens
w : Iso.hom (Hom.appIso (X.ofRestrict h) U) = Iso.hom (Iso.refl Γ(X, X.ofRestrict h ''ᵁ U))
⊢ Hom.appIso (X.ofRestrict h) U = Iso.refl Γ(X, X.ofRestrict h ''ᵁ U)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U_1 : TopCat
X : Scheme
f : U_1 ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U_1 : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U_1 : Type u)) → (↑(TopCat.of ↥X) : Type u))
U : (X.restrict h).Opens
⊢ Iso.hom (Hom.appIso (X.ofRestrict h) U) = Iso.hom (Iso.refl Γ(X, X.ofRestrict h ''ᵁ U))

Tactic:
simp only [restrict_presheaf_obj, Hom.appIso_hom', ofRestrict_appLE, homOfLE_refl, op_id,
    CategoryTheory.Functor.map_id, Iso.refl_hom]

Premises used: AlgebraicGeometry.Scheme.ofRestrict_appLE, CategoryTheory.homOfLE_refl, AlgebraicGeometry.Scheme.restrict_presheaf_obj, AlgebraicGeometry.Scheme.Hom.appIso_hom', CategoryTheory.Functor.map_id, CategoryTheory.Iso.refl_hom, CategoryTheory.op_id
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↥X
h :
  IsOpenEmbedding (X := (↑U : Type u)) (Y := (↑(TopCat.of ↥X) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f) :
      (a : (↑U : Type u)) → (↑(TopCat.of ↥X) : Type u))
V W : (TopologicalSpace.Opens ↥(X.restrict h))ᵒᵖ
i : V ⟶ W
⊢ (X.restrict h).presheaf.map i = X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
rfl

Premises used: IsOpenMap.functorMap, Set.Mem, Quiver.Hom.op, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsIso g
⊢ IsOpenImmersion g

Tactic:
LocallyRingedSpace.IsOpenImmersion.of_isIso _

Premises used: AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : Epi f.base
⊢ IsIso f

Tactic:
@isIso_of_reflects_iso _ _ _ _ _ _ f
    (Scheme.forgetToLocallyRingedSpace ⋙
      LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace)
    (@PresheafedSpace.IsOpenImmersion.to_iso _ _ _ _ f.toPshHom ‹_› _) _

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Functor.comp, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
hf : IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
inst : ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
⊢ IsOpenImmersion f

Tactic:
have (x : X) : IsIso (f.toShHom.hom.stalkMap x) := inferInstanceAs (IsIso (f.stalkMap x))
  SheafedSpace.IsOpenImmersion.of_stalk_iso f.toShHom hf

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom', _private.0.AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap._proof_1, AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
H : IsOpenImmersion f_1
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap f x)

Tactic:
inferInstanceAs <| IsIso (f.toLRSHom.stalkMap x)

Premises used: _private.0.AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap._proof_1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion g
inst_1 : IsOpenImmersion (f ≫ g)
x : ↥X
rw : IsIso (Scheme.Hom.stalkMap (f ≫ g) x)
⊢ IsIso (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)

Tactic:
rw [← Scheme.Hom.stalkMap_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion g
inst_1 : IsOpenImmersion (f ≫ g)
x : ↥X
⊢ IsIso (Scheme.Hom.stalkMap (f ≫ g) x)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f ↔ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
⟨fun H ↦ ⟨H.1, fun x ↦ inferInstanceAs <| IsIso (f.toPshHom.stalkMap x)⟩,
    fun ⟨h, _⟩ ↦ .of_isIso_stalkMap f h⟩

Premises used: _private.0.AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap.match_1, _private.0.AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap._proof_1, And.intro, AlgebraicGeometry.IsOpenImmersion, Iff.intro, AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsOpenImmersion f ∧ Epi f.base

Tactic:
⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => IsOpenImmersion.isIso f⟩

Premises used: CategoryTheory.IsIso, AlgebraicGeometry.IsOpenImmersion.isIso, inferInstance, _private.0.AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base.match_1, And.intro, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
rw :
  ((Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f) ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
⊢ IsIso f ↔ IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
rw [isIso_iff_isOpenImmersion_and_epi_base,
    IsOpenImmersion.iff_isIso_stalkMap, and_comm, ← and_assoc]

Premises used: AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap, and_comm, AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base, and_assoc
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ ((Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f) ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
and_congr ⟨?_, ?_⟩ Iff.rfl

Premises used: Iff.rfl, Iff.intro, and_congr
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
refine_1 : Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f → IsIso f.base
refine_2 : IsIso f.base → Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
⊢ ((Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f) ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
refine and_congr ⟨?_, ?_⟩ Iff.rfl

Premises used: Iff.rfl, Iff.intro, and_congr
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
h₁ : Epi f.base
h₂ : IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
refine_1 : IsIso (TopCat.isoOfHomeo ((Equiv.ofBijective ⇑f ⋯).toHomeomorphOfContinuousOpen ⋯ ⋯)).hom
⊢ IsIso f.base

Tactic:
convert_to
      IsIso
        (TopCat.isoOfHomeo
          (Equiv.toHomeomorphOfContinuousOpen
            (.ofBijective _ ⟨h₂.injective, (TopCat.epi_iff_surjective _).mp h₁⟩) h₂.continuous
            h₂.isOpenMap)).hom

Premises used: CategoryTheory.IsIso, Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Equiv.toHomeomorphOfContinuousOpen, Topology.IsOpenEmbedding.continuous, TopCat.isoOfHomeo, And.intro, Equiv.ofBijective, Topology.IsEmbedding.injective, Iff.mp, TopCat.epi_iff_surjective, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
h₁ : Epi f.base
h₂ : IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsIso (TopCat.isoOfHomeo ((Equiv.ofBijective ⇑f ⋯).toHomeomorphOfContinuousOpen ⋯ ⋯)).hom

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsIso f.base
⊢ Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
⟨inferInstance, (TopCat.homeoOfIso (asIso f.base)).isOpenEmbedding⟩

Premises used: inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.homeoOfIso, And.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, Homeomorph.isOpenEmbedding, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsIso f.base
⊢ Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
exact ⟨inferInstance, (TopCat.homeoOfIso (asIso f.base)).isOpenEmbedding⟩
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Mono f

Tactic:
(forget).mono_of_mono_map (inferInstanceAs (Mono f.toLRSHom))

Premises used: CategoryTheory.Functor.mono_of_mono_map, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, _private.0.AlgebraicGeometry.IsOpenImmersion.mono._proof_1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
⊢ IsOpenImmersion ≤ MorphismProperty.monomorphisms Scheme

Tactic:
fun _ _ _ _ ↦
  MorphismProperty.monomorphisms.infer_property _

Premises used: CategoryTheory.MorphismProperty.monomorphisms.infer_property
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ LocallyRingedSpace.IsOpenImmersion (forget.map 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.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  HasLimit (cospan ((cospan f g ⋙ forget).map WalkingCospan.Hom.inl) ((cospan f g ⋙ forget).map WalkingCospan.Hom.inr))
⊢ HasLimit (cospan f g ⋙ forget)

Tactic:
rw [hasLimit_iff_of_iso (diagramIsoCospan _)]

Premises used: CategoryTheory.Limits.hasLimit_iff_of_iso, CategoryTheory.Limits.diagramIsoCospan
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map WalkingCospan.Hom.inl) ((cospan f g ⋙ forget).map WalkingCospan.Hom.inr))

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

Premises used: _private.0.AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_left._proof_1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map WalkingCospan.Hom.inl) ((cospan f g ⋙ forget).map WalkingCospan.Hom.inr))

Tactic:
exact inferInstanceAs (HasLimit (cospan ((forget).map f) ((forget).map g)))
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))
⊢ HasLimit (cospan g f ⋙ forget)

Tactic:
rw [hasLimit_iff_of_iso (diagramIsoCospan _)]

Premises used: CategoryTheory.Limits.hasLimit_iff_of_iso, CategoryTheory.Limits.diagramIsoCospan
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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:
inferInstanceAs (HasLimit (cospan ((forget).map g) ((forget).map f)))

Premises used: _private.0.AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right._proof_1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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:
exact inferInstanceAs (HasLimit (cospan ((forget).map g) ((forget).map f)))
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ forget.obj
      (PresheafedSpace.IsOpenImmersion.toScheme (X :=
        (pullback (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g)).toPresheafedSpace) Y
        (InducedCategory.Hom.hom
          (LocallyRingedSpace.Hom.toShHom (pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))))) =
    limit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ forget.obj
      (PresheafedSpace.IsOpenImmersion.toScheme (X :=
        (pullback (Scheme.Hom.toLRSHom g) (Scheme.Hom.toLRSHom f)).toPresheafedSpace) Y
        (LocallyRingedSpace.Hom.toHom (pullback.fst (Scheme.Hom.toLRSHom g) (Scheme.Hom.toLRSHom f)))) =
    limit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g) forget

Tactic:
CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit _ _

Premises used: CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan g f) forget

Tactic:
preservesPullback_symmetry _ _ _

Premises used: CategoryTheory.Limits.preservesPullback_symmetry
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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, CategoryTheory.Limits.cospan, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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, CategoryTheory.Limits.cospan, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Eq (α := forget.obj (pullback f g) ⟶ forget.obj Y)
    (CategoryStruct.comp (Y := pullback (forget.map f) (forget.map g)) (Iso.hom (PreservesPullback.iso forget f g))
      (pullback.snd (forget.map f) (forget.map g)))
    (forget.map (pullback.snd f g))

Tactic:
have := PreservesPullback.iso_hom_snd forget f g
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback f g).toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace)
    (CategoryStruct.comp (Y := pullback (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
      (Iso.hom
        (PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y : Scheme.{u}} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g))
      (pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g)))
    (Scheme.Hom.toLRSHom (pullback.snd f g))
rw :
  LocallyRingedSpace.IsOpenImmersion (X := (pullback f g).toLocallyRingedSpace)
    (CategoryStruct.comp (Y := pullback (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
      (Iso.hom
        (PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y : Scheme.{u}} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g))
      (pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g)))
⊢ LocallyRingedSpace.IsOpenImmersion (X := (pullback f g).toLocallyRingedSpace) (Scheme.Hom.toLRSHom (pullback.snd f g))

Tactic:
rw [← this]
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback f g).toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace)
    (CategoryStruct.comp (Y := pullback (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
      (Iso.hom
        (PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y : Scheme.{u}} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g))
      (pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g)))
    (Scheme.Hom.toLRSHom (pullback.snd f g))
⊢ LocallyRingedSpace.IsOpenImmersion (X := (pullback f g).toLocallyRingedSpace)
    (CategoryStruct.comp (Y := pullback (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
      (Iso.hom
        (PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y : Scheme.{u}} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g))
      (pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
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 ≫ (cospan f g).map Hom.inl)
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) one)

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

Premises used: CategoryTheory.Limits.WalkingCospan.Hom.inl, CategoryTheory.Limits.cospan, CategoryTheory.Limits.limit.w