awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this :
  IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
      (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU))
    (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection ⋯ hVU ⋯ ⋯)
rw :
  IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U) (appLE g U V hVU)) (Y :=
    Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W))
    (Iso.hom (pushout.congrHom ⋯ ⋯) ≫ pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W)
⊢ IsIso (Y := Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W)) (app (normalizationPullback f g) W)

Tactic:
rw [← @isIso_comp_left_iff _ _ _ _ _ _ _ this,
    ← isIso_comp_left_iff (pushout.congrHom f.fromNormalization.app_eq_appLE rfl).hom]

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, CategoryTheory.isIso_comp_left_iff, CategoryTheory.Limits.pushout.congrHom, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CategoryTheory.Iso.hom, rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this :
  IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
      (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU))
    (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection ⋯ hVU ⋯ ⋯)
⊢ (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth

Tactic:
have : (g.appLE U V hVU).hom.Smooth := g.smooth_appLE hU hV hVU
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this_1 :
  IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
      (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU))
    (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection ⋯ hVU ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
⊢ Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)

Tactic:
algebraize [(f.app U).hom, (g.appLE U V hVU).hom, ((pullback.snd f g).app V).hom]

Premises used: CommRingCat.Hom.hom, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Hom.app
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this_1 :
  IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
      (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU))
    (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection ⋯ hVU ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
simp_rw :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.fst f g ≫ f) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
simp_rw₁ :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) ((pullback.snd f g ≫ g) ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
simp_rw₂ :
  Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ g ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)
simp_rw₃ : Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.snd f g ⁻¹ᵁ (g ⁻¹ᵁ U ⊓ V))
⊢ Eq (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U ⊓ pullback.snd f g ⁻¹ᵁ V)

Tactic:
simp_rw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.Scheme.Hom.preimage_inf, CategoryTheory.Limits.pullback.condition, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this_1 :
  IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
      (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU))
    (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection ⋯ hVU ⋯ ⋯)
this : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
⊢ IsIso (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)

Tactic:
have := isIso_pushoutSection_of_isQuasiSeparated_of_flat_right
    (.of_hasPullback f g) hVU le_rfl (UY := pullback.snd f g ⁻¹ᵁ V)
    (by simp_rw [← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]) hU hV (f.isCompact_preimage hU.isCompact)
    (f.isQuasiSeparated_preimage hU.isQuasiSeparated)
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this_1 :
  IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
      (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU))
    (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection ⋯ hVU ⋯ ⋯)
this_2 : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
this : IsIso (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    ((↑(Y.presheaf.1 (Opposite.op V)) : Type u) ⊗[(↑(S.presheaf.1 (Opposite.op U)) : Type u)]
      (↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U))) : Type u)) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  Iso.trans (Y :=
    pushout (X := CommRingCat.of (↑(S.presheaf.1 (Opposite.op U)) : Type u)) (Y :=
      CommRingCat.of (↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U))) : Type u)) (Z :=
      CommRingCat.of (↑(Y.presheaf.1 (Opposite.op V)) : Type u))
      (CommRingCat.ofHom
        (algebraMap (↑(S.presheaf.1 (Opposite.op U)) : Type u) (↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U))) : Type u)))
      (CommRingCat.ofHom
        (algebraMap (↑(S.presheaf.1 (Opposite.op U)) : Type u) (↑(Y.presheaf.1 (Opposite.op V)) : Type u))))
    (IsPushout.isoPushout ⋯) (pushout.congrHom ⋯ ⋯ ≪≫ asIso (pushoutSection ⋯ hVU ⋯ ⋯))
r : (↑Γ(Y, V) : Type u)
⊢ CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ e₀.hom = app (pullback.snd f g) V

Tactic:
simp [e₀, pushout.inr_desc_assoc, Scheme.Hom.app_eq_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CategoryTheory.Limits.pushout.inr_desc_assoc
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsOpenImmersion f
inst_2 : IsOpenImmersion g
⊢ IsOpenImmersion (f ≫ g)

Tactic:
LocallyRingedSpace.IsOpenImmersion.comp f.toLRSHom g.toLRSHom

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.comp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : LocallyRingedSpace
h :
  ∀ (x : (↑X.toTopCat : Type u)),
    ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X),
      Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
          x ∧
        IsOpenImmersion f
x : (↑X.toTopCat : Type u)
obtain :
  ∀ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X)
    (h₁ :
      Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
        x)
    (h₂ : IsOpenImmersion f),
    ∃ (U : OpenNhds x) (R : CommRingCat.{u}), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u}), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))

Tactic:
obtain ⟨R, f, h₁, h₂⟩ := h x
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : LocallyRingedSpace
h :
  ∀ (x : (↑X.toTopCat : Type u)),
    ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X),
      Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
          x ∧
        IsOpenImmersion f
x : (↑X.toTopCat : Type u)
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ :
  Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base) :
        (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
    x
h₂ : IsOpenImmersion f
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u}), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))

Tactic:
⟨⟨⟨_, h₂.base_open.isOpen_range⟩, h₁⟩, R, ⟨?_⟩⟩

Premises used: Nonempty.intro, Subtype.mk, Topology.IsOpenEmbedding.isOpen_range, TopologicalSpace.Opens.mk, Exists.intro, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X : LocallyRingedSpace
h :
  ∀ (x : (↑X.toTopCat : Type u)),
    ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X),
      Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
          (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f.base) :
              (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
          x ∧
        IsOpenImmersion f
x : (↑X.toTopCat : Type u)
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ :
  Membership.mem (γ := Set (↑(↑X.toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.base) :
        (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑X.toPresheafedSpace : TopCat) : Type u)))
    x
h₂ : IsOpenImmersion f
refine :
  X.restrict (U :=
      Functor.obj (C := Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
        (↑(Subtype.mk (p := fun (U : Opens (↑X.toTopCat : Type u)) ↦ x ∈ U)
              {
                carrier :=
                  Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) (Hom.toShHom f).hom.base) :
                      (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
                        (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
                is_open' := ⋯ : Opens (↑X.toTopCat : Type u) }
              h₁) :
          Opens (↑X.toTopCat : Type u)))
      ⋯ ≅
    Spec.toLocallyRingedSpace.obj (op R)
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u}), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))

Tactic:
refine ⟨⟨⟨_, h₂.base_open.isOpen_range⟩, h₁⟩, R, ⟨?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsOpen (X := ↥Y) (Set.range (ι := ↥X) ⇑f)

Tactic:
H.base_open.isOpen_range

Premises used: Topology.IsOpenEmbedding.isOpen_range, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
H.base_open

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
y : ↥Y
⊢ y ∈ opensRange f ↔ ∃ (x : ↥X), f x = y

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ (↑(f ''ᵁ U) : Set ↥Y) = ⇑f '' (↑U : Set ↥X)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
⊢ f ''ᵁ U ≤ f ''ᵁ V

Tactic:
Set.image_mono e

Premises used: Set.Mem, Set.image_mono, setOf, Set.Subset, Set.image
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
⊢ (opensFunctor f).map (homOfLE e) = homOfLE ⋯

Tactic:
rfl

Premises used: IsOpenMap.functorMap, Set.Mem, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (opensFunctor f).IsContinuous (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)

Tactic:
f.isOpenEmbedding.functor_isContinuous

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, Topology.IsOpenEmbedding.functor_isContinuous, Set.Mem, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
h : (↑(f ''ᵁ ⊤) : Set ↥Y) = (↑(opensRange f) : Set ↥Y)
⊢ f ''ᵁ ⊤ = opensRange f

Tactic:
apply Opens.ext

Premises used: TopologicalSpace.Opens.ext
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (↑(f ''ᵁ ⊤) : Set ↥Y) = (↑(opensRange f) : Set ↥Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ opensRange (f ≫ g) = g ''ᵁ opensRange f

Tactic:
TopologicalSpace.Opens.ext (Set.range_comp g f)

Premises used: Set.range_comp, CategoryTheory.ConcreteCategory.hom, TopologicalSpace.Opens.ext, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ opensRange f = ⊤

Tactic:
TopologicalSpace.Opens.ext (Set.range_eq_univ.mpr f.homeomorph.surjective)

Premises used: Iff.mpr, Set.range_eq_univ, TopologicalSpace.Opens.ext, AlgebraicGeometry.Scheme.Hom.homeomorph, Homeomorph.surjective
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
inst_1 : IsOpenImmersion g
rw : g ''ᵁ opensRange f = opensRange g
rw₁ : g ''ᵁ ⊤ = opensRange g
rw₂ rw₃ : opensRange g = opensRange g
⊢ opensRange (f ≫ g) = opensRange g

Tactic:
rw [opensRange_comp, opensRange_of_isIso, image_top_eq_opensRange]

Premises used: AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.Scheme.Hom.opensRange_comp, AlgebraicGeometry.Scheme.Hom.opensRange_of_isIso
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f ''ᵁ U ≤ opensRange f

Tactic:
simpa using f.image_mono le_top

Premises used: AlgebraicGeometry.Scheme.Hom.image_mono, le_top
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
h : (↑(f ⁻¹ᵁ f ''ᵁ U) : Set ↥X) = (↑U : Set ↥X)
⊢ f ⁻¹ᵁ f ''ᵁ U = U

Tactic:
apply Opens.ext

Premises used: TopologicalSpace.Opens.ext
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ (↑(f ⁻¹ᵁ f ''ᵁ U) : Set ↥X) = (↑U : Set ↥X)

Tactic:
simp [Set.preimage_image_eq _ f.isOpenEmbedding.injective]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective, Set.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U U' : X.Opens
⊢ f ''ᵁ U ≤ f ''ᵁ U' ↔ U ≤ U'

Tactic:
⟨fun h ↦ ?_, f.image_mono⟩

Premises used: AlgebraicGeometry.Scheme.Hom.image_mono, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U U' : X.Opens
refine : ∀ (h : f ''ᵁ U ≤ f ''ᵁ U'), U ≤ U'
⊢ f ''ᵁ U ≤ f ''ᵁ U' ↔ U ≤ U'

Tactic:
refine ⟨fun h ↦ ?_, f.image_mono⟩
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
rw : f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'
⊢ U ≤ U'

Tactic:
rw [← preimage_image_eq f U, ← preimage_image_eq f U']

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'

Tactic:
apply f.preimage_mono h

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_mono
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
h : (↑(f ''ᵁ f ⁻¹ᵁ U) : Set ↥Y) = (↑(opensRange f ⊓ U) : Set ↥Y)
⊢ f ''ᵁ f ⁻¹ᵁ U = opensRange f ⊓ U

Tactic:
apply Opens.ext

Premises used: TopologicalSpace.Opens.ext
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
⊢ (↑(f ''ᵁ f ⁻¹ᵁ U) : Set ↥Y) = (↑(opensRange f ⊓ U) : Set ↥Y)

Tactic:
simp [Set.image_preimage_eq_range_inter]

Premises used: Set.image_preimage_eq_range_inter
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
⊢ f ''ᵁ f ⁻¹ᵁ U ≤ U

Tactic:
(f.image_preimage_eq_opensRange_inf U).trans_le inf_le_right

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, inf_le_right, Eq.trans_le