awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
change : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ f)
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ (cospan f g).map Hom.inl)

Tactic:
change IsOpenImmersion (_ ≫ f)

Premises used: AlgebraicGeometry.IsOpenImmersion, CategoryTheory.CategoryStruct.comp
-- 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
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ f)

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
⊢ PreservesLimit (cospan f g) (forget ⋙ LocallyRingedSpace.forgetToTop)

Tactic:
@Limits.comp_preservesLimit _ _ _ _ _ _ (K := cospan f g) _ _ (F := forget)
    (G := LocallyRingedSpace.forgetToTop) ?_ ?_

Premises used: CategoryTheory.Limits.comp_preservesLimit, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, AlgebraicGeometry.LocallyRingedSpace.forgetToTop
-- 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
refine_1 : PreservesLimit (cospan f g) forget
refine_2 : PreservesLimit (cospan f g ⋙ forget) LocallyRingedSpace.forgetToTop
⊢ PreservesLimit (cospan f g) (forget ⋙ LocallyRingedSpace.forgetToTop)

Tactic:
refine @Limits.comp_preservesLimit _ _ _ _ _ _ (K := cospan f g) _ _ (F := forget)
    (G := LocallyRingedSpace.forgetToTop) ?_ ?_

Premises used: CategoryTheory.Limits.comp_preservesLimit, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, AlgebraicGeometry.LocallyRingedSpace.forgetToTop
-- 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:
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
⊢ PreservesLimit (cospan f g ⋙ forget) LocallyRingedSpace.forgetToTop

Tactic:
@preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoCospan.{u} _).symm ?_

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm, 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
refine_2 :
  PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    LocallyRingedSpace.forgetToTop
⊢ PreservesLimit (cospan f g ⋙ forget) LocallyRingedSpace.forgetToTop

Tactic:
refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoCospan.{u} _).symm ?_
-- 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
refine_2 :
  PreservesLimit (cospan (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
    (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat)
⊢ PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    LocallyRingedSpace.forgetToTop

Tactic:
dsimp [LocallyRingedSpace.forgetToTop]

Premises used: AlgebraicGeometry.LocallyRingedSpace.forgetToTop
-- 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 (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
    (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat)

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
⊢ PreservesLimit (cospan g f) Scheme.forgetToTop

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
⊢ PreservesLimit (cospan f g)
    (Scheme.forgetToTop ⋙
      «forget» TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier))

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
⊢ PreservesLimit (cospan g f)
    (Scheme.forgetToTop ⋙
      «forget» TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Set.image (α := (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
            (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) :
        (a : (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u)) → ↥Y)
      (Set.preimage (β := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
          (a : (↑(pullback f.base g.base) : Type u)) → ↥X)
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
rw₁ :
  Function.Surjective (α := ↥(pullback f g)) (β :=
    (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat)) (Y :=
          pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
          (Iso.hom (PreservesPullback.iso Scheme.forgetToTop f g))) :
      (a : ↥(pullback f g)) → (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
⊢ Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g) = (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)

Tactic:
rw [← show _ = (pullback.snd f g).base from
    PreservesPullback.iso_hom_snd Scheme.forgetToTop f g, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.fst f.base g.base)]

Premises used: Iff.mpr, Set.range_eq_univ, Set.range_comp, AlgebraicGeometry.Scheme.forgetToTop, Set.preimage_univ, TopCat.coe_comp, CategoryTheory.Limits.PreservesPullback.iso_hom_snd
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
erw :
  Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map g)) :
        (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
      (Set.image (α := (↑(Scheme.forgetToTop.obj X) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Scheme.forgetToTop.map f)) :
          (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
⊢ Set.image (α := (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
            (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) :
        (a : (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u)) → ↥Y)
      (Set.preimage (β := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
          (a : (↑(pullback f.base g.base) : Type u)) → ↥X)
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)

Tactic:
erw [TopCat.pullback_snd_image_fst_preimage]

Premises used: TopCat.pullback_snd_image_fst_preimage
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map g)) :
        (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
      (Set.range (ι := (↑(Scheme.forgetToTop.obj X) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Scheme.forgetToTop.map f)) :
          (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
⊢ Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map g)) :
        (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
      (Set.image (α := (↑(Scheme.forgetToTop.obj X) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Scheme.forgetToTop.map f)) :
          (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)

Tactic:
rw [Set.image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map g)) :
        (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
      (Set.range (ι := (↑(Scheme.forgetToTop.obj X) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Scheme.forgetToTop.map f)) :
          (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Epi (X := (↑(pullback f g).toPresheafedSpace : TopCat)) (Y :=
    pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
    (Iso.hom (PreservesPullback.iso Scheme.forgetToTop f g))
⊢ Function.Surjective (α := ↥(pullback f g)) (β :=
    (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat)) (Y :=
          pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
          (Iso.hom (PreservesPullback.iso Scheme.forgetToTop f g))) :
      (a : ↥(pullback f g)) → (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))

Tactic:
rw [← TopCat.epi_iff_surjective]

Premises used: TopCat.epi_iff_surjective
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (X := (↑(pullback f g).toPresheafedSpace : TopCat)) (Y :=
    pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
    (Iso.hom (PreservesPullback.iso Scheme.forgetToTop f g))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Scheme.Hom.opensRange (X := pullback f g) (pullback.snd f g) = g ⁻¹ᵁ Scheme.Hom.opensRange f

Tactic:
Opens.ext (range_pullbackSnd f g)

Premises used: AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, TopologicalSpace.Opens.ext
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Set.image (α := (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
            (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) :
        (a : (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u)) → ↥Y)
      (Set.preimage (β := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := pullback g.base f.base) (pullback.snd g.base f.base)) :
          (a : (↑(pullback g.base f.base) : Type u)) → ↥X)
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
rw₁ :
  Function.Surjective (α := ↥(pullback g f)) (β :=
    (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(pullback g f).toPresheafedSpace : TopCat)) (Y :=
          pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
          (Iso.hom (PreservesPullback.iso Scheme.forgetToTop g f))) :
      (a : ↥(pullback g f)) → (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
⊢ Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f) = (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)

Tactic:
rw [← show _ = (pullback.fst g f).base from
    PreservesPullback.iso_hom_fst Scheme.forgetToTop g f, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.snd g.base f.base)]

Premises used: Iff.mpr, Set.range_eq_univ, Set.range_comp, CategoryTheory.Limits.PreservesPullback.iso_hom_fst, AlgebraicGeometry.Scheme.forgetToTop, Set.preimage_univ, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
erw :
  Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map g)) :
        (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
      (Set.image (α := (↑(Scheme.forgetToTop.obj X) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Scheme.forgetToTop.map f)) :
          (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
⊢ Set.image (α := (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
            (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) :
        (a : (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u)) → ↥Y)
      (Set.preimage (β := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := pullback g.base f.base) (pullback.snd g.base f.base)) :
          (a : (↑(pullback g.base f.base) : Type u)) → ↥X)
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)

Tactic:
erw [TopCat.pullback_fst_image_snd_preimage]

Premises used: TopCat.pullback_fst_image_snd_preimage
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Epi (X := (↑(pullback g f).toPresheafedSpace : TopCat)) (Y :=
    pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
    (Iso.hom (PreservesPullback.iso Scheme.forgetToTop g f))
⊢ Function.Surjective (α := ↥(pullback g f)) (β :=
    (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(pullback g f).toPresheafedSpace : TopCat)) (Y :=
          pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
          (Iso.hom (PreservesPullback.iso Scheme.forgetToTop g f))) :
      (a : ↥(pullback g f)) → (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))

Tactic:
rw [← TopCat.epi_iff_surjective]

Premises used: TopCat.epi_iff_surjective
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (X := (↑(pullback g f).toPresheafedSpace : TopCat)) (Y :=
    pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
    (Iso.hom (PreservesPullback.iso Scheme.forgetToTop g f))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Scheme.Hom.opensRange (X := pullback g f) (pullback.fst g f) = g ⁻¹ᵁ Scheme.Hom.opensRange f

Tactic:
Opens.ext (range_pullbackFst f g)

Premises used: TopologicalSpace.Opens.ext, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₂ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₃ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₅ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₆ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₇ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g
rw₈ : (↑(Scheme.Hom.opensRange f) : Set ↥Z) ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g
rw₉ rw₁₀ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)

Tactic:
rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]

Premises used: Set.range_comp, TopologicalSpace.Opens.map_obj, AlgebraicGeometry.IsOpenImmersion.range_pullbackSnd, Set.image_preimage_eq_inter_range, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_coe, AlgebraicGeometry.Scheme.Hom.comp_base, CategoryTheory.Limits.pullback.condition, TopCat.coe_comp, AlgebraicGeometry.Scheme.Hom.coe_opensRange
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback g f))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback g f).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.fst g f))) ≫
              g.base)) :
        (a : ↥(pullback g f)) → ↥Z))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₁ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.fst g f)))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₂ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f)))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₃ :
  Eq (α := Set ↥Z) (⇑g '' (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)) (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₄ :
  Eq (α := Set ↥Z) (⇑g '' (↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ : Opens ↥Y } : Set ↥Y))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₅ :
  Eq (α := Set ↥Z) (Set.image (α := ↥Y) (⇑g) (⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
rw₆ : (Scheme.Hom.opensRange f).carrier ∩ Set.range (ι := ↥Y) ⇑g = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
rw₇ : Set.range (ι := ↥Y) ⇑g ∩ (Scheme.Hom.opensRange f).carrier = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
rw₈ : Set.range (ι := ↥Y) ⇑g ∩ (↑(Scheme.Hom.opensRange f) : Set ↥Z) = Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f
rw₉ rw₁₀ :
  Eq (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f ≫ g))
    (Set.range (ι := ↥Y) ⇑g ∩ Set.range (ι := ↥X) ⇑f)

Tactic:
rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_pullbackFst,
    Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range,
    Set.inter_comm, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]

Premises used: Set.range_comp, TopologicalSpace.Opens.map_obj, Set.image_preimage_eq_inter_range, TopologicalSpace.Opens.coe_mk, Set.inter_comm, TopologicalSpace.Opens.carrier_eq_coe, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, AlgebraicGeometry.Scheme.Hom.coe_opensRange
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
h : ∀ (x : ↥X), x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
⊢ iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
pos :
  ∀ (hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥U) ⇑iU) x),
    x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
neg : ∀ (hx : x ∉ Set.range (ι := ↥U) ⇑iU), x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)
⊢ x ∈ (↑(iU ''ᵁ f' ⁻¹ᵁ W) : Set ↥X) ↔ x ∈ (↑(f ⁻¹ᵁ iV ''ᵁ W) : Set ↥X)

Tactic:
by_cases hx : x ∈ Set.range iU

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, DFunLike.coe