awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
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 ⋯) ≫
                (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)
⊢ X.PartialMap 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) ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)) ⋯
⊢ ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f

Tactic:
have hg₁ (x) : (g x).toRationalMap = f := x.2.choose_spec.1
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
⊢ ∀ (x : f.openCoverDomain.I₀), (g x).domain = (↑x : X.Opens)

Tactic:
have hg₂ (x) : (g x).domain = x.1 := x.2.choose_spec.2
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)

Tactic:
(cancel_epi (isPullback_opens_inf_le (le_sSup x.2) (le_sSup y.2)).isoPullback.hom).mp ?_

Premises used: AlgebraicGeometry.Scheme.homOfLE, AlgebraicGeometry.Scheme.RationalMap.domain, AlgebraicGeometry.IsOpenImmersion.lift, AlgebraicGeometry.Scheme.restrict, CategoryTheory.IsPullback.isoPullback, Iff.mp, le_sSup, AlgebraicGeometry.isPullback_opens_inf_le, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.Opens.toScheme, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
refine :
  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))
⊢ 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)

Tactic:
refine (cancel_epi (isPullback_opens_inf_le (le_sSup x.2) (le_sSup y.2)).isoPullback.hom).mp ?_

Premises used: CategoryTheory.IsPullback.isoPullback, Iff.mp, le_sSup, AlgebraicGeometry.isPullback_opens_inf_le, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
simp :
  Eq (α := (↑((↑x : X.Opens) ⊓ (↑y : X.Opens)) : Scheme) ⟶ Y)
    (X.homOfLE ⋯ ≫
      Iso.inv (X.isoOfEq ⋯) ≫
        (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯).hom)
    (X.homOfLE ⋯ ≫
      Iso.inv (X.isoOfEq ⋯) ≫
        (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑y : X.Opens)) ⋯).hom)
⊢ 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))

Tactic:
simp only [openCoverDomain, IsPullback.isoPullback_hom_fst_assoc,
    IsPullback.isoPullback_hom_snd_assoc]

Premises used: AlgebraicGeometry.Scheme.RationalMap.openCoverDomain, CategoryTheory.IsPullback.isoPullback_hom_snd_assoc, CategoryTheory.IsPullback.isoPullback_hom_fst_assoc
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
change :
  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)
⊢ Eq (α := (↑((↑x : X.Opens) ⊓ (↑y : X.Opens)) : Scheme) ⟶ Y)
    (X.homOfLE ⋯ ≫
      Iso.inv (X.isoOfEq ⋯) ≫
        (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑x : X.Opens)) ⋯).hom)
    (X.homOfLE ⋯ ≫
      Iso.inv (X.isoOfEq ⋯) ≫
        (Exists.choose (p := fun (g : X.PartialMap Y) ↦ ∃ (_ : g.toRationalMap = f), g.domain = (↑y : X.Opens)) ⋯).hom)

Tactic:
change _ ≫ _ ≫ (g x).hom = _ ≫ _ ≫ (g y).hom

Premises used: AlgebraicGeometry.Scheme.PartialMap.hom
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
simp_rw :
  ((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
⊢ 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)

Tactic:
simp_rw [← cancel_epi (X.isoOfEq congr($(hg₂ x) ⊓ $(hg₂ y))).hom, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, congrArg, id, AlgebraicGeometry.Scheme.isoOfEq, congr, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, Min.min
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
⊢ ((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom = ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

Tactic:
(PartialMap.equiv_iff_of_isSeparated (S := ⊤_ _) (f := g x) (g := g y)).mp ?_

Premises used: AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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
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 y).hom =
      ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom
convert! : (g x).equiv (g y)
⊢ ((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

Tactic:
convert! (PartialMap.equiv_iff_of_isSeparated (S := ⊤_ _) (f := g x) (g := g y)).mp ?_ using 1

Premises used: AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
e_1 :
  ((↑((g x).domain ⊓ (g y).domain) : Scheme) ⟶ Y) =
    ((↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain : Scheme) ⟶ Y)
h : ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g x).hom = X.homOfLE ⋯ ≫ (g x).hom
⊢ ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g x).hom =
    ((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
e_1 :
  ((↑((g x).domain ⊓ (g y).domain) : Scheme) ⟶ Y) =
    ((↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain : Scheme) ⟶ Y)
h : (Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯) = X.homOfLE ⋯
⊢ ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g x).hom = X.homOfLE ⋯ ≫ (g x).hom

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
e_1 :
  ((↑((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 ⋯) = X.homOfLE ⋯

Tactic:
simp [g, ← cancel_mono (Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
e_1 :
  ((↑((g x).domain ⊓ (g y).domain) : Scheme) ⟶ Y) =
    ((↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain : Scheme) ⟶ Y)
h : ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g y).hom = X.homOfLE ⋯ ≫ (g y).hom
⊢ ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
e_1 :
  ((↑((g x).domain ⊓ (g y).domain) : Scheme) ⟶ Y) =
    ((↑((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).domain : Scheme) ⟶ Y)
h : (Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯) = X.homOfLE ⋯
⊢ ((Iso.hom (X.isoOfEq ⋯) ≫ X.homOfLE ⋯) ≫ Iso.inv (X.isoOfEq ⋯)) ≫ (g y).hom = X.homOfLE ⋯ ≫ (g y).hom

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
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)
rw : (g x).toRationalMap = (g y).toRationalMap
rw₁ : f = (g y).toRationalMap
rw₂ rw₃ : f = f
⊢ (g x).equiv (g y)

Tactic:
rw [← PartialMap.toRationalMap_eq_iff, hg₁, hg₁]

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
dsimp :
  X.homOfLE ⋯ ≫
      Cover.glueMorphisms f.toRationalMap.openCoverDomain
        (fun (x : f.toRationalMap.openCoverDomain.I₀) ↦
          (X.isoOfEq ⋯).inv ≫
            (Exists.choose (p := fun (g : X.PartialMap Y) ↦
                ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = (↑x : X.Opens)) ⋯).hom)
        ⋯ =
    f.hom
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).hom = f.hom

Tactic:
dsimp [RationalMap.toPartialMap]

Premises used: AlgebraicGeometry.Scheme.RationalMap.toPartialMap
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
⊢ X.homOfLE ⋯ ≫
      Cover.glueMorphisms f.toRationalMap.openCoverDomain
        (fun (x : f.toRationalMap.openCoverDomain.I₀) ↦
          (X.isoOfEq ⋯).inv ≫
            (Exists.choose (p := fun (g : X.PartialMap Y) ↦
                ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = (↑x : X.Opens)) ⋯).hom)
        ⋯ =
    f.hom

Tactic:
(f.toRationalMap.openCoverDomain.ι_glueMorphisms _ _ ⟨_, f, rfl, rfl⟩).trans ?_

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap, Set.Mem, Subtype.mk, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, AlgebraicGeometry.Scheme.RationalMap.openCoverDomain, Exists.intro, AlgebraicGeometry.Scheme.Opens.toScheme, rfl, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
refine :
  Iso.inv (X.isoOfEq ⋯) ≫
      (Exists.choose (p := fun (g : X.PartialMap Y) ↦
          ∃ (_ : g.toRationalMap = f.toRationalMap),
            g.domain =
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                    Membership.mem (γ := Set X.Opens)
                      {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                    f.domain ⋯) :
                X.Opens))
          ⋯).hom =
    f.hom
⊢ X.homOfLE ⋯ ≫
      Cover.glueMorphisms f.toRationalMap.openCoverDomain
        (fun (x : f.toRationalMap.openCoverDomain.I₀) ↦
          (X.isoOfEq ⋯).inv ≫
            (Exists.choose (p := fun (g : X.PartialMap Y) ↦
                ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = (↑x : X.Opens)) ⋯).hom)
        ⋯ =
    f.hom

Tactic:
refine (f.toRationalMap.openCoverDomain.ι_glueMorphisms _ _ ⟨_, f, rfl, rfl⟩).trans ?_

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap, Subtype.mk, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, AlgebraicGeometry.Scheme.RationalMap.openCoverDomain, Exists.intro, rfl, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
⊢ Membership.mem (γ := Set X.Opens)
    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} f.domain

Tactic:
generalize_proofs _ _ H _
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
pf :
  Membership.mem (γ := Set X.Opens)
    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} f.domain
⊢ ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain

Tactic:
generalize_proofs _ _ H _
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
pf :
  Membership.mem (γ := Set X.Opens)
    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} f.domain
pf₁ : ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
⊢ ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap),
    g.domain =
      (↑(Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
            f.domain pf₁) :
        X.Opens)

Tactic:
generalize_proofs _ _ H _
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
pf :
  Membership.mem (γ := Set X.Opens)
    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} f.domain
pf₁ : ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
H :
  ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap),
    g.domain =
      (↑(Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
            f.domain pf₁) :
        X.Opens)
⊢ H.choose (p := fun (g : X.PartialMap Y) ↦
        ∃ (_ : g.toRationalMap = f.toRationalMap),
          g.domain =
            (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                  Membership.mem (γ := Set X.Opens)
                    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                  f.domain pf₁) :
              X.Opens)).domain =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦
          Membership.mem (γ := Set X.Opens)
            {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
          f.domain pf) :
      X.Opens)

Tactic:
generalize_proofs _ _ H _