awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ ((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
have convert! : (g x).equiv (g y)
Tactic: convert! (PartialMap.equiv_iff_of_isSeparated (S := ⊤_ _) (f := g x) (g := g y)).mp ?_ using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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 ⋯)) ≫ (g x).hom =
    ((g x).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom
have h : ((Iso.hom (X.isoOfEq sorry) ≫ X.homOfLE sorry) ≫ Iso.inv (X.isoOfEq sorry)) ≫ (g x).hom = X.homOfLE sorry ≫ (g x).hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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 ⋯)) ≫ (g x).hom = X.homOfLE ⋯ ≫ (g x).hom
have h : (Iso.hom (X.isoOfEq sorry) ≫ X.homOfLE sorry) ≫ Iso.inv (X.isoOfEq sorry) = X.homOfLE sorry
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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 ⋯)) ≫ (g y).hom =
    ((g y).restrict ((g x).domain ⊓ (g y).domain) ⋯ ⋯).hom
have h : ((Iso.hom (X.isoOfEq sorry) ≫ X.homOfLE sorry) ≫ Iso.inv (X.isoOfEq sorry)) ≫ (g y).hom = X.homOfLE sorry ≫ (g y).hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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 ⋯)) ≫ (g y).hom = X.homOfLE ⋯ ≫ (g y).hom
have h : (Iso.hom (X.isoOfEq sorry) ≫ X.homOfLE sorry) ≫ Iso.inv (X.isoOfEq sorry) = X.homOfLE sorry
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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).equiv (g y)
have rw : (g x).toRationalMap = (g y).toRationalMap
Tactic: rw [← PartialMap.toRationalMap_eq_iff, hg₁, hg₁]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ (g x).equiv (g y)
have rw₁ : f = (g y).toRationalMap
Tactic: rw [← PartialMap.toRationalMap_eq_iff, hg₁, hg₁]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
⊢ (g x).equiv (g y)
have rw₂ : f = f
Tactic: rw [← PartialMap.toRationalMap_eq_iff, hg₁, hg₁]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).hom = f.hom
have dsimp : X.homOfLE sorry ≫
    Cover.glueMorphisms f.toRationalMap.openCoverDomain
      (fun (x : f.toRationalMap.openCoverDomain.I₀) ↦
        (X.isoOfEq sorry).inv ≫
          (Exists.choose (p := fun (g : X.PartialMap Y) ↦
              ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = (↑x : X.Opens)) sorry).hom)
      sorry =
  f.hom
Tactic: dsimp [RationalMap.toPartialMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
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
have refine : Iso.inv (X.isoOfEq sorry) ≫
    (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 sorry) :
              X.Opens))
        sorry).hom =
  f.hom
Tactic: refine (f.toRationalMap.openCoverDomain.ι_glueMorphisms _ _ ⟨_, f, rfl, rfl⟩).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
⊢ 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
have pf : 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 _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
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
⊢ 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
have pf₁ : ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
Tactic: generalize_proofs _ _ H _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
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
⊢ 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
have 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)
Tactic: generalize_proofs _ _ H _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
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)
⊢ 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
have pf₂ : 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 _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (hypothesis)
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_1 : ∃ (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_1) :
        X.Opens)
pf_2 :
  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_1) :
              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)
⊢ (X.isoOfEq pf_2).inv ≫
      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_1) :
                X.Opens)).hom =
    f.hom
have this : 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_1) :
          X.Opens)) =
  f
Tactic: have : H.choose = f := (equiv_iff_of_domain_eq_of_isSeparated (S := ⊤_ _) H.choose_spec.2).mp
    (toRationalMap_eq_iff.mp H.choose_spec.1)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
⊢ f.toPartialMap.toRationalMap = f
have obtain : ∀ (f : X.PartialMap Y), f.toRationalMap.toPartialMap.toRationalMap = f.toRationalMap
Tactic: obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.toRationalMap = f.toRationalMap
have trans : f.toRationalMap.toPartialMap.toRationalMap = (f.toRationalMap.toPartialMap.restrict f.domain sorry sorry).toRationalMap
Tactic: trans (f.toRationalMap.toPartialMap.restrict _
    f.dense_domain f.le_domain_toRationalMap).toRationalMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
trans : f.toRationalMap.toPartialMap.toRationalMap = (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap
⊢ f.toRationalMap.toPartialMap.toRationalMap = f.toRationalMap
have trans₁ : (f.toRationalMap.toPartialMap.restrict f.domain sorry sorry).toRationalMap = f.toRationalMap
Tactic: trans (f.toRationalMap.toPartialMap.restrict _
    f.dense_domain f.le_domain_toRationalMap).toRationalMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Birational.RationalMap (goal)
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap = f.toRationalMap
have e_f : f.toRationalMap.toPartialMap.restrict f.domain sorry sorry = f
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
S : Scheme
J : Type u_1
inst_2 : Category.{v_1, u_1} J
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
𝒰 : OpenCover.{u_2, u} S
inst_3 : Category.{v_2, u_2} 𝒰.I₀
inst_4 : LocallyDirected.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰
d : ColimitGluingData.{v_2, u, v_1, u_1, u_2} (P := P) D 𝒰
i : 𝒰.I₀
⊢ Eq (α := Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) i).pt)
    (d.transitionMap (P := P) (𝟙 i) :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) i).pt)
    (NatTrans.app
        (Iso.hom
          (MorphismProperty.Over.mapId (P := P) ⊤ (𝒰.X i) (Cover.trans.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰 (𝟙 i)) ⋯))
        (d.cocone (P := P) i).pt :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (𝟭 (P.Over ⊤ (𝒰.X i))) (d.cocone (P := P) i).pt)
have apply : ∀ (j : J),
  Eq (α :=
    ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ sorry).obj j ⟶
      (d.cocone (P := P) i).pt)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, u, u_1, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ sorry)
            (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i))))
        j)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i))) j)
      (d.transitionMap (P := P) (𝟙 i)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, u, u_1, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ sorry)
            (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i))))
        j)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i))) j)
      (NatTrans.app
        (Iso.hom
          (MorphismProperty.Over.mapId (P := P) ⊤ (𝒰.X i) (Cover.trans.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰 (𝟙 i)) sorry))
        (d.cocone (P := P) i).pt))
Tactic: apply (isColimitOfPreserves (Over.map ⊤ (d.prop_trans <| 𝟙 i)) (d.isColimit i)).hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
S : Scheme
J : Type u_1
inst_2 : Category.{v_1, u_1} J
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
𝒰 : OpenCover.{u_2, u} S
inst_3 : Category.{v_2, u_2} 𝒰.I₀
inst_4 : LocallyDirected.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰
d : ColimitGluingData.{v_2, u, v_1, u_1, u_2} (P := P) D 𝒰
inst_5 :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
    PreservesColimitsOfShape.{v_1, u_1, u, u, u + 1, u + 1} (C := P.Over ⊤ (𝒰.X j)) J
      (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
inst_6 : Quiver.IsThin.{u_2, v_2} 𝒰.I₀
inst_7 : Small.{u, u_2} 𝒰.I₀
inst_8 : IsZariskiLocalAtTarget P
⊢ P (X := d.relativeGluingData (P := P).glued) d.relativeGluingData (P := P).toBase
have rw : ∀ (i : 𝒰.toPreZeroHypercover.1),
  P (X :=
    PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ d.relativeGluingData (P := P).toBase 𝒰))
      i)
    (pullbackHom (P := IsOpenImmersion) 𝒰 d.relativeGluingData (P := P).toBase i :
      PreZeroHypercover.X
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ d.relativeGluingData (P := P).toBase 𝒰))
          i ⟶
        𝒰.X i)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := P) 𝒰]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
S : Scheme
J : Type u_1
inst_2 : Category.{v_1, u_1} J
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
𝒰 : OpenCover.{u_2, u} S
inst_3 : Category.{v_2, u_2} 𝒰.I₀
inst_4 : LocallyDirected.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰
d : ColimitGluingData.{v_2, u, v_1, u_1, u_2} (P := P) D 𝒰
inst_5 :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
    PreservesColimitsOfShape.{v_1, u_1, u, u, u + 1, u + 1} (C := P.Over ⊤ (𝒰.X j)) J
      (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
inst_6 : Quiver.IsThin.{u_2, v_2} 𝒰.I₀
inst_7 : Small.{u, u_2} 𝒰.I₀
inst_8 : IsZariskiLocalAtTarget P
i : 𝒰.toPreZeroHypercover.1
⊢ P (X :=
    PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ d.relativeGluingData (P := P).toBase 𝒰))
      i)
    (pullbackHom (P := IsOpenImmersion) 𝒰 d.relativeGluingData (P := P).toBase i :
      PreZeroHypercover.X
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ d.relativeGluingData (P := P).toBase 𝒰))
          i ⟶
        𝒰.X i)
have rw : P (d.relativeGluingData (P := P).natTrans.app i)
Tactic: rw [Scheme.Cover.pullbackHom,
      ← (d.relativeGluingData.isPullback_natTrans_ι_toBase i).flip.isoPullback_inv_snd,
      P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
S : Scheme
J : Type u_1
inst_2 : Category.{v_1, u_1} J
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
𝒰 : OpenCover.{u_2, u} S
inst_3 : Category.{v_2, u_2} 𝒰.I₀
inst_4 : LocallyDirected.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰
d : ColimitGluingData.{v_2, u, v_1, u_1, u_2} (P := P) D 𝒰
inst_5 :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
    PreservesColimitsOfShape.{v_1, u_1, u, u, u + 1, u + 1} (C := P.Over ⊤ (𝒰.X j)) J
      (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
inst_6 : Quiver.IsThin.{u_2, v_2} 𝒰.I₀
inst_7 : Small.{u, u_2} 𝒰.I₀
inst_8 : IsZariskiLocalAtTarget P
𝒱 : (a : J) → OpenCover.{u_2, u} (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).left :=
  fun (a : J) ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰
⊢ Cocone D
have refine_1 : (a : J) → D.obj a ⟶ Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.glued (P := P))) a
Tactic: refine { pt := d.glued, ι.app a := ?_, ι.naturality {a b} f := ?_ }