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 : IsSeparated (Y ↘ S)
g : X.PartialMap Y
inst_4 : IsOver S g
Uf : X.Opens
dense_domain : Dense (↑Uf : Set ↥X)
f : (↑Uf : Scheme) ⟶ Y
hfg : { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain = g.domain
inst_5 : IsOver S { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }
obtain :
  ∀ (Ug : X.Opens) (dense_domain_1 : Dense (↑Ug : Set ↥X)) (g : (↑Ug : Scheme) ⟶ Y)
    [IsOver S { domain := Ug, dense_domain := dense_domain_1, hom := g : X.PartialMap Y }]
    (hfg :
      { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain =
        { domain := Ug, dense_domain := dense_domain_1, hom := g : X.PartialMap Y }.domain),
    ({ domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.restrict
            { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom =
        ({ domain := Ug, dense_domain := dense_domain_1, hom := g }.restrict
            { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom ↔
      { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y } =
        { domain := Ug, dense_domain := dense_domain_1, hom := g }
⊢ ({ domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.restrict
          { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom =
      (g.restrict { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y } = g

Tactic:
obtain ⟨Ug, _, g⟩ := g
-- 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 : IsSeparated (Y ↘ S)
Uf : X.Opens
dense_domain : Dense (↑Uf : Set ↥X)
f : (↑Uf : Scheme) ⟶ Y
inst_4 : IsOver S { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }
Ug : X.Opens
dense_domain_1 : Dense (↑Ug : Set ↥X)
g : (↑Ug : Scheme) ⟶ Y
inst_5 : IsOver S { domain := Ug, dense_domain := dense_domain_1, hom := g : X.PartialMap Y }
hfg :
  { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain =
    { domain := Ug, dense_domain := dense_domain_1, hom := g : X.PartialMap Y }.domain
⊢ Uf = Ug

Tactic:
hfg
-- 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 : IsSeparated (Y ↘ S)
Uf : X.Opens
dense_domain : Dense (↑Uf : Set ↥X)
f : (↑Uf : Scheme) ⟶ Y
inst_4 : IsOver S { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }
Ug : X.Opens
dense_domain_1 : Dense (↑Ug : Set ↥X)
g : (↑Ug : Scheme) ⟶ Y
inst_5 : IsOver S { domain := Ug, dense_domain := dense_domain_1, hom := g : X.PartialMap Y }
hfg :
  { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain =
    { domain := Ug, dense_domain := dense_domain_1, hom := g : X.PartialMap Y }.domain
obtain :
  ∀ (dense_domain_2 : Dense (↑Uf : Set ↥X)) (g : (↑Uf : Scheme) ⟶ Y)
    [IsOver S { domain := Uf, dense_domain := dense_domain_2, hom := g : X.PartialMap Y }],
    ({ domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.restrict
            { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom =
        ({ domain := Uf, dense_domain := dense_domain_2, hom := g }.restrict
            { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom ↔
      { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y } =
        { domain := Uf, dense_domain := dense_domain_2, hom := g }
⊢ ({ domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.restrict
          { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom =
      ({ domain := Ug, dense_domain := dense_domain_1, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y } =
      { domain := Ug, dense_domain := dense_domain_1, hom := g }

Tactic:
obtain rfl : Uf = Ug := hfg

Premises used: rfl
-- 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 : IsSeparated (Y ↘ S)
Uf : X.Opens
dense_domain : Dense (↑Uf : Set ↥X)
f : (↑Uf : Scheme) ⟶ Y
inst_4 : IsOver S { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }
dense_domain_1 : Dense (↑Uf : Set ↥X)
g : (↑Uf : Scheme) ⟶ Y
inst_5 : IsOver S { domain := Uf, dense_domain := dense_domain_1, hom := g : X.PartialMap Y }
⊢ ({ domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.restrict
          { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom =
      ({ domain := Uf, dense_domain := dense_domain_1, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y } =
      { domain := Uf, dense_domain := dense_domain_1, hom := g }

Tactic:
simp
-- 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 : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst_4 : IsOver S f
inst_5 : Hom.IsOver g S
rw :
  (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    Iso.hom (X.isoOfEq ⋯) ≫ f.hom = Iso.hom (X.isoOfEq ⋯) ≫ f.domain.ι ≫ g
⊢ f.equiv (Hom.toPartialMap g) ↔ f.hom = f.domain.ι ≫ g

Tactic:
rw [equiv_iff_of_isSeparated (S := S), ← cancel_epi (X.isoOfEq (inf_top_eq f.domain)).hom]

Premises used: inf_top_eq, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, AlgebraicGeometry.Scheme.isoOfEq, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.PartialMap.domain
-- 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 : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst_4 : IsOver S f
inst_5 : Hom.IsOver g S
simp : X.homOfLE ⋯ ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g ↔ Iso.hom (X.isoOfEq ⋯) ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    Iso.hom (X.isoOfEq ⋯) ≫ f.hom = Iso.hom (X.isoOfEq ⋯) ≫ f.domain.ι ≫ g

Tactic:
simp
-- 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 : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst_4 : IsOver S f
inst_5 : Hom.IsOver g S
⊢ X.homOfLE ⋯ ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g ↔ Iso.hom (X.isoOfEq ⋯) ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
⊢ Function.Surjective.{u + 1, u + 1} (α := X.PartialMap Y) toRationalMap

Tactic:
Quotient.exists_rep

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap, Quotient.exists_rep, AlgebraicGeometry.Scheme.RationalMap, Function.Surjective
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X ⤏ Y
⊢ ∃ (g : X.PartialMap Y), g.toRationalMap = f

Tactic:
Quotient.exists_rep f

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap, Quotient.exists_rep, AlgebraicGeometry.Scheme.RationalMap
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f g : X.PartialMap Y
⊢ f.toRationalMap = g.toRationalMap ↔ f.equiv g

Tactic:
Quotient.eq

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap, AlgebraicGeometry.Scheme.RationalMap, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X ⤏ Y
⊢ f.representative.toRationalMap = f

Tactic:
f.exists_rep.choose_spec

Premises used: Exists.choose_spec, AlgebraicGeometry.Scheme.RationalMap.representative, AlgebraicGeometry.Scheme.RationalMap.exists_rep
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
f : X.PartialMap Y
rw : f.toRationalMap.representative.toRationalMap = f.toRationalMap
rw₁ rw₂ : f.toRationalMap = f.toRationalMap
⊢ f.toRationalMap.representative.equiv f

Tactic:
rw [← PartialMap.toRationalMap_eq_iff, f.toRationalMap.toRationalMap_representative]

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap, AlgebraicGeometry.Scheme.RationalMap.toRationalMap_representative, AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff
-- 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
⊢ (f.restrict U hU hU').toRationalMap = f.toRationalMap

Tactic:
toRationalMap_eq_iff.mpr (f.restrict_equiv U hU hU')

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff, AlgebraicGeometry.Scheme.PartialMap.restrict_equiv
-- 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
inst_2 : PartialMap.IsOver S f
⊢ RationalMap.IsOver S f.toRationalMap

Tactic:
⟨f, ‹_›, rfl⟩

Premises used: AlgebraicGeometry.Scheme.RationalMap.IsOver.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
inst_2 : IsOver S f
⊢ ∃ (g : X.PartialMap Y), PartialMap.IsOver S g ∧ g.toRationalMap = f

Tactic:
IsOver.exists_partialMap_over

Premises used: AlgebraicGeometry.Scheme.RationalMap.IsOver.exists_partialMap_over
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
refine :
  ∀ ⦃a b : X.PartialMap Y⦄,
    a ≈ b →
      HasEquiv.Equiv.{u + 1, 0} (α := X.PartialMap Z) ((fun (x : X.PartialMap Y) ↦ x.compHom g) a)
        ((fun (x : X.PartialMap Y) ↦ x.compHom g) b)
⊢ X ⤏ Z

Tactic:
refine Quotient.map (PartialMap.compHom · g) ?_ f

Premises used: AlgebraicGeometry.Scheme.PartialMap.compHom, Quotient.map
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
this :
  ∀ (W : X.Opens) (hW : Dense (↑W : Set ↥X)) (hWl : W ≤ f₁.domain) (hWr : W ≤ f₂.domain)
    (e : (f₁.restrict W hW hWl).hom = (f₂.restrict W hW hWr).hom),
    HasEquiv.Equiv.{u + 1, 0} (α := X.PartialMap Z) ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁)
      ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₂)
⊢ f₁ ≈ f₂ →
    HasEquiv.Equiv.{u + 1, 0} (α := X.PartialMap Z) ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁)
      ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₂)

Tactic:
⟨W, hW, hWl, hWr, e⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f₁.domain
hWr : W ≤ f₂.domain
e : (f₁.restrict W hW hWl).hom = (f₂.restrict W hW hWr).hom
⊢ HasEquiv.Equiv.{u + 1, 0} (α := X.PartialMap Z) ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁)
    ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₂)

Tactic:
⟨W, hW, hWl, hWr, ?_⟩

Premises used: AlgebraicGeometry.Scheme.PartialMap.equiv, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f₁.domain
hWr : W ≤ f₂.domain
e : (f₁.restrict W hW hWl).hom = (f₂.restrict W hW hWr).hom
refine :
  Eq (α := (↑(PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁) W hW hWl).domain : Scheme) ⟶ Z)
    ((PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁) W hW hWl).hom :
      (↑(PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁) W hW hWl).domain : Scheme) ⟶ Z)
    ((PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₂) W hW hWr).hom :
      (↑(PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₂) W hW hWr).domain : Scheme) ⟶ Z)
⊢ HasEquiv.Equiv.{u + 1, 0} (α := X.PartialMap Z) ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁)
    ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₂)

Tactic:
refine ⟨W, hW, hWl, hWr, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f₁.domain
hWr : W ≤ f₂.domain
e : (f₁.restrict W hW hWl).hom = (f₂.restrict W hW hWr).hom
simp : X.homOfLE hWl ≫ f₁.hom ≫ g = X.homOfLE hWr ≫ f₂.hom ≫ g
⊢ Eq (α := (↑(PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁) W hW hWl).domain : Scheme) ⟶ Z)
    ((PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁) W hW hWl).hom :
      (↑(PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₁) W hW hWl).domain : Scheme) ⟶ Z)
    ((PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₂) W hW hWr).hom :
      (↑(PartialMap.restrict ((fun (x : X.PartialMap Y) ↦ x.compHom g) f₂) W hW hWr).domain : Scheme) ⟶ Z)

Tactic:
simp only [PartialMap.restrict_domain, PartialMap.restrict_hom, PartialMap.compHom_domain,
    PartialMap.compHom_hom] at e ⊢

Premises used: AlgebraicGeometry.Scheme.PartialMap.compHom_domain, AlgebraicGeometry.Scheme.PartialMap.restrict_hom, AlgebraicGeometry.Scheme.PartialMap.compHom_hom, AlgebraicGeometry.Scheme.PartialMap.restrict_domain
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f₁.domain
hWr : W ≤ f₂.domain
e : X.homOfLE hWl ≫ f₁.hom = X.homOfLE hWr ≫ f₂.hom
rw rw₁ : X.homOfLE hWr ≫ f₂.hom ≫ g = X.homOfLE hWr ≫ f₂.hom ≫ g
⊢ X.homOfLE hWl ≫ f₁.hom ≫ g = X.homOfLE hWr ≫ f₂.hom ≫ g

Tactic:
rw [reassoc_of% e]
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z : Scheme
f : X.PartialMap Y
g : Y ⟶ Z
⊢ (f.compHom g).toRationalMap = f.toRationalMap.compHom g

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap, Quotient.map, AlgebraicGeometry.Scheme.RationalMap.compHom, Quot.map, 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 : Z.Over S
f : X ⤏ Y
g : Y ⟶ Z
inst_3 : RationalMap.IsOver S f
inst_4 : Hom.IsOver g S
obtain :
  ∀ (f : X.PartialMap Y) (hf : PartialMap.IsOver S f) [RationalMap.IsOver S f.toRationalMap],
    ∃ (g_1 : X.PartialMap Z), PartialMap.IsOver S g_1 ∧ g_1.toRationalMap = f.toRationalMap.compHom g
⊢ ∃ (g_1 : X.PartialMap Z), PartialMap.IsOver S g_1 ∧ g_1.toRationalMap = f.compHom g

Tactic:
obtain ⟨f, hf, rfl⟩ := f.exists_partialMap_over S

Premises used: AlgebraicGeometry.Scheme.RationalMap.exists_partialMap_over, 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 : Z.Over S
g : Y ⟶ Z
inst_3 : Hom.IsOver g S
f : X.PartialMap Y
hf : PartialMap.IsOver S f
inst_4 : RationalMap.IsOver S f.toRationalMap
⊢ ∃ (g_1 : X.PartialMap Z), PartialMap.IsOver S g_1 ∧ g_1.toRationalMap = f.toRationalMap.compHom g

Tactic:
⟨f.compHom g, inferInstance, rfl⟩

Premises used: AlgebraicGeometry.Scheme.PartialMap.compHom, inferInstance, And.intro, Exists.intro, 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 : Z.Over S
g : Y ⟶ Z
inst_3 : Hom.IsOver g S
f : X.PartialMap Y
hf : PartialMap.IsOver S f
inst_4 : RationalMap.IsOver S f.toRationalMap
⊢ ∃ (g_1 : X.PartialMap Z), PartialMap.IsOver S g_1 ∧ g_1.toRationalMap = f.toRationalMap.compHom g

Tactic:
exact ⟨f.compHom g, inferInstance, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
inst_2 : RationalMap.IsOver S f.toRationalMap
obtain :
  ∀ (f' : X.PartialMap Y) (hf₁ : IsOver S f') (hf₂ : f'.toRationalMap = f.toRationalMap),
    ∃ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')
⊢ ∃ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')

Tactic:
obtain ⟨f', hf₁, hf₂⟩ := RationalMap.IsOver.exists_partialMap_over (S := S) (f := f.toRationalMap)

Premises used: AlgebraicGeometry.Scheme.RationalMap.IsOver.exists_partialMap_over
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
inst_2 : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
obtain :
  ∀ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hUl : U ≤ f'.domain) (hUr : U ≤ f.domain)
    (e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom),
    ∃ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')
⊢ ∃ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')

Tactic:
obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp hf₂

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
inst_2 : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
U : X.Opens
hU : Dense (↑U : Set ↥X)
hUl : U ≤ f'.domain
hUr : U ≤ f.domain
e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom
rw : Hom.IsOver (f'.restrict U hU hUl).hom S
⊢ IsOver S (f.restrict U hU hUr)

Tactic:
rw [IsOver, ← e]

Premises used: AlgebraicGeometry.Scheme.PartialMap.IsOver
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
inst_2 : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
U : X.Opens
hU : Dense (↑U : Set ↥X)
hUl : U ≤ f'.domain
hUr : U ≤ f.domain
e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom
⊢ Hom.IsOver (f'.restrict U hU hUl).hom S

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
inst_2 : RationalMap.IsOver S f.toRationalMap
f' : X.PartialMap Y
hf₁ : IsOver S f'
hf₂ : f'.toRationalMap = f.toRationalMap
U : X.Opens
hU : Dense (↑U : Set ↥X)
hUl : U ≤ f'.domain
hUr : U ≤ f.domain
e : (f'.restrict U hU hUl).hom = (f.restrict U hU hUr).hom
⊢ ∃ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')

Tactic:
exact ⟨U, hU, hUr, by rw [IsOver, ← e]; infer_instance⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
mp : IsOver S f → f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
mpr : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) → IsOver S f
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
h : IsOver S f
mp :
  ∀ (g : X.PartialMap Y) (hg : PartialMap.IsOver S g) (e : g.toRationalMap = f),
    f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
obtain ⟨g, hg, e⟩ := f.exists_partialMap_over S

Premises used: AlgebraicGeometry.Scheme.RationalMap.exists_partialMap_over
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
h : IsOver S f
g : X.PartialMap Y
hg : PartialMap.IsOver S g
e : g.toRationalMap = f
mp : g.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
mp₁ : g.toRationalMap.compHom (Y ↘ S) = (Hom.toPartialMap (X ↘ S)).toRationalMap
mp₂ : (g.compHom (Y ↘ S)).toRationalMap = (Hom.toPartialMap (X ↘ S)).toRationalMap
mp₃ : ((Hom.toPartialMap (X ↘ S)).restrict g.domain ⋯ ⋯).toRationalMap = (Hom.toPartialMap (X ↘ S)).toRationalMap
mp₄ mp₅ : (Hom.toPartialMap (X ↘ S)).toRationalMap = (Hom.toPartialMap (X ↘ S)).toRationalMap
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]

Premises used: AlgebraicGeometry.Scheme.PartialMap.isOver_iff_eq_restrict, AlgebraicGeometry.Scheme.RationalMap.compHom_toRationalMap, Iff.mp, AlgebraicGeometry.Scheme.PartialMap.restrict_toRationalMap, AlgebraicGeometry.Scheme.Hom.toRationalMap
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
e : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
mpr : ∀ (f : X.PartialMap Y) (e : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)), IsOver S f.toRationalMap
⊢ IsOver S f

Tactic:
obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
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
⊢ IsOver S f.toRationalMap

Tactic:
obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp e

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
e_1 : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
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
⊢ PartialMap.IsOver S (f.restrict U hU hUl)

Tactic:
simpa using e
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
e_1 : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
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
⊢ (f.restrict U hU hUl).toRationalMap = f.toRationalMap

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
e_1 : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
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:
exact ⟨⟨f.restrict U hU hUl, by simpa using e, by simp⟩⟩