awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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 ⋯) =
    U.ι ≫ X.homOfLE ⋯
have h : CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
      (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE sorry) ≫
    f.domain.ι =
  (U.ι ≫ X.homOfLE sorry) ≫ f.domain.ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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 ⋯) =
    U.ι ≫ X.homOfLE ⋯
have h : CategoryStruct.comp (Y := (↑((f.domain ⊓ g.domain).ι ''ᵁ U) : Scheme))
      (Iso.hom (Hom.isoImage (f.domain ⊓ g.domain).ι U)) (X.homOfLE sorry) ≫
    g.domain.ι =
  (U.ι ≫ X.homOfLE sorry) ≫ g.domain.ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
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 ⋯)
⊢ 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)
have H₁ : (f.restrict (f.domain ⊓ g.domain) hdense sorry).fromSpecStalkOfMem sorry =
  (g.restrict (f.domain ⊓ g.domain) hdense sorry).fromSpecStalkOfMem sorry
Tactic: rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,
      ← g.fromSpecStalkOfMem_restrict hdense inf_le_right ⟨hxf, hxg⟩] at H
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : 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
have 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
Tactic: refine ⟨fun ⟨V, hV, hVl, hVr, e⟩ ↦ ?_, fun e ↦ ⟨_, _, _, _, e⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : 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
⊢ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
have this : IsDominant (X := (↑(W ⊓ V) : Scheme)) (X.homOfLE sorry)
Tactic: have : IsDominant (X.homOfLE (inf_le_left : W ⊓ V ≤ W)) :=
    Opens.isDominant_homOfLE (hW.inter_of_isOpen_left hV W.2) _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : 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 ⋯)
⊢ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
have apply : Eq (α := (↑(W ⊓ V) : Scheme) ⟶ Y) (X.homOfLE sorry ≫ (f.restrict W hW hWl).hom) (X.homOfLE sorry ≫ (g.restrict W hW hWr).hom)
Tactic: apply ext_of_isDominant_of_isSeparated' S (X.homOfLE (inf_le_left : W ⊓ V ≤ W))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
hfg : f.domain = g.domain
inst_4 : IsOver S f
inst_5 : IsOver S g
⊢ f.equiv g ↔ f = g
have rw : (f.restrict f.domain sorry sorry).hom = (g.restrict f.domain sorry sorry).hom ↔ f = g
Tactic: rw [equiv_iff_of_isSeparated_of_le (S := S) f.dense_domain le_rfl hfg.le]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
hfg : f.domain = g.domain
inst_4 : IsOver S f
inst_5 : IsOver S g
⊢ (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g
have 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 sorry sorry).hom =
      (g.restrict { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain sorry sorry).hom ↔
    { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y } = g
Tactic: obtain ⟨Uf, _, f⟩ := f
Cleared hypotheses: f, hfg, inst_4
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : 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 }
⊢ ({ 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
have 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 sorry sorry).hom =
      ({ domain := Ug, dense_domain := dense_domain_1, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain sorry sorry).hom ↔
    { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y } =
      { domain := Ug, dense_domain := dense_domain_1, hom := g }
Tactic: obtain ⟨Ug, _, g⟩ := g
Cleared hypotheses: g, inst_4, hfg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : 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
⊢ ({ 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 }
have 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 sorry sorry).hom =
      ({ domain := Uf, dense_domain := dense_domain_2, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y }.domain sorry sorry).hom ↔
    { domain := Uf, dense_domain := dense_domain, hom := f : X.PartialMap Y } =
      { domain := Uf, dense_domain := dense_domain_2, hom := g }
Tactic: obtain rfl : Uf = Ug := hfg
Cleared hypotheses: Ug, dense_domain_1, g, inst_5, hfg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst_4 : IsOver S f
inst_5 : Hom.IsOver g S
⊢ f.equiv (Hom.toPartialMap g) ↔ f.hom = f.domain.ι ≫ g
have rw : (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) sorry sorry).hom =
    ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) sorry sorry).hom ↔
  Iso.hom (X.isoOfEq sorry) ≫ f.hom = Iso.hom (X.isoOfEq sorry) ≫ f.domain.ι ≫ g
Tactic: rw [equiv_iff_of_isSeparated (S := S), ← cancel_epi (X.isoOfEq (inf_top_eq f.domain)).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
inst_2 : IsReduced X
inst_3 : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst_4 : IsOver S f
inst_5 : Hom.IsOver g S
⊢ (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
have simp : X.homOfLE sorry ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g ↔ Iso.hom (X.isoOfEq sorry) ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
f : X.PartialMap Y
⊢ f.toRationalMap.representative.equiv f
have rw : f.toRationalMap.representative.toRationalMap = f.toRationalMap
Tactic: rw [← PartialMap.toRationalMap_eq_iff, f.toRationalMap.toRationalMap_representative]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
f : X.PartialMap Y
rw : f.toRationalMap.representative.toRationalMap = f.toRationalMap
⊢ f.toRationalMap.representative.equiv f
have rw₁ : f.toRationalMap = f.toRationalMap
Tactic: rw [← PartialMap.toRationalMap_eq_iff, f.toRationalMap.toRationalMap_representative]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
⊢ X ⤏ Z
have 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)
Tactic: refine Quotient.map (PartialMap.compHom · g) ?_ f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
g : Y ⟶ Z
f₁ f₂ : X.PartialMap Y
⊢ 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₂)
have 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₂)
Tactic: ⟨W, hW, hWl, hWr, e⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
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₂)
have 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)
Tactic: refine ⟨W, hW, hWl, hWr, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ 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)
have simp : X.homOfLE hWl ≫ f₁.hom ≫ g = X.homOfLE hWr ≫ f₂.hom ≫ g
Tactic: simp only [PartialMap.restrict_domain, PartialMap.restrict_hom, PartialMap.compHom_domain,
    PartialMap.compHom_hom] at e ⊢
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ X.homOfLE hWl ≫ f₁.hom ≫ g = X.homOfLE hWr ≫ f₂.hom ≫ g
have rw : X.homOfLE hWr ≫ f₂.hom ≫ g = X.homOfLE hWr ≫ f₂.hom ≫ g
Tactic: rw [reassoc_of% e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : X.Over S
inst_1 : Y.Over S
inst_2 : Z.Over S
f : X ⤏ Y
g : Y ⟶ Z
inst_3 : RationalMap.IsOver S f
inst_4 : Hom.IsOver g S
⊢ ∃ (g_1 : X.PartialMap Z), PartialMap.IsOver S g_1 ∧ g_1.toRationalMap = f.compHom g
have 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
Tactic: obtain ⟨f, hf, rfl⟩ := f.exists_partialMap_over S
Cleared hypotheses: f, inst_3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
inst_2 : RationalMap.IsOver S f.toRationalMap
⊢ ∃ (U : X.Opens) (hU : Dense (↑U : Set ↥X)) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')
have 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')
Tactic: obtain ⟨f', hf₁, hf₂⟩ := RationalMap.IsOver.exists_partialMap_over (S := S) (f := f.toRationalMap)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
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)) (hU' : U ≤ f.domain), IsOver S (f.restrict U hU hU')
have 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')
Tactic: obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp hf₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X.PartialMap Y
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
⊢ IsOver S (f.restrict U hU hUr)
have rw : Hom.IsOver (f'.restrict U hU hUl).hom S
Tactic: rw [IsOver, ← e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
have mp : IsOver S f → f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
mp : IsOver S f → f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
have mpr : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) → IsOver S f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
h : IsOver S f
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
have mp : ∀ (g : X.PartialMap Y) (hg : PartialMap.IsOver S g) (e : g.toRationalMap = f),
  f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
Tactic: obtain ⟨g, hg, e⟩ := f.exists_partialMap_over S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
h : IsOver S f
g : X.PartialMap Y
hg : PartialMap.IsOver S g
e : g.toRationalMap = f
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
have mp : g.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
Tactic: rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ 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)
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
have mp₁ : g.toRationalMap.compHom (Y ↘ S) = (Hom.toPartialMap (X ↘ S)).toRationalMap
Tactic: rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ 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
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
have mp₂ : (g.compHom (Y ↘ S)).toRationalMap = (Hom.toPartialMap (X ↘ S)).toRationalMap
Tactic: rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ 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
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
have mp₃ : ((Hom.toPartialMap (X ↘ S)).restrict g.domain sorry sorry).toRationalMap = (Hom.toPartialMap (X ↘ S)).toRationalMap
Tactic: rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ 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
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
have mp₄ : (Hom.toPartialMap (X ↘ S)).toRationalMap = (Hom.toPartialMap (X ↘ S)).toRationalMap
Tactic: rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
      PartialMap.restrict_toRationalMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y S : Scheme
inst : X.Over S
inst_1 : Y.Over S
f : X ⤏ Y
e : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f
have mpr : ∀ (f : X.PartialMap Y) (e : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)), IsOver S f.toRationalMap
Tactic: obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f
Cleared hypotheses: f, e