awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
refine : ∀ (H : ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)), IsLocallyArtinian X
⊢ IsLocallyArtinian X ↔ ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)

Tactic:
refine ⟨fun _ _ ↦ IsLocallyArtinian.isArtinianRing_presheaf_obj ⟨_, hU' _⟩, fun H ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
H : ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)
rw : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsLocallyArtinian.{u} ((X.openCoverOfIsOpenCover U hU).X i)
⊢ IsLocallyArtinian X

Tactic:
rw [isLocallyArtinian_iff_openCover (X.openCoverOfIsOpenCover U hU)]

Premises used: AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, AlgebraicGeometry.isLocallyArtinian_iff_openCover
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
H : ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)
⊢ ∀ (i : ι), IsLocallyArtinian.{u} (Spec Γ(X, U i))

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
H : ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)
⊢ ∀ (i : ι), IsLocallyArtinian.{u} (Spec Γ(X, U i))

Tactic:
have : ∀ i, IsLocallyArtinian (Spec Γ(X, U i)) := by simpa
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
H : ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)
this : ∀ (i : ι), IsLocallyArtinian.{u} (Spec Γ(X, U i))
⊢ ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsLocallyArtinian.{u} ((X.openCoverOfIsOpenCover U hU).X i)

Tactic:
fun i ↦ .of_isImmersion (hU' _).isoSpec.hom

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.IsLocallyArtinian.of_isImmersion, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
H : ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)
this : ∀ (i : ι), IsLocallyArtinian.{u} (Spec Γ(X, U i))
⊢ ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsLocallyArtinian.{u} ((X.openCoverOfIsOpenCover U hU).X i)

Tactic:
exact fun i ↦ .of_isImmersion (hU' _).isoSpec.hom
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X),
        IsLocallyArtinian X)
    (hX : ¬Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
wlog :
  ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
⊢ IsLocallyArtinian X

Tactic:
wlog hX : Subsingleton X generalizing X

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, Subsingleton, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
this :
  ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
hX : ¬Subsingleton.{u_1 + 1} ↥X
h :
  ∀ (x : ↥X),
    x ∈ (↑(⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ : TopologicalSpace.Opens ↥X }) : Set ↥X) ↔ x ∈ (↑⊤ : Set ↥X)
⊢ Eq.{u_1 + 1} (α := TopologicalSpace.Opens ↥X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ }) ⊤

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
this :
  ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
hX : ¬Subsingleton.{u_1 + 1} ↥X
x : ↥X
⊢ x ∈ (↑(⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ : TopologicalSpace.Opens ↥X }) : Set ↥X) ↔ x ∈ (↑⊤ : Set ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
this :
  ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
hX : ¬Subsingleton.{u_1 + 1} ↥X
𝒰 : X.OpenCover := X.openCoverOfIsOpenCover (fun (x : ↥X) ↦ { carrier := {x}, is_open' := ⋯ }) ⋯
⊢ ∀ (i : 𝒰.I₀), DiscreteTopology.{u_1} ↥(𝒰.X i)

Tactic:
have inst (i : _) : DiscreteTopology (𝒰.X i) := (𝒰.f i).isOpenEmbedding.discreteTopology
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst_1 : DiscreteTopology.{u_1} ↥X
inst_2 : IsReduced X
this :
  ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
hX : ¬Subsingleton.{u_1 + 1} ↥X
𝒰 : X.OpenCover := X.openCoverOfIsOpenCover (fun (x : ↥X) ↦ { carrier := {x}, is_open' := ⋯ }) ⋯
inst : ∀ (i : 𝒰.I₀), DiscreteTopology.{u_1} ↥(𝒰.X i)
⊢ ∀ (i : 𝒰.I₀), IsReduced.{u_1} (𝒰.X i)

Tactic:
have inst (i : _) : IsReduced (𝒰.X i) := isReduced_of_isOpenImmersion (𝒰.f i)
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst_1 : DiscreteTopology.{u_1} ↥X
inst_2 : IsReduced X
this :
  ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
hX : ¬Subsingleton.{u_1 + 1} ↥X
𝒰 : X.OpenCover := X.openCoverOfIsOpenCover (fun (x : ↥X) ↦ { carrier := {x}, is_open' := ⋯ }) ⋯
inst_3 : ∀ (i : 𝒰.I₀), DiscreteTopology.{u_1} ↥(𝒰.X i)
inst : ∀ (i : 𝒰.I₀), IsReduced.{u_1} (𝒰.X i)
⊢ IsLocallyArtinian X

Tactic:
(isLocallyArtinian_iff_openCover 𝒰).mpr
      fun i ↦ this (inferInstanceAs (Subsingleton ({i} : Set X)))

Premises used: Iff.mpr, AlgebraicGeometry.isLocallyArtinian_iff_openCover, _private.0.AlgebraicGeometry.instIsLocallyArtinianOfDiscreteTopologyCarrierCarrierCommRingCatOfIsReduced._proof_1
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst_1 : DiscreteTopology.{u_1} ↥X
inst_2 : IsReduced X
this :
  ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
hX : ¬Subsingleton.{u_1 + 1} ↥X
𝒰 : X.OpenCover := X.openCoverOfIsOpenCover (fun (x : ↥X) ↦ { carrier := {x}, is_open' := ⋯ }) ⋯
inst_3 : ∀ (i : 𝒰.I₀), DiscreteTopology.{u_1} ↥(𝒰.X i)
inst : ∀ (i : 𝒰.I₀), IsReduced.{u_1} (𝒰.X i)
⊢ IsLocallyArtinian X

Tactic:
exact (isLocallyArtinian_iff_openCover 𝒰).mpr
      fun i ↦ this (inferInstanceAs (Subsingleton ({i} : Set X)))

Premises used: Iff.mpr, AlgebraicGeometry.isLocallyArtinian_iff_openCover, _private.0.AlgebraicGeometry.instIsLocallyArtinianOfDiscreteTopologyCarrierCarrierCommRingCatOfIsReduced._proof_1
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
hX : Subsingleton.{u_1 + 1} ↥X
inl : IsEmpty.{u_1 + 1} ↥X → IsLocallyArtinian X
inr : Nonempty.{u_1 + 1} ↥X → IsLocallyArtinian X
⊢ IsLocallyArtinian X

Tactic:
cases isEmpty_or_nonempty X

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, isEmpty_or_nonempty, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
hX : Subsingleton.{u_1 + 1} ↥X
h : IsEmpty.{u_1 + 1} ↥X
⊢ IsLocallyArtinian X

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
hX : Subsingleton.{u_1 + 1} ↥X
h : Nonempty.{u_1 + 1} ↥X
⊢ IsIntegral X

Tactic:
have : IsIntegral X := (isIntegral_iff_irreducibleSpace_and_isReduced _).mpr
    ⟨⟨inferInstance⟩, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
hX : Subsingleton.{u_1 + 1} ↥X
h : Nonempty.{u_1 + 1} ↥X
this_1 : IsIntegral X
this : Field (↑Γ(X, ⊤) : Type u_1) := ⋯.toField
⊢ IsLocallyArtinian.{u_1} (Spec Γ(X, ⊤))

Tactic:
have : IsLocallyArtinian (Spec Γ(X, ⊤)) := Scheme.isLocallyArtinianScheme_Spec.mpr inferInstance
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
hX : Subsingleton.{u_1 + 1} ↥X
h : Nonempty.{u_1 + 1} ↥X
this_1 : IsIntegral X
this_2 : Field (↑Γ(X, ⊤) : Type u_1) := ⋯.toField
this : IsLocallyArtinian.{u_1} (Spec Γ(X, ⊤))
⊢ IsLocallyArtinian X

Tactic:
exact .of_isImmersion X.isoSpec.hom
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsArtinianScheme X
⊢ Finite.{u + 1} ↥X

Tactic:
finite_of_compact_of_discrete

Premises used: finite_of_compact_of_discrete
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
⊢ IsArtinianScheme X ↔ IsNoetherian X ∧ DiscreteTopology.{u} ↥X

Tactic:
aesop (add simp [isArtinianScheme_iff, isNoetherian_iff,
    IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology])

Premises used: AlgebraicGeometry.isNoetherian_iff, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, AlgebraicGeometry.isArtinianScheme_iff
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
R : CommRingCat
inst : IsArtinianRing.{u_1} (↑R : Type u_1)
⊢ IsArtinianScheme.{u_1} (Spec R)

Tactic:
IsArtinianScheme.iff_isNoetherian_and_discreteTopology.mpr
    ⟨inferInstance, inferInstanceAs (DiscreteTopology (PrimeSpectrum R))⟩

Premises used: Iff.mpr, _private.0.AlgebraicGeometry.instIsArtinianSchemeSpecOfIsArtinianRingCarrier._proof_1, inferInstance, AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology, And.intro
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
R : CommRingCat
⊢ IsArtinianScheme.{u_1} (Spec R) ↔ IsArtinianRing.{u_1} (↑R : Type u_1)

Tactic:
simp [isArtinianScheme_iff, (inferInstance : CompactSpace (Spec R))]

Premises used: inferInstance, AlgebraicGeometry.isArtinianScheme_iff
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g : X.PartialMap Y
mp : f = g → ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
mpr : (∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom) → f = g
⊢ f = g ↔ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
⊢ ∃ (e : f.domain = f.domain), f.hom = (X.isoOfEq e).hom ≫ f.hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g : X.PartialMap Y
mpr :
  ∀ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (f : (↑U : Scheme) ⟶ Y),
    (∃ (e : { domain := U, dense_domain := hU, hom := f : X.PartialMap Y }.domain = g.domain),
        { domain := U, dense_domain := hU, hom := f : X.PartialMap Y }.hom = (X.isoOfEq e).hom ≫ g.hom) →
      { domain := U, dense_domain := hU, hom := f : X.PartialMap Y } = g
⊢ (∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom) → f = g

Tactic:
obtain ⟨U, hU, f⟩ := f
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
g : X.PartialMap Y
U : X.Opens
hU : Dense (↑U : Set ↥X)
f : (↑U : Scheme) ⟶ Y
mpr :
  ∀ (V : X.Opens) (hV : Dense (↑V : Set ↥X)) (g : (↑V : Scheme) ⟶ Y),
    (∃ (e :
        { domain := U, dense_domain := hU, hom := f : X.PartialMap Y }.domain =
          { domain := V, dense_domain := hV, hom := g : X.PartialMap Y }.domain),
        { domain := U, dense_domain := hU, hom := f : X.PartialMap Y }.hom =
          (X.isoOfEq e).hom ≫ { domain := V, dense_domain := hV, hom := g }.hom) →
      { domain := U, dense_domain := hU, hom := f : X.PartialMap Y } = { domain := V, dense_domain := hV, hom := g }
⊢ (∃ (e : { domain := U, dense_domain := hU, hom := f : X.PartialMap Y }.domain = g.domain),
      { domain := U, dense_domain := hU, hom := f : X.PartialMap Y }.hom = (X.isoOfEq e).hom ≫ g.hom) →
    { domain := U, dense_domain := hU, hom := f : X.PartialMap Y } = g

Tactic:
obtain ⟨V, hV, g⟩ := g
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
U : X.Opens
hU : Dense (↑U : Set ↥X)
f : (↑U : Scheme) ⟶ Y
hV : Dense (↑U : Set ↥X)
g : (↑U : Scheme) ⟶ Y
e :
  { domain := U, dense_domain := hU, hom := f : X.PartialMap Y }.hom =
    (X.isoOfEq ⋯).hom ≫ { domain := U, dense_domain := hV, hom := g }.hom
mpr : f = g
⊢ { domain := U, dense_domain := hU, hom := f : X.PartialMap Y } = { domain := U, dense_domain := hV, hom := g }

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
U : X.Opens
hU : Dense (↑U : Set ↥X)
f : (↑U : Scheme) ⟶ Y
hV : Dense (↑U : Set ↥X)
g : (↑U : Scheme) ⟶ Y
e :
  { domain := U, dense_domain := hU, hom := f : X.PartialMap Y }.hom =
    (X.isoOfEq ⋯).hom ≫ { domain := U, dense_domain := hV, hom := g }.hom
⊢ f = g

Tactic:
simpa using e
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
rw : ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ f = g

Tactic:
rw [ext_iff]

Premises used: AlgebraicGeometry.Scheme.PartialMap.ext_iff
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
⟨e, H⟩

Premises used: Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom

Tactic:
exact ⟨e, H⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
e : (f.restrict f.domain ⋯ ⋯).domain = f.domain
H : (f.restrict f.domain ⋯ ⋯).hom = (X.isoOfEq ⋯).hom ≫ f.hom
⊢ f.restrict f.domain ⋯ ⋯ = f

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
⊢ (f.restrict f.domain ⋯ ⋯).domain = f.domain

Tactic:
simp [restrict_domain]

Premises used: AlgebraicGeometry.Scheme.PartialMap.restrict_domain
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
⊢ (f.restrict f.domain ⋯ ⋯).hom = (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
simp [restrict_domain]

Premises used: AlgebraicGeometry.Scheme.PartialMap.restrict_domain
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
⊢ (f.restrict f.domain ⋯ ⋯).hom = f.hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense (↑U : Set ↥X)
hU' : U ≤ f.domain
V : X.Opens
hV : Dense (↑V : Set ↥X)
hV' : V ≤ U
e : ((f.restrict U hU hU').restrict V hV hV').domain = (f.restrict V hV ⋯).domain
H : ((f.restrict U hU hU').restrict V hV hV').hom = (X.isoOfEq ⋯).hom ≫ (f.restrict V hV ⋯).hom
⊢ (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV ⋯

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense (↑U : Set ↥X)
hU' : U ≤ f.domain
V : X.Opens
hV : Dense (↑V : Set ↥X)
hV' : V ≤ U
⊢ ((f.restrict U hU hU').restrict V hV hV').domain = (f.restrict V hV ⋯).domain

Tactic:
simp [restrict_domain]

Premises used: AlgebraicGeometry.Scheme.PartialMap.restrict_domain
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense (↑U : Set ↥X)
hU' : U ≤ f.domain
V : X.Opens
hV : Dense (↑V : Set ↥X)
hV' : V ≤ U
⊢ ((f.restrict U hU hU').restrict V hV hV').hom = (X.isoOfEq ⋯).hom ≫ (f.restrict V hV ⋯).hom

Tactic:
simp [restrict_domain]

Premises used: AlgebraicGeometry.Scheme.PartialMap.restrict_domain
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense (↑U : Set ↥X)
hU' : U ≤ f.domain
V : X.Opens
hV : Dense (↑V : Set ↥X)
hV' : V ≤ U
⊢ ((f.restrict U hU hU').restrict V hV hV').hom = (f.restrict V hV ⋯).hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
⊢ IsOver S f ↔ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
⊢ f.domain ≤ (Hom.toPartialMap (X ↘ S)).domain

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = (Hom.toPartialMap (X ↘ S)).restrict f.domain ⋯ ⋯

Tactic:
simp [PartialMap.ext_iff]

Premises used: AlgebraicGeometry.Scheme.PartialMap.ext_iff
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
inst : IrreducibleSpace.{u} ↥X
U : X.Opens
hU : Dense (↑U : Set ↥X)
hU' : U ≤ f.domain
⊢ Eq (α := Spec X.functionField ⟶ Y) (f.restrict U hU hU').fromFunctionField f.fromFunctionField

Tactic:
fromSpecStalkOfMem_restrict f _ _ _

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_restrict
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
inst_1 : LocallyOfFiniteType sY
x : ↥X
inst_2 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ (ofFromSpecStalk sX sY φ h).hom ≫ sY = (ofFromSpecStalk sX sY φ h).domain.ι ≫ sX

Tactic:
(spread_out_of_isGermInjective' sX sY φ h).choose_spec.choose_spec.choose_spec.2

Premises used: Exists.choose_spec, And.right, Classical.choose, AlgebraicGeometry.spread_out_of_isGermInjective'
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
inst_1 : LocallyOfFiniteType sY
x : ↥X
inst_2 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ x ∈ (ofFromSpecStalk sX sY φ h).domain

Tactic:
(spread_out_of_isGermInjective' sX sY φ h).choose_spec.choose

Premises used: Exists.choose_spec, Set.Mem, Exists.choose, AlgebraicGeometry.spread_out_of_isGermInjective'
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
inst_1 : LocallyOfFiniteType sY
x : ↥X
inst_2 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ (ofFromSpecStalk sX sY φ h).fromSpecStalkOfMem ⋯ = φ

Tactic:
(spread_out_of_isGermInjective' sX sY φ h).choose_spec.choose_spec.choose_spec.1.symm

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem, Exists.choose_spec, And.left, Classical.choose, Eq.symm, AlgebraicGeometry.spread_out_of_isGermInjective'
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z : Scheme
f : X.PartialMap Y
g : Y ⟶ Z
x : ↥X
hx : x ∈ (f.compHom g).domain
⊢ (f.compHom g).fromSpecStalkOfMem hx = f.fromSpecStalkOfMem hx ≫ g

Tactic:
simp [fromSpecStalkOfMem]

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ (Hom.toPartialMap f).fromSpecStalkOfMem trivial = X.fromSpecStalk x ≫ f

Tactic:
simp [fromSpecStalkOfMem]

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
⊢ ∃ (hWl : f.domain ≤ f.domain) (hWr : f.domain ≤ f.domain),
    (f.restrict f.domain ⋯ hWl).hom = (f.restrict f.domain ⋯ hWr).hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g : X.PartialMap Y
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ g.equiv f

Tactic:
⟨W, hW, hWr, hWl, e.symm⟩

Premises used: AlgebraicGeometry.Scheme.PartialMap.equiv, Exists.intro, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g : X.PartialMap Y
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ g.equiv f

Tactic:
exact ⟨W, hW, hWr, hWl, e.symm⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense (↑W₁ : Set ↥X)
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : (f.restrict W₁ hW₁ hW₁l).hom = (g.restrict W₁ hW₁ hW₁r).hom
this :
  ∀ (W₂ : X.Opens) (hW₂ : Dense (↑W₂ : Set ↥X)) (hW₂l : W₂ ≤ g.domain) (hW₂r : W₂ ≤ h.domain)
    (e₂ : (g.restrict W₂ hW₂ hW₂l).hom = (h.restrict W₂ hW₂ hW₂r).hom), f.equiv h
⊢ g.equiv h → f.equiv h

Tactic:
⟨W₂, hW₂, hW₂l, hW₂r, e₂⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense (↑W₁ : Set ↥X)
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : (f.restrict W₁ hW₁ hW₁l).hom = (g.restrict W₁ hW₁ hW₁r).hom
W₂ : X.Opens
hW₂ : Dense (↑W₂ : Set ↥X)
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : (g.restrict W₂ hW₂ hW₂l).hom = (h.restrict W₂ hW₂ hW₂r).hom
⊢ f.equiv h

Tactic:
⟨W₁ ⊓ W₂, hW₁.inter_of_isOpen_left hW₂ W₁.2, inf_le_left.trans hW₁l,
      inf_le_right.trans hW₂r, ?_⟩

Premises used: AlgebraicGeometry.Scheme.PartialMap.equiv, inf_le_right, Dense.inter_of_isOpen_left, Exists.intro, TopologicalSpace.Opens.is_open', inf_le_left, LE.le.trans, Min.min
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense (↑W₁ : Set ↥X)
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : (f.restrict W₁ hW₁ hW₁l).hom = (g.restrict W₁ hW₁ hW₁r).hom
W₂ : X.Opens
hW₂ : Dense (↑W₂ : Set ↥X)
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : (g.restrict W₂ hW₂ hW₂l).hom = (h.restrict W₂ hW₂ hW₂r).hom
refine : (f.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom = (h.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom
⊢ f.equiv h

Tactic:
refine ⟨W₁ ⊓ W₂, hW₁.inter_of_isOpen_left hW₂ W₁.2, inf_le_left.trans hW₁l,
      inf_le_right.trans hW₂r, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense (↑W₁ : Set ↥X)
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : X.homOfLE hW₁l ≫ f.hom = X.homOfLE hW₁r ≫ g.hom
W₂ : X.Opens
hW₂ : Dense (↑W₂ : Set ↥X)
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : X.homOfLE hW₂l ≫ g.hom = X.homOfLE hW₂r ≫ h.hom
simp : X.homOfLE ⋯ ≫ X.homOfLE hW₁r ≫ g.hom = X.homOfLE ⋯ ≫ X.homOfLE hW₂l ≫ g.hom
⊢ (f.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom = (h.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom

Tactic:
simp only [restrict_domain, restrict_hom, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_left hW₁l,
      Category.assoc, e₁, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_right hW₂r, ← e₂]

Premises used: CategoryTheory.Category.assoc, inf_le_right, AlgebraicGeometry.Scheme.homOfLE_homOfLE, AlgebraicGeometry.Scheme.PartialMap.restrict_hom, inf_le_left, AlgebraicGeometry.Scheme.PartialMap.restrict_domain
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense (↑W₁ : Set ↥X)
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : X.homOfLE hW₁l ≫ f.hom = X.homOfLE hW₁r ≫ g.hom
W₂ : X.Opens
hW₂ : Dense (↑W₂ : Set ↥X)
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : X.homOfLE hW₂l ≫ g.hom = X.homOfLE hW₂r ≫ h.hom
⊢ X.homOfLE ⋯ ≫ X.homOfLE hW₁r ≫ g.hom = X.homOfLE ⋯ ≫ X.homOfLE hW₂l ≫ g.hom

Tactic:
simp only [homOfLE_homOfLE_assoc]

Premises used: AlgebraicGeometry.Scheme.homOfLE_homOfLE_assoc