awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
⊢ IsLocallyArtinian X ↔ ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
have refine : ∀ (H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)), IsLocallyArtinian X
Tactic: refine ⟨fun h ↦ inferInstance, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
⊢ IsLocallyArtinian X
have refine_1 : IsLocallyNoetherian X
Tactic: refine IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
refine_1 : IsLocallyNoetherian X
⊢ IsLocallyArtinian X
have refine_2 : DiscreteTopology.{u} ↥X
Tactic: refine IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
⊢ DiscreteTopology.{u} ↥X
have refine_2 : ∀ (x : ↥X), IsOpen (X := ↥X) {x}
Tactic: refine discreteTopology_iff_isOpen_singleton.mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
x : ↥X
⊢ IsOpen (X := ↥X) {x}
have refine_2 : ∀ (i : 𝒰.I₀) (x : ↥(𝒰.X i)), IsOpen (X := ↥X) (singleton (α := ↥X) ((𝒰.f i) x : ↥X))
Tactic: obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
⊢ IsLocallyArtinian X ↔ ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)
have refine : ∀ (H : ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)), IsLocallyArtinian X
Tactic: refine ⟨fun _ _ ↦ IsLocallyArtinian.isArtinianRing_presheaf_obj ⟨_, hU' _⟩, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
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)
⊢ IsLocallyArtinian X
have rw : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsLocallyArtinian.{u} ((X.openCoverOfIsOpenCover U hU).X i)
Tactic: rw [isLocallyArtinian_iff_openCover (X.openCoverOfIsOpenCover U hU)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
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 : (X.openCoverOfIsOpenCover U hU).I₀), IsLocallyArtinian.{u} ((X.openCoverOfIsOpenCover U hU).X i)
have this : ∀ (i : ι), IsLocallyArtinian.{u} (Spec Γ(X, U i))
Tactic: have : ∀ i, IsLocallyArtinian (Spec Γ(X, U i)) := by simpa
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : DiscreteTopology.{u_1} ↥X
inst_1 : IsReduced X
⊢ IsLocallyArtinian X
have 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
Tactic: wlog hX : Subsingleton X generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
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
⊢ IsLocallyArtinian X
have wlog : ∀ {X : Scheme.{u_1}} [DiscreteTopology.{u_1} ↥X] [IsReduced X] (hX : Subsingleton.{u_1 + 1} ↥X), IsLocallyArtinian X
Tactic: wlog hX : Subsingleton X generalizing X
Cleared hypotheses: X, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
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
⊢ Eq.{u_1 + 1} (α := TopologicalSpace.Opens ↥X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ }) ⊤
have h : ∀ (x : ↥X),
  x ∈ (↑(⨆ (x : ↥X), { carrier := {x}, is_open' := sorry : TopologicalSpace.Opens ↥X }) : Set ↥X) ↔ x ∈ (↑⊤ : Set ↥X)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
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' := ⋯ }) ⋯
⊢ IsLocallyArtinian X
have inst : ∀ (i : 𝒰.I₀), DiscreteTopology.{u_1} ↥(𝒰.X i)
Tactic: have inst (i : _) : DiscreteTopology (𝒰.X i) := (𝒰.f i).isOpenEmbedding.discreteTopology
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
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)
⊢ IsLocallyArtinian X
have inst₁ : ∀ (i : 𝒰.I₀), IsReduced.{u_1} (𝒰.X i)
Tactic: have inst (i : _) : IsReduced (𝒰.X i) := isReduced_of_isOpenImmersion (𝒰.f i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
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
⊢ IsLocallyArtinian X
have inl : IsEmpty.{u_1 + 1} ↥X → IsLocallyArtinian X
Tactic: cases isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
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
⊢ IsLocallyArtinian X
have inr : Nonempty.{u_1 + 1} ↥X → IsLocallyArtinian X
Tactic: cases isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
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
⊢ IsLocallyArtinian X
have this : IsIntegral X
Tactic: have : IsIntegral X := (isIntegral_iff_irreducibleSpace_and_isReduced _).mpr
    ⟨⟨inferInstance⟩, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
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 X
have this₁ : IsLocallyArtinian.{u_1} (Spec Γ(X, ⊤))
Tactic: have : IsLocallyArtinian (Spec Γ(X, ⊤)) := Scheme.isLocallyArtinianScheme_Spec.mpr inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
f g : X.PartialMap Y
⊢ f = g ↔ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
have mp : f = g → ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ f = g ↔ ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
have mpr : (∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom) → f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
f g : X.PartialMap Y
⊢ (∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom) → f = g
have 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
Tactic: obtain ⟨U, hU, f⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
g : X.PartialMap Y
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
have 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 }
Tactic: obtain ⟨V, hV, g⟩ := g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ { domain := U, dense_domain := hU, hom := f : X.PartialMap Y } = { domain := U, dense_domain := hV, hom := g }
have mpr : f = g
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
f g : X.PartialMap Y
e : f.domain = g.domain
H : f.hom = (X.isoOfEq e).hom ≫ g.hom
⊢ f = g
have rw : ∃ (e : f.domain = g.domain), f.hom = (X.isoOfEq e).hom ≫ g.hom
Tactic: rw [ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
f : X.PartialMap Y
⊢ f.restrict f.domain ⋯ ⋯ = f
have e : (f.restrict f.domain sorry sorry).domain = f.domain
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
f : X.PartialMap Y
e : (f.restrict f.domain ⋯ ⋯).domain = f.domain
⊢ f.restrict f.domain ⋯ ⋯ = f
have H : (f.restrict f.domain sorry sorry).hom = (X.isoOfEq sorry).hom ≫ f.hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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' = f.restrict V hV ⋯
have e : ((f.restrict U hU hU').restrict V hV hV').domain = (f.restrict V hV sorry).domain
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV ⋯
have H : ((f.restrict U hU hU').restrict V hV hV').hom = (X.isoOfEq sorry).hom ≫ (f.restrict V hV sorry).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ g.equiv h → f.equiv h
have 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
Tactic: ⟨W₂, hW₂, hW₂l, hW₂r, e₂⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
have refine : (f.restrict (W₁ ⊓ W₂) sorry sorry).hom = (h.restrict (W₁ ⊓ W₂) sorry sorry).hom
Tactic: refine ⟨W₁ ⊓ W₂, hW₁.inter_of_isOpen_left hW₂ W₁.2, inf_le_left.trans hW₁l,
      inf_le_right.trans hW₂r, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ (f.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom = (h.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom
have simp : X.homOfLE sorry ≫ X.homOfLE hW₁r ≫ g.hom = X.homOfLE sorry ≫ X.homOfLE hW₂l ≫ g.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₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
⊢ f.equiv g
have hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
Tactic: have hdense : Dense ((f.domain ⊓ g.domain) : Set X) :=
    f.dense_domain.inter_of_isOpen_left g.dense_domain f.domain.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
⊢ f.equiv g
have this : IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x sorry)
Tactic: have := (isGermInjectiveAt_iff_of_isOpenImmersion (f := (f.domain ⊓ g.domain).ι)
    (x := ⟨x, hxf, hxg⟩)).mp ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
⊢ f.equiv g
have refine_2 : ∀
  (this :
    ∃ (U : (↑(f.domain ⊓ g.domain) : Scheme).Opens),
      Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x sorry ∈ U ∧
        U.ι ≫ X.homOfLE sorry ≫ f.hom = U.ι ≫ X.homOfLE sorry ≫ g.hom),
  f.equiv g
Tactic: have := spread_out_unique_of_isGermInjective' (X := (f.domain ⊓ g.domain).toScheme)
    (X.homOfLE inf_le_left ≫ f.hom) (X.homOfLE inf_le_right ≫ g.hom) (x := ⟨x, hxf, hxg⟩) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
refine_2 :
  ∀
    (this :
      ∃ (U : (↑(f.domain ⊓ g.domain) : Scheme).Opens),
        Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U ∧
          U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom),
    f.equiv g
⊢ f.equiv g
have refine_1 : Eq (α :=
  Spec
      ((↑(f.domain ⊓ g.domain) : Scheme).presheaf.stalk
        (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x sorry)) ⟶
    Y)
  ((↑(f.domain ⊓ g.domain) : Scheme).fromSpecStalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x sorry) ≫
    X.homOfLE sorry ≫ f.hom)
  ((↑(f.domain ⊓ g.domain) : Scheme).fromSpecStalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x sorry) ≫
    X.homOfLE sorry ≫ g.hom)
Tactic: have := spread_out_unique_of_isGermInjective' (X := (f.domain ⊓ g.domain).toScheme)
    (X.homOfLE inf_le_left ≫ f.hom) (X.homOfLE inf_le_right ≫ g.hom) (x := ⟨x, hxf, hxg⟩) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this_1 :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
this :
  ∃ (U : (↑(f.domain ⊓ g.domain) : Scheme).Opens),
    Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U ∧
      U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ f.equiv g
have refine_2 : ∀ (U : (↑(f.domain ⊓ g.domain) : Scheme).Opens) (hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x sorry ∈ U)
  (e : U.ι ≫ X.homOfLE sorry ≫ f.hom = U.ι ≫ X.homOfLE sorry ≫ g.hom), f.equiv g
Tactic: obtain ⟨U, hxU, e⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ f.equiv g
have refine_2 : (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) sorry sorry).hom = (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) sorry sorry).hom
Tactic: refine ⟨(f.domain ⊓ g.domain).ι ''ᵁ U, ((f.domain ⊓ g.domain).ι ''ᵁ U).2.dense
      ⟨_, ⟨_, hxU, rfl⟩⟩,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom = (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom
have refine_2 : Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U) ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) sorry sorry).hom =
  Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U) ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) sorry sorry).hom
Tactic: rw [← cancel_epi (Scheme.Hom.isoImage _ _).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U) ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom =
    Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U) ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom
have refine_2 : ∀ (e : (U.ι ≫ X.homOfLE sorry) ≫ f.hom = (U.ι ≫ X.homOfLE sorry) ≫ g.hom),
  CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE sorry) ≫
      f.hom =
    CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE sorry) ≫
      g.hom
Tactic: simp only [restrict_hom, ← Category.assoc] at e ⊢
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      f.hom =
    CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      g.hom
have h : CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
    (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE sorry) =
  U.ι ≫ X.homOfLE sorry
Tactic: convert! e using 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
h :
  CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
      (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) =
    U.ι ≫ X.homOfLE ⋯
⊢ CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      f.hom =
    CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      g.hom
have h₁ : CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
    (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE sorry) =
  U.ι ≫ X.homOfLE sorry
Tactic: convert! e using 2