awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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').restrict U hU ⋯).hom = (f.restrict U hU hU').hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
⊢ Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))

Tactic:
have hdense : Dense ((f.domain ⊓ g.domain) : Set X) :=
    f.dense_domain.inter_of_isOpen_left g.dense_domain f.domain.2
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
⊢ IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)

Tactic:
have := (isGermInjectiveAt_iff_of_isOpenImmersion (f := (f.domain ⊓ g.domain).ι)
    (x := ⟨x, hxf, hxg⟩)).mp ‹_›
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
refine_2 :
  ∀
    (this :
      ∃ (U : (↑(f.domain ⊓ g.domain) : Scheme).Opens),
        Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U ∧
          U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom),
    f.equiv g
refine_1 :
  Eq (α :=
    Spec
        ((↑(f.domain ⊓ g.domain) : Scheme).presheaf.stalk
          (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)) ⟶
      Y)
    ((↑(f.domain ⊓ g.domain) : Scheme).fromSpecStalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯) ≫
      X.homOfLE ⋯ ≫ f.hom)
    ((↑(f.domain ⊓ g.domain) : Scheme).fromSpecStalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯) ≫
      X.homOfLE ⋯ ≫ g.hom)
⊢ f.equiv g

Tactic:
have := spread_out_unique_of_isGermInjective' (X := (f.domain ⊓ g.domain).toScheme)
    (X.homOfLE inf_le_left ≫ f.hom) (X.homOfLE inf_le_right ≫ g.hom) (x := ⟨x, hxf, hxg⟩) ?_
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this_1 :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
this :
  ∃ (U : (↑(f.domain ⊓ g.domain) : Scheme).Opens),
    Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U ∧
      U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
refine_2 :
  ∀ (U : (↑(f.domain ⊓ g.domain) : Scheme).Opens)
    (hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U)
    (e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom), f.equiv g
⊢ f.equiv g

Tactic:
obtain ⟨U, hxU, e⟩ := this
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ f.equiv g

Tactic:
⟨(f.domain ⊓ g.domain).ι ''ᵁ U, ((f.domain ⊓ g.domain).ι ''ᵁ U).2.dense
      ⟨_, ⟨_, hxU, rfl⟩⟩,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, LE.le.trans_eq, AlgebraicGeometry.Scheme.PartialMap.equiv, inf_le_right, Set.image_subset_range, Subtype.range_val, IsOpen.dense, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.is_open', inf_le_left, LE.le.trans, CategoryTheory.Functor.obj, Min.min, rfl, AlgebraicGeometry.Scheme.PartialMap.domain
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
refine_2 : (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom = (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom
⊢ f.equiv g

Tactic:
refine ⟨(f.domain ⊓ g.domain).ι ''ᵁ U, ((f.domain ⊓ g.domain).ι ''ᵁ U).2.dense
      ⟨_, ⟨_, hxU, rfl⟩⟩,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
refine_2 :
  Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U) ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom =
    Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U) ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom
⊢ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom = (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom

Tactic:
rw [← cancel_epi (Scheme.Hom.isoImage _ _).hom]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.Hom.isoImage
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
refine_2 :
  ∀ (e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom),
    CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
          (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
        f.hom =
      CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
          (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
        g.hom
⊢ Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U) ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom =
    Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U) ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom

Tactic:
simp only [restrict_hom, ← Category.assoc] at e ⊢

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.PartialMap.restrict_hom
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom

Tactic:
e
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
h :
  CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
      (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) =
    U.ι ≫ X.homOfLE ⋯
h₁ :
  CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
      (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) =
    U.ι ≫ X.homOfLE ⋯
⊢ CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      f.hom =
    CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      g.hom

Tactic:
convert! e using 2
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
h :
  CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      f.domain.ι =
    (U.ι ≫ X.homOfLE ⋯) ≫ f.domain.ι
⊢ CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
      (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) =
    U.ι ≫ X.homOfLE ⋯

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
h :
  CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      g.domain.ι =
    (U.ι ≫ X.homOfLE ⋯) ≫ g.domain.ι
⊢ CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
      (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) =
    U.ι ≫ X.homOfLE ⋯

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      f.domain.ι =
    (U.ι ≫ X.homOfLE ⋯) ≫ f.domain.ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
U : (↑(f.domain ⊓ g.domain) : Scheme).Opens
hxU : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
        (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE ⋯) ≫
      g.domain.ι =
    (U.ι ≫ X.homOfLE ⋯) ≫ g.domain.ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
⊢ (f.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯ =
    (g.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯

Tactic:
rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,
      ← g.fromSpecStalkOfMem_restrict hdense inf_le_right ⟨hxf, hxg⟩] at H

Premises used: inf_le_right, And.intro, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_restrict, inf_le_left
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
H₁ :
  (f.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯ =
    (g.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯
⊢ IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)

Tactic:
rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,
      ← g.fromSpecStalkOfMem_restrict hdense inf_le_right ⟨hxf, hxg⟩] at H

Premises used: inf_le_right, And.intro, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_restrict, inf_le_left
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IrreducibleSpace.{u} ↥X
x : ↥X
inst_1 : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
hdense : Dense ((↑f.domain : Set ↥X) ⊓ (↑g.domain : Set ↥X))
H :
  (f.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯ =
    (g.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯
this :
  IsGermInjectiveAt.{u} (↑(f.domain ⊓ g.domain) : Scheme) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)
⊢ Eq (α :=
    Spec
        ((↑(f.domain ⊓ g.domain) : Scheme).presheaf.stalk
          (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯)) ⟶
      Y)
    ((↑(f.domain ⊓ g.domain) : Scheme).fromSpecStalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯) ≫
      X.homOfLE ⋯ ≫ f.hom)
    ((↑(f.domain ⊓ g.domain) : Scheme).fromSpecStalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ f.domain ⊓ g.domain) x ⋯) ≫
      X.homOfLE ⋯ ≫ g.hom)

Tactic:
simpa only [fromSpecStalkOfMem, restrict_domain, Opens.fromSpecStalkOfMem, Spec.map_inv,
      restrict_hom, Category.assoc, IsIso.eq_inv_comp, IsIso.hom_inv_id_assoc] using H

Premises used: AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.IsIso.hom_inv_id_assoc, AlgebraicGeometry.Scheme.PartialMap.restrict_hom, AlgebraicGeometry.Spec.map_inv, AlgebraicGeometry.Scheme.PartialMap.restrict_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 g : X.PartialMap Y
inst_4 : IsOver S f
inst_5 : IsOver S g
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f.domain
hWr : W ≤ g.domain
⊢ f.equiv g ↔ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Tactic:
⟨fun ⟨V, hV, hVl, hVr, e⟩ ↦ ?_, fun e ↦ ⟨_, _, _, _, e⟩⟩

Premises used: AlgebraicGeometry.Scheme.PartialMap.hom, Iff.intro, Exists.intro, AlgebraicGeometry.Scheme.PartialMap.restrict, Eq, _private.0.AlgebraicGeometry.Scheme.PartialMap.equivalence_rel.match_1
-- 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 g : X.PartialMap Y
inst_4 : IsOver S f
inst_5 : IsOver S g
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f.domain
hWr : W ≤ g.domain
refine :
  f.equiv g →
    ∀ (V : X.Opens) (hV : Dense (↑V : Set ↥X)) (hVl : V ≤ f.domain) (hVr : V ≤ g.domain)
      (e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom), (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ f.equiv g ↔ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Tactic:
refine ⟨fun ⟨V, hV, hVl, hVr, e⟩ ↦ ?_, fun e ↦ ⟨_, _, _, _, e⟩⟩
-- 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 g : X.PartialMap Y
inst_4 : IsOver S f
inst_5 : IsOver S g
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f.domain
hWr : W ≤ g.domain
h : f.equiv g
V : X.Opens
hV : Dense (↑V : Set ↥X)
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
⊢ IsDominant (X := (↑(W ⊓ V) : Scheme)) (X.homOfLE ⋯)

Tactic:
have : IsDominant (X.homOfLE (inf_le_left : W ⊓ V ≤ W)) :=
    Opens.isDominant_homOfLE (hW.inter_of_isOpen_left hV W.2) _
-- 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 g : X.PartialMap Y
inst_4 : IsOver S f
inst_5 : IsOver S g
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f.domain
hWr : W ≤ g.domain
h : f.equiv g
V : X.Opens
hV : Dense (↑V : Set ↥X)
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X := (↑(W ⊓ V) : Scheme)) (X.homOfLE ⋯)
apply :
  Eq (α := (↑(W ⊓ V) : Scheme) ⟶ Y) (X.homOfLE ⋯ ≫ (f.restrict W hW hWl).hom) (X.homOfLE ⋯ ≫ (g.restrict W hW hWr).hom)
⊢ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Tactic:
apply ext_of_isDominant_of_isSeparated' S (X.homOfLE (inf_le_left : W ⊓ V ≤ W))

Premises used: AlgebraicGeometry.Scheme.homOfLE, AlgebraicGeometry.ext_of_isDominant_of_isSeparated', inf_le_left
-- 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 g : X.PartialMap Y
inst_4 : IsOver S f
inst_5 : IsOver S g
W : X.Opens
hW : Dense (↑W : Set ↥X)
hWl : W ≤ f.domain
hWr : W ≤ g.domain
h : f.equiv g
V : X.Opens
hV : Dense (↑V : Set ↥X)
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X := (↑(W ⊓ V) : Scheme)) (X.homOfLE ⋯)
⊢ Eq (α := (↑(W ⊓ V) : Scheme) ⟶ Y) (X.homOfLE ⋯ ≫ (f.restrict W hW hWl).hom) (X.homOfLE ⋯ ≫ (g.restrict W hW hWr).hom)

Tactic:
simpa using congr(X.homOfLE (inf_le_right : W ⊓ V ≤ V) ≫ $e)

Premises used: AlgebraicGeometry.Scheme.homOfLE, inf_le_right
-- 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 g : X.PartialMap Y
inst_4 : IsOver S f
inst_5 : IsOver S g
⊢ f.equiv g ↔ (f.restrict (f.domain ⊓ g.domain) ⋯ ⋯).hom = (g.restrict (f.domain ⊓ g.domain) ⋯ ⋯).hom

Tactic:
equiv_iff_of_isSeparated_of_le (S := S) _ _ _

Premises used: AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_le
-- 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 g : X.PartialMap Y
hfg : f.domain = g.domain
inst_4 : IsOver S f
inst_5 : IsOver S g
rw : (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g
⊢ f.equiv g ↔ f = g

Tactic:
rw [equiv_iff_of_isSeparated_of_le (S := S) f.dense_domain le_rfl hfg.le]

Premises used: le_rfl, Eq.le, AlgebraicGeometry.Scheme.PartialMap.dense_domain, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_le
-- 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 g : X.PartialMap Y
hfg : f.domain = g.domain
inst_4 : IsOver S f
inst_5 : IsOver S g
obtain :
  ∀ (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)
    [IsOver S { domain := Uf, dense_domain := dense_domain, hom := f : 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 =
        (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
⊢ (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g

Tactic:
obtain ⟨Uf, _, f⟩ := f