awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
e : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f.toRationalMap
have mpr : ∀ (U : X.Opens) (hU : Dense (↑U : Set ↥X))
  (hUl : U ≤ PartialMap.domain (Y := S) ((fun (x : X.PartialMap Y) ↦ x.compHom (Y ↘ S)) f))
  (hUr : U ≤ (Hom.toPartialMap (X ↘ S)).domain)
  (e :
    (PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom (Y ↘ S)) f) U hU hUl).hom =
      ((Hom.toPartialMap (X ↘ S)).restrict U hU hUr).hom),
  IsOver S f.toRationalMap
Tactic: obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : S.IsSeparated
f : X.PartialMap Y
⊢ RationalMap.IsOver S f.toRationalMap ↔ IsOver S f
have refine : RationalMap.IsOver S f.toRationalMap → IsOver S f
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : S.IsSeparated
f : X.PartialMap Y
h : RationalMap.IsOver S f.toRationalMap
⊢ IsOver S f
have obtain : ∀ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hU' : U ≤ f.domain) (H : IsOver S (f.restrict U hU hU')), IsOver S f
Tactic: obtain ⟨U, hU, hU', H⟩ := f.exists_restrict_isOver (S := S)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : S.IsSeparated
f : X.PartialMap Y
h : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense (↑U : Set ↥X)
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
⊢ IsOver S f
have rw : (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S
Tactic: rw [isOver_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : S.IsSeparated
f : X.PartialMap Y
h : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense (↑U : Set ↥X)
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
⊢ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S
have this : IsDominant (X.homOfLE hU')
Tactic: have : IsDominant (X.homOfLE hU') := Opens.isDominant_homOfLE hU _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f : X ⤏ Y
⊢ Spec X.functionField ⟶ Y
have refine : ∀ (a b : X.PartialMap Y), a ≈ b → Eq (α := Spec X.functionField ⟶ Y) a.fromFunctionField b.fromFunctionField
Tactic: refine Quotient.lift PartialMap.fromFunctionField ?_ f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f_1 : X ⤏ Y
f g : X.PartialMap Y
⊢ f ≈ g → Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField
have this : ∀ (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),
  Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField
Tactic: ⟨W, hW, hWl, hWr, e⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f_1 : X ⤏ Y
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
⊢ f.restrict W hW hWl = g.restrict W hW hWr
have e₁ : (f.restrict W hW hWl).domain = (g.restrict W hW hWr).domain
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f_1 : X ⤏ Y
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
e₁ : (f.restrict W hW hWl).domain = (g.restrict W hW hWr).domain
⊢ f.restrict W hW hWl = g.restrict W hW hWr
have H : (f.restrict W hW hWl).hom = (X.isoOfEq sorry).hom ≫ (g.restrict W hW hWr).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f_1 : X ⤏ Y
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
⊢ (f.restrict W hW hWl).hom = (X.isoOfEq ⋯).hom ≫ (g.restrict W hW hWr).hom
have H : (g.restrict W hW hWr).hom = (X.isoOfEq sorry).hom ≫ (g.restrict W hW hWr).hom
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f_1 : X ⤏ Y
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
⊢ Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField
have this : f.restrict W hW hWl = g.restrict W hW hWr
Tactic: have : f.restrict W hW hWl = g.restrict W hW hWr := by
    ext1
    · rfl
    rw [e]; simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f_1 : X ⤏ Y
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
this : f.restrict W hW hWl = g.restrict W hW hWr
⊢ Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField
have rw : Eq (α := Spec X.functionField ⟶ Y) (f.restrict W hW hWl).fromFunctionField g.fromFunctionField
Tactic: rw [← f.fromFunctionField_restrict hW hWl, this, g.fromFunctionField_restrict]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f_1 : X ⤏ Y
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
this : f.restrict W hW hWl = g.restrict W hW hWr
rw : Eq (α := Spec X.functionField ⟶ Y) (f.restrict W hW hWl).fromFunctionField g.fromFunctionField
⊢ Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField
have rw₁ : Eq (α := Spec X.functionField ⟶ Y) (g.restrict W hW hWr).fromFunctionField g.fromFunctionField
Tactic: rw [← f.fromFunctionField_restrict hW hWl, this, g.fromFunctionField_restrict]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f_1 : X ⤏ Y
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
this : f.restrict W hW hWl = g.restrict W hW hWr
rw : Eq (α := Spec X.functionField ⟶ Y) (f.restrict W hW hWl).fromFunctionField g.fromFunctionField
rw₁ : Eq (α := Spec X.functionField ⟶ Y) (g.restrict W hW hWr).fromFunctionField g.fromFunctionField
⊢ Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField
have rw₂ : Eq (α := Spec X.functionField ⟶ Y) g.fromFunctionField g.fromFunctionField
Tactic: rw [← f.fromFunctionField_restrict hW hWl, this, g.fromFunctionField_restrict]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IsIntegral X
f g : X ⤏ Y
H : Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField
⊢ f = g
have obtain : ∀ (f : X.PartialMap Y) (H : Eq (α := Spec X.functionField ⟶ Y) f.toRationalMap.fromFunctionField g.fromFunctionField),
  f.toRationalMap = g
Tactic: obtain ⟨f, rfl⟩ := f.exists_rep
Cleared hypotheses: f, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IsIntegral X
g : X ⤏ Y
f : X.PartialMap Y
H : Eq (α := Spec X.functionField ⟶ Y) f.toRationalMap.fromFunctionField g.fromFunctionField
⊢ f.toRationalMap = g
have obtain : ∀ (g : X.PartialMap Y)
  (H : Eq (α := Spec X.functionField ⟶ Y) f.toRationalMap.fromFunctionField g.toRationalMap.fromFunctionField),
  f.toRationalMap = g.toRationalMap
Tactic: obtain ⟨g, rfl⟩ := g.exists_rep
Cleared hypotheses: g, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IsIntegral X
f g : X.PartialMap Y
H : Eq (α := Spec X.functionField ⟶ Y) f.toRationalMap.fromFunctionField g.toRationalMap.fromFunctionField
⊢ f.toRationalMap = g.toRationalMap
have refine : f.equiv g
Tactic: refine PartialMap.toRationalMap_eq_iff.mpr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsIntegral X
inst_1 : LocallyOfFiniteType sY
f : { f : X ⤏ Y // f.compHom sY = Hom.toRationalMap sX }
⊢ Eq (α := Spec X.functionField ⟶ S) ((↑f : X ⤏ Y).fromFunctionField ≫ sY) (X.fromSpecStalk (genericPoint ↥X) ≫ sX)
have obtain : ∀ (f : X ⤏ Y) (hf : f.compHom sY = Hom.toRationalMap sX),
  Eq (α := Spec X.functionField ⟶ S)
    ((↑(Subtype.mk (p := fun (f : X ⤏ Y) ↦ f.compHom sY = Hom.toRationalMap sX) f hf) : X ⤏ Y).fromFunctionField ≫ sY)
    (X.fromSpecStalk (genericPoint ↥X) ≫ sX)
Tactic: obtain ⟨f, hf⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsIntegral X
inst_1 : LocallyOfFiniteType sY
f : X ⤏ Y
hf : f.compHom sY = Hom.toRationalMap sX
⊢ Eq (α := Spec X.functionField ⟶ S)
    ((↑(Subtype.mk (p := fun (f : X ⤏ Y) ↦ f.compHom sY = Hom.toRationalMap sX) f hf) : X ⤏ Y).fromFunctionField ≫ sY)
    (X.fromSpecStalk (genericPoint ↥X) ≫ sX)
have obtain : ∀ (f : X.PartialMap Y) (hf : f.toRationalMap.compHom sY = Hom.toRationalMap sX),
  Eq (α := Spec X.functionField ⟶ S)
    ((↑(Subtype.mk (p := fun (f : X ⤏ Y) ↦ f.compHom sY = Hom.toRationalMap sX) f.toRationalMap hf) :
          X ⤏ Y).fromFunctionField ≫
      sY)
    (X.fromSpecStalk (genericPoint ↥X) ≫ sX)
Tactic: obtain ⟨f, rfl⟩ := f.exists_rep
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsIntegral X
inst_3 : LocallyOfFiniteType (Y ↘ S)
⊢ Eq.{max 1 (u + 1)} (α := (Spec X.functionField ⟶ Y) → Prop) (fun (f : Spec X.functionField ⟶ Y) ↦ Hom.IsOver f S)
    fun (f : Spec X.functionField ⟶ Y) ↦ f ≫ Y ↘ S = X.fromSpecStalk (genericPoint ↥X) ≫ X ↘ S
have simp : Eq.{max 1 (u + 1)} (α := (Spec X.functionField ⟶ Y) → Prop)
  (fun (f : Spec X.functionField ⟶ Y) ↦ f ≫ Y ↘ S = Spec X.functionField ↘ S) fun (f : Spec X.functionField ⟶ Y) ↦
  f ≫ Y ↘ S = X.fromSpecStalk (genericPoint ↥X) ≫ X ↘ S
Tactic: simp only [Hom.isOver_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsIntegral X
inst_3 : LocallyOfFiniteType (Y ↘ S)
⊢ Eq.{max 1 (u + 1)} (α := (X ⤏ Y) → Prop) (fun (f : X ⤏ Y) ↦ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S))
    fun (f : X ⤏ Y) ↦ IsOver S f
have h : ∀ (f : X ⤏ Y), f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) ↔ IsOver S f
Tactic: ext f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsIntegral X
inst_3 : LocallyOfFiniteType (Y ↘ S)
f : X ⤏ Y
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) ↔ IsOver S f
have h : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) ↔ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
Tactic: rw [RationalMap.isOver_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
⊢ X.PartialMap Y
have refine : ∀ (x y : f.openCoverDomain.I₀),
  Eq (α := Limits.pullback (f.openCoverDomain.f x) (f.openCoverDomain.f y) ⟶ Y)
    (Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq sorry) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  sorry).hom :
            f.openCoverDomain.X x ⟶ Y))
        x)
    (Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq sorry) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  sorry).hom :
            f.openCoverDomain.X x ⟶ Y))
        y)
Tactic: refine ⟨f.domain, f.dense_domain, f.openCoverDomain.glueMorphisms
    (fun x ↦ (X.isoOfEq x.2.choose_spec.2).inv ≫ x.2.choose.hom) ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : (x : f.openCoverDomain.I₀) → X.PartialMap Y :=
  fun (x : f.openCoverDomain.I₀) ↦
    Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯
⊢ Eq (α := Limits.pullback (f.openCoverDomain.f x) (f.openCoverDomain.f y) ⟶ Y)
    (Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq ⋯) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  ⋯).hom :
            f.openCoverDomain.X x ⟶ Y))
        x)
    (Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq ⋯) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  ⋯).hom :
            f.openCoverDomain.X x ⟶ Y))
        y)
have hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
Tactic: have hg₁ (x) : (g x).toRationalMap = f := x.2.choose_spec.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : (x : f.openCoverDomain.I₀) → X.PartialMap Y :=
  fun (x : f.openCoverDomain.I₀) ↦
    Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
⊢ Eq (α := Limits.pullback (f.openCoverDomain.f x) (f.openCoverDomain.f y) ⟶ Y)
    (Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq ⋯) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  ⋯).hom :
            f.openCoverDomain.X x ⟶ Y))
        x)
    (Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq ⋯) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  ⋯).hom :
            f.openCoverDomain.X x ⟶ Y))
        y)
have hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = (↑x : X.Opens)
Tactic: have hg₂ (x) : (g x).domain = x.1 := x.2.choose_spec.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : (x : f.openCoverDomain.I₀) → X.PartialMap Y :=
  fun (x : f.openCoverDomain.I₀) ↦
    Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = (↑x : X.Opens)
⊢ Eq (α := Limits.pullback (f.openCoverDomain.f x) (f.openCoverDomain.f y) ⟶ Y)
    (Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq ⋯) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  ⋯).hom :
            f.openCoverDomain.X x ⟶ Y))
        x)
    (Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq ⋯) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  ⋯).hom :
            f.openCoverDomain.X x ⟶ Y))
        y)
have refine : Eq (α := (↑((↑x : X.Opens) ⊓ (↑y : X.Opens)) : Scheme) ⟶ Y)
  (CategoryStruct.comp (Y := Limits.pullback (X.homOfLE sorry) (X.homOfLE sorry)) (Iso.hom sorry.isoPullback)
    (Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq sorry) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  sorry).hom :
            f.openCoverDomain.X x ⟶ Y))
        x))
  (CategoryStruct.comp (Y := Limits.pullback (X.homOfLE sorry) (X.homOfLE sorry)) (Iso.hom sorry.isoPullback)
    (Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
      (fun (x : f.openCoverDomain.I₀) ↦
          (Iso.inv (X.isoOfEq sorry) ≫
              (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                  sorry).hom :
            f.openCoverDomain.X x ⟶ Y))
        y))
Tactic: refine (cancel_epi (isPullback_opens_inf_le (le_sSup x.2) (le_sSup y.2)).isoPullback.hom).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : (x : f.openCoverDomain.I₀) → X.PartialMap Y :=
  fun (x : f.openCoverDomain.I₀) ↦
    Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = (↑x : X.Opens)
⊢ Eq (α := (↑((↑x : X.Opens) ⊓ (↑y : X.Opens)) : Scheme) ⟶ Y)
    (CategoryStruct.comp (Y := Limits.pullback (X.homOfLE ⋯) (X.homOfLE ⋯)) (Iso.hom ⋯.isoPullback)
      (Limits.pullback.fst (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
        (fun (x : f.openCoverDomain.I₀) ↦
            (Iso.inv (X.isoOfEq ⋯) ≫
                (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                    ⋯).hom :
              f.openCoverDomain.X x ⟶ Y))
          x))
    (CategoryStruct.comp (Y := Limits.pullback (X.homOfLE ⋯) (X.homOfLE ⋯)) (Iso.hom ⋯.isoPullback)
      (Limits.pullback.snd (f.openCoverDomain.f x) (f.openCoverDomain.f y) ≫
        (fun (x : f.openCoverDomain.I₀) ↦
            (Iso.inv (X.isoOfEq ⋯) ≫
                (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens))
                    ⋯).hom :
              f.openCoverDomain.X x ⟶ Y))
          y))
have simp : Eq (α := (↑((↑x : X.Opens) ⊓ (↑y : X.Opens)) : Scheme) ⟶ Y)
  (X.homOfLE sorry ≫
    Iso.inv (X.isoOfEq sorry) ≫
      (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) sorry).hom)
  (X.homOfLE sorry ≫
    Iso.inv (X.isoOfEq sorry) ≫
      (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑y : X.Opens)) sorry).hom)
Tactic: simp only [openCoverDomain, IsPullback.isoPullback_hom_fst_assoc,
    IsPullback.isoPullback_hom_snd_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : (x : f.openCoverDomain.I₀) → X.PartialMap Y :=
  fun (x : f.openCoverDomain.I₀) ↦
    Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = (↑x : X.Opens)
⊢ Eq (α := (↑((↑x : X.Opens) ⊓ (↑y : X.Opens)) : Scheme) ⟶ Y) (X.homOfLE ⋯ ≫ Iso.inv (X.isoOfEq ⋯) ≫ (g x).hom)
    (X.homOfLE ⋯ ≫ Iso.inv (X.isoOfEq ⋯) ≫ (g y).hom)
have simp_rw : ((Iso.hom (X.isoOfEq sorry) ≫ X.homOfLE sorry) ≫ Iso.inv (X.isoOfEq sorry)) ≫ (g x).hom =
  ((Iso.hom (X.isoOfEq sorry) ≫ X.homOfLE sorry) ≫ Iso.inv (X.isoOfEq sorry)) ≫ (g y).hom
Tactic: simp_rw [← cancel_epi (X.isoOfEq congr($(hg₂ x) ⊓ $(hg₂ y))).hom, ← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : (x : f.openCoverDomain.I₀) → X.PartialMap Y :=
  fun (x : f.openCoverDomain.I₀) ↦
    Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = (↑x : X.Opens)
⊢ ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g x).hom =
    ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g y).hom
have h : ((↑((g x).domain ⊓ (g y).domain) : Scheme) ⟶ Y) =
    ((↑((g x).restrict ((g x).domain ⊓ (g y).domain) sorry sorry).domain : Scheme) ⟶ Y) →
  ((Iso.hom (X.isoOfEq sorry) ≫ X.homOfLE sorry) ≫ Iso.inv (X.isoOfEq sorry)) ≫ (g x).hom =
    ((g x).restrict ((g x).domain ⊓ (g y).domain) sorry sorry).hom
Tactic: convert! (PartialMap.equiv_iff_of_isSeparated (S := ⊤_ _) (f := g x) (g := g y)).mp ?_ using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : (x : f.openCoverDomain.I₀) → X.PartialMap Y :=
  fun (x : f.openCoverDomain.I₀) ↦
    Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = (↑x : X.Opens)
h :
  ((↑((g x).domain ⊓ (g y).domain) : Scheme) ⟶ Y) =
      ((↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain : Scheme) ⟶ Y) →
    ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g x).hom =
      ((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom
⊢ ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g x).hom =
    ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g y).hom
have h₁ : ((↑((g x).domain ⊓ (g y).domain) : Scheme) ⟶ Y) =
    ((↑((g x).restrict ((g x).domain ⊓ (g y).domain) sorry sorry).domain : Scheme) ⟶ Y) →
  ((Iso.hom (X.isoOfEq sorry) ≫ X.homOfLE sorry) ≫ Iso.inv (X.isoOfEq sorry)) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) sorry sorry).hom
Tactic: convert! (PartialMap.equiv_iff_of_isSeparated (S := ⊤_ _) (f := g x) (g := g y)).mp ?_ using 1