awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
refine : RationalMap.IsOver S f.toRationalMap → IsOver S f
⊢ RationalMap.IsOver S f.toRationalMap ↔ IsOver S f

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
obtain :
  ∀ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hU' : U ≤ f.domain) (H : IsOver S (f.restrict U hU hU')), IsOver S f
⊢ IsOver S f

Tactic:
obtain ⟨U, hU, hU', H⟩ := f.exists_restrict_isOver (S := S)

Premises used: AlgebraicGeometry.Scheme.PartialMap.exists_restrict_isOver
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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')
rw : (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S
⊢ IsOver S f

Tactic:
rw [isOver_iff]

Premises used: AlgebraicGeometry.Scheme.PartialMap.isOver_iff
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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')
⊢ IsDominant (X.homOfLE hU')

Tactic:
have : IsDominant (X.homOfLE hU') := Opens.isDominant_homOfLE hU _
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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')
this : IsDominant (X.homOfLE hU')
⊢ X.homOfLE hU' ≫ (f.compHom (Y ↘ S)).hom = X.homOfLE hU' ≫ f.domain.ι ≫ X ↘ S

Tactic:
simpa using H.1

Premises used: CategoryTheory.HomIsOver.comp_over
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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')
this : IsDominant (X.homOfLE hU')
⊢ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Tactic:
exact ext_of_isDominant (ι := X.homOfLE hU') (by simpa using H.1)

Premises used: AlgebraicGeometry.Scheme.homOfLE, AlgebraicGeometry.ext_of_isDominant
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IrreducibleSpace.{u} ↥X
f : X ⤏ Y
refine : ∀ (a b : X.PartialMap Y), a ≈ b → Eq (α := Spec X.functionField ⟶ Y) a.fromFunctionField b.fromFunctionField
⊢ Spec X.functionField ⟶ Y

Tactic:
refine Quotient.lift PartialMap.fromFunctionField ?_ f

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromFunctionField, Quotient.lift
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
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
⊢ f ≈ g → Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField

Tactic:
⟨W, hW, hWl, hWr, e⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
H : (f.restrict W hW hWl).hom = (X.isoOfEq ⋯).hom ≫ (g.restrict W hW hWr).hom
⊢ f.restrict W hW hWl = g.restrict W hW hWr

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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).domain = (g.restrict W hW hWr).domain

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
H : (g.restrict W hW hWr).hom = (X.isoOfEq ⋯).hom ≫ (g.restrict W hW hWr).hom
⊢ (f.restrict W hW hWl).hom = (X.isoOfEq ⋯).hom ≫ (g.restrict W hW hWr).hom

Tactic:
rw [e]
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
⊢ (g.restrict W hW hWr).hom = (X.isoOfEq ⋯).hom ≫ (g.restrict W hW hWr).hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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

Tactic:
have : f.restrict W hW hWl = g.restrict W hW hWr := by
    ext1
    · rfl
    rw [e]; simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
rw₂ rw₃ : Eq (α := Spec X.functionField ⟶ Y) g.fromFunctionField g.fromFunctionField
⊢ Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField

Tactic:
rw [← f.fromFunctionField_restrict hW hWl, this, g.fromFunctionField_restrict]

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromFunctionField_restrict
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
f : X.PartialMap Y
⊢ Eq (α := Spec X.functionField ⟶ Y) f.toRationalMap.fromFunctionField f.fromFunctionField

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem, AlgebraicGeometry.Scheme.RationalMap.fromFunctionField, rfl
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsIntegral X
inst_1 : LocallyOfFiniteType sY
f : Spec X.functionField ⟶ Y
h : f ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX
⊢ (ofFunctionField sX sY f h).fromFunctionField = f

Tactic:
PartialMap.fromSpecStalkOfMem_ofFromSpecStalk sX sY _ _

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem, AlgebraicGeometry.Scheme.RationalMap.fromFunctionField, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_ofFromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsIntegral X
f g : X ⤏ Y
H : Eq (α := Spec X.functionField ⟶ Y) f.fromFunctionField g.fromFunctionField
obtain :
  ∀ (f : X.PartialMap Y) (H : Eq (α := Spec X.functionField ⟶ Y) f.toRationalMap.fromFunctionField g.fromFunctionField),
    f.toRationalMap = g
⊢ f = g

Tactic:
obtain ⟨f, rfl⟩ := f.exists_rep

Premises used: rfl, AlgebraicGeometry.Scheme.RationalMap.exists_rep
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
obtain :
  ∀ (g : X.PartialMap Y)
    (H : Eq (α := Spec X.functionField ⟶ Y) f.toRationalMap.fromFunctionField g.toRationalMap.fromFunctionField),
    f.toRationalMap = g.toRationalMap
⊢ f.toRationalMap = g

Tactic:
obtain ⟨g, rfl⟩ := g.exists_rep

Premises used: rfl, AlgebraicGeometry.Scheme.RationalMap.exists_rep
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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

Tactic:
PartialMap.toRationalMap_eq_iff.mpr ?_

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsIntegral X
f g : X.PartialMap Y
H : Eq (α := Spec X.functionField ⟶ Y) f.toRationalMap.fromFunctionField g.toRationalMap.fromFunctionField
refine : f.equiv g
⊢ f.toRationalMap = g.toRationalMap

Tactic:
refine PartialMap.toRationalMap_eq_iff.mpr ?_

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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.equiv g

Tactic:
PartialMap.equiv_of_fromSpecStalkOfMem_eq _ _ _ _ H

Premises used: AlgebraicGeometry.Scheme.PartialMap.equiv_of_fromSpecStalkOfMem_eq
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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.equiv g

Tactic:
exact PartialMap.equiv_of_fromSpecStalkOfMem_eq _ _ _ _ H

Premises used: AlgebraicGeometry.Scheme.PartialMap.equiv_of_fromSpecStalkOfMem_eq
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsIntegral X
inst_1 : LocallyOfFiniteType sY
f : { f : Spec X.functionField ⟶ Y // f ≫ sY = X.fromSpecStalk (genericPoint ↥X) ≫ sX }
⊢ PartialMap.hom
      (PartialMap.restrict
        ((fun (x : X.PartialMap Y) ↦ x.compHom sY) (PartialMap.ofFromSpecStalk sX sY (↑f : Spec X.functionField ⟶ Y) ⋯))
        (PartialMap.domain (Y := S)
          ((fun (x : X.PartialMap Y) ↦ x.compHom sY)
            (PartialMap.ofFromSpecStalk sX sY (↑f : Spec X.functionField ⟶ Y) ⋯)))
        ⋯ ⋯) =
    ((Hom.toPartialMap sX).restrict
        (PartialMap.domain (Y := S)
          ((fun (x : X.PartialMap Y) ↦ x.compHom sY)
            (PartialMap.ofFromSpecStalk sX sY (↑f : Spec X.functionField ⟶ Y) ⋯)))
        ⋯ ⋯).hom

Tactic:
simp [PartialMap.ofFromSpecStalk_comp]

Premises used: AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk_comp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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 }
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)
⊢ Eq (α := Spec X.functionField ⟶ S) ((↑f : X ⤏ Y).fromFunctionField ≫ sY) (X.fromSpecStalk (genericPoint ↥X) ≫ sX)

Tactic:
obtain ⟨f, hf⟩ := f
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
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)
⊢ 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, rfl⟩ := f.exists_rep

Premises used: rfl, AlgebraicGeometry.Scheme.RationalMap.exists_rep
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsIntegral X
inst_1 : LocallyOfFiniteType sY
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:
simpa [fromFunctionField_toRationalMap] using congr(RationalMap.fromFunctionField $hf)

Premises used: AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_toRationalMap
-- 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
inst_2 : IsIntegral X
inst_3 : LocallyOfFiniteType (Y ↘ S)
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
⊢ 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

Tactic:
simp only [Hom.isOver_iff]

Premises used: AlgebraicGeometry.Scheme.Hom.isOver_iff
-- 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
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) ↦ f ≫ Y ↘ S = Spec X.functionField ↘ S) fun (f : Spec X.functionField ⟶ Y) ↦
    f ≫ Y ↘ S = X.fromSpecStalk (genericPoint ↥X) ≫ X ↘ S

Tactic:
rfl
-- 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
inst_2 : IsIntegral X
inst_3 : LocallyOfFiniteType (Y ↘ S)
h : ∀ (f : X ⤏ Y), f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) ↔ IsOver S f
⊢ 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

Tactic:
ext f
-- 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
inst_2 : IsIntegral X
inst_3 : LocallyOfFiniteType (Y ↘ S)
f : X ⤏ Y
h h₁ : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) ↔ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) ↔ IsOver S f

Tactic:
rw [RationalMap.isOver_iff]

Premises used: AlgebraicGeometry.Scheme.RationalMap.isOver_iff
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
⊢ f.domain ≤ f.toRationalMap.domain

Tactic:
le_sSup ⟨f, rfl, rfl⟩

Premises used: Set.Mem, Exists.intro, le_sSup, rfl
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X ⤏ Y
x : ↥X
⊢ (∃ (u : TopologicalSpace.Opens ↥X),
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
          {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} u ∧
        x ∈ u) ↔
    ∃ (g : X.PartialMap Y), x ∈ g.domain ∧ g.toRationalMap = f

Tactic:
simp [@and_comm (x ∈ _)]

Premises used: and_comm
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X ⤏ Y
⊢ Dense (↑f.domain : Set ↥X)

Tactic:
f.inductionOn (fun g ↦ g.dense_domain.mono g.le_domain_toRationalMap)

Premises used: Quotient.inductionOn
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
⊢ (∀ (x : ↥(↑f.domain : Scheme)),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := (↑f.domain : Scheme))
          { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
            X := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              X.homOfLE ⋯ }),
        Membership.mem (γ := Set ↥(↑f.domain : Scheme))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
                  X :=
                    fun
                      (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                    (↑(↑U : X.Opens) : Scheme),
                  f :=
                    fun
                      (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                    X.homOfLE ⋯ :
                  PreZeroHypercover (↑f.domain : Scheme) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
                  X :=
                    fun
                      (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                    (↑(↑U : X.Opens) : Scheme),
                  f :=
                    fun
                      (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                    X.homOfLE ⋯ :
                  PreZeroHypercover (↑f.domain : Scheme) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := (↑f.domain : Scheme))
          { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
            X := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              X.homOfLE ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
            X := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              X.homOfLE ⋯ :
            PreZeroHypercover (↑f.domain : Scheme) }
          i)

Tactic:
⟨fun x ↦ ?_, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
x : ↥(↑f.domain : Scheme)
⊢ (↑((PreZeroHypercover.f
            { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
              X :=
                fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                (↑(↑U : X.Opens) : Scheme),
              f :=
                fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
                X.homOfLE ⋯ }
            (Subtype.mk (p := fun (x : X.Opens) ↦
              Membership.mem (γ := Set X.Opens)
                {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} x)
              (⋯.choose (p := fun (u : TopologicalSpace.Opens ↥X) ↦
                Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
                    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} u ∧
                  (↑x : ↥X) ∈ u))
              ⋯))
          (Subtype.mk (p := fun (x_1 : ↥X) ↦
            x_1 ∈
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                    Membership.mem (γ := Set X.Opens)
                      {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} x)
                    (⋯.choose (p := fun (u : TopologicalSpace.Opens ↥X) ↦
                      Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
                          {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} u ∧
                        (↑x : ↥X) ∈ u))
                    ⋯) :
                X.Opens))
            (↑x : ↥X) ⋯)) :
      ↥X) =
    (↑x : ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
x : ↥(↑f.domain : Scheme)
⊢ Membership.mem (γ := Set ↥(↑f.domain : Scheme))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := (↑f.domain : Scheme))
          { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
            X := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              X.homOfLE ⋯ :
            PreZeroHypercover (↑f.domain : Scheme) }
          (Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} x)
            (⋯.choose (p := fun (u : TopologicalSpace.Opens ↥X) ↦
              Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
                  {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} u ∧
                (↑x : ↥X) ∈ u))
            ⋯)))
      ⇑(PreZeroHypercover.f
          { I₀ := (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u),
            X := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑{x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} : Type u)) ↦
              X.homOfLE ⋯ }
          (Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} x)
            (⋯.choose (p := fun (u : TopologicalSpace.Opens ↥X) ↦
              Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
                  {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f), g.domain = x} u ∧
                (↑x : ↥X) ∈ u))
            ⋯)))
    x

Tactic:
exact ⟨⟨x.1, (TopologicalSpace.Opens.mem_sSup.mp x.2).choose_spec.2⟩, Subtype.ext (by simp)⟩