awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
f : X ⟶ S
hf : Eq (α := pullback π π ⟶ S) (fst π π ≫ f) (snd π π ≫ f)
b : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑S.toPresheafedSpace : TopCat)
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun
        (V :
          { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u) //
            x.1 ∈ Y.affineOpens ∧
              x.1 ≤
                (TopologicalSpace.Opens.comap (TopCat.Hom.hom b) :
                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
                  (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
      (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).1)
    ⋯
i : 𝒰.I₀
this : IsAffine.{u} (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶
  (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme) :=
  IsOpenImmersion.lift
    (Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S))
    (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (fst π π))
h2 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (snd π π))
⊢ Eq (α :=
    pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶
      (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme))
    (fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ f') (snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ f')

Tactic:
simp only [← cancel_mono (Scheme.Opens.ι i.1.2.1),
      Category.assoc, IsOpenImmersion.lift_fac, f', reassoc_of% h1, reassoc_of% h2, hf]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι, Subtype.val, Prod.snd, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
f : X ⟶ S
hf : Eq (α := pullback π π ⟶ S) (fst π π ≫ f) (snd π π ≫ f)
b : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑S.toPresheafedSpace : TopCat)
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun
        (V :
          { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u) //
            x.1 ∈ Y.affineOpens ∧
              x.1 ≤
                (TopologicalSpace.Opens.comap (TopCat.Hom.hom b) :
                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
                  (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
      (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).1)
    ⋯
i : 𝒰.I₀
this : IsAffine.{u} (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶
  (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme) :=
  IsOpenImmersion.lift
    (Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S))
    (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (fst π π))
h2 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (snd π π))
obtain :
  ∀
    (u :
      𝒰.X i ⟶ (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme))
    (hu : snd π (𝒰.f i) ≫ u = f'),
    ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
⊢ ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)

Tactic:
obtain ⟨u, hu⟩ := of_isAffine_target (pullback.snd π (𝒰.f i)) f' <| by
    simp only [← cancel_mono (Scheme.Opens.ι i.1.2.1),
      Category.assoc, IsOpenImmersion.lift_fac, f', reassoc_of% h1, reassoc_of% h2, hf]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, _private.0.AlgebraicGeometry.EffectiveEpiConstruction.of_isAffine_target
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
f : X ⟶ S
hf : Eq (α := pullback π π ⟶ S) (fst π π ≫ f) (snd π π ≫ f)
b : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑S.toPresheafedSpace : TopCat)
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun
        (V :
          { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u) //
            x.1 ∈ Y.affineOpens ∧
              x.1 ≤
                (TopologicalSpace.Opens.comap (TopCat.Hom.hom b) :
                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
                  (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
      (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).1)
    ⋯
i : 𝒰.I₀
this : IsAffine.{u} (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶
  (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme) :=
  IsOpenImmersion.lift
    (Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S))
    (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (fst π π))
h2 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (snd π π))
u : 𝒰.X i ⟶ (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme)
hu : snd π (𝒰.f i) ≫ u = f'
⊢ ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)

Tactic:
⟨u ≫ Scheme.Opens.ι _, ?_⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
f : X ⟶ S
hf : Eq (α := pullback π π ⟶ S) (fst π π ≫ f) (snd π π ≫ f)
b : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑S.toPresheafedSpace : TopCat)
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun
        (V :
          { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u) //
            x.1 ∈ Y.affineOpens ∧
              x.1 ≤
                (TopologicalSpace.Opens.comap (TopCat.Hom.hom b) :
                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
                  (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
      (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).1)
    ⋯
i : 𝒰.I₀
this : IsAffine.{u} (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶
  (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme) :=
  IsOpenImmersion.lift
    (Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S))
    (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (fst π π))
h2 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (snd π π))
u : 𝒰.X i ⟶ (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme)
hu : snd π (𝒰.f i) ≫ u = f'
refine :
  Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f)
    (snd π (𝒰.f i) ≫
      u ≫ Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S))
⊢ ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)

Tactic:
refine ⟨u ≫ Scheme.Opens.ι _, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
f : X ⟶ S
hf : Eq (α := pullback π π ⟶ S) (fst π π ≫ f) (snd π π ≫ f)
b : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑S.toPresheafedSpace : TopCat)
hfac : π.base ≫ b = f.base
𝒰 : Y.OpenCover :=
  Y.openCoverOfIsOpenCover
    (fun
        (V :
          { x : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u) //
            x.1 ∈ Y.affineOpens ∧
              x.1 ≤
                (TopologicalSpace.Opens.comap (TopCat.Hom.hom b) :
                    (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥Y)
                  (↑x.2 : TopologicalSpace.Opens ↥S) }) ↦
      (↑V : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).1)
    ⋯
i : 𝒰.I₀
this : IsAffine.{u} (𝒰.X i)
f' : pullback π (𝒰.f i) ⟶
  (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme) :=
  IsOpenImmersion.lift
    (Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S))
    (fst π (𝒰.f i) ≫ f) ⋯
h1 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (fst (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (fst π π))
h2 :
  Eq (α := pullback (X := pullback π (𝒰.f i)) (Y := pullback π (𝒰.f i)) (snd π (𝒰.f i)) (snd π (𝒰.f i)) ⟶ X)
    (snd (snd π (𝒰.f i)) (snd π (𝒰.f i)) ≫ fst π (𝒰.f i))
    (CategoryStruct.comp (Y := pullback π π)
      (map (snd π (𝒰.f i)) (snd π (𝒰.f i)) π π (fst π (𝒰.f i)) (fst π (𝒰.f i)) (𝒰.f i) ⋯ ⋯) (snd π π))
u : 𝒰.X i ⟶ (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme)
hu : snd π (𝒰.f i) ≫ u = f'
⊢ Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f)
    (snd π (𝒰.f i) ≫
      u ≫ Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S))

Tactic:
simp [reassoc_of% hu, f']
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
⊢ Epi π

Tactic:
have : Epi π := Flat.epi_of_flat_of_surjective _
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
⊢ IsRegularEpi π

Tactic:
.of_epi_of_exists fun Z f hf ↦ ?_

Premises used: CategoryTheory.IsRegularEpi.of_epi_of_exists
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
refine :
  ∀ (Z : Scheme.{u}) (f : X ⟶ Z) (hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)),
    ∃ (u : Y ⟶ Z), π ≫ u = f
⊢ IsRegularEpi π

Tactic:
refine .of_epi_of_exists fun Z f hf ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
obtain :
  ∀ (𝒰 : Y.OpenCover)
    (h :
      ∀ (i : 𝒰.I₀),
        ∃ (u : 𝒰.X i ⟶ Z), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u)),
    ∃ (u : Y ⟶ Z), π ≫ u = f
⊢ ∃ (u : Y ⟶ Z), π ≫ u = f

Tactic:
obtain ⟨𝒰, h⟩ := EffectiveEpiConstruction.exists_openCover_exists π f hf

Premises used: _private.0.AlgebraicGeometry.EffectiveEpiConstruction.exists_openCover_exists
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
h :
  ∀ (i : 𝒰.I₀),
    ∃ (u : 𝒰.X i ⟶ Z), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u)
choose :
  ∀ (u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z)
    (hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)),
    ∃ (u : Y ⟶ Z), π ≫ u = f
⊢ ∃ (u : Y ⟶ Z), π ≫ u = f

Tactic:
choose u hfac using h
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
⊢ ∃ (u : Y ⟶ Z), π ≫ u = f

Tactic:
⟨𝒰.glueMorphisms u ?_, ?_⟩

Premises used: AlgebraicGeometry.Scheme.Cover.glueMorphisms, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
refine_1 :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Z) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ u x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ u y)
refine_2 : π ≫ Cover.glueMorphisms 𝒰 u ⋯ = f
⊢ ∃ (u : Y ⟶ Z), π ≫ u = f

Tactic:
refine ⟨𝒰.glueMorphisms u ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
i j : 𝒰.I₀
⊢ Epi (X := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))

Tactic:
have : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) :=
      Flat.epi_of_flat_of_surjective _
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this_1 : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
i j : 𝒰.I₀
this :
  Epi (X := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
refine_1 :
  Eq (α := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
    (CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
      (Iso.hom (pullback.congrHom ⋯ ⋯))
      (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i))
    (CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
      (Iso.hom (pullback.congrHom ⋯ ⋯))
      (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j))
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ Z) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j)

Tactic:
rw [← cancel_epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)),
      ← cancel_epi (pullback.congrHom rfl pullback.condition.symm).hom]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.pullback.congrHom, CategoryTheory.Limits.pullback.condition, Eq.symm, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this_1 : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
i j : 𝒰.I₀
this :
  Epi (X := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
simp : pullback.snd π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j
| CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    (Iso.hom (pullback.congrHom ⋯ ⋯))
    (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j)

Tactic:
simp only [pullback.congrHom_hom, limit.lift_π_assoc, PullbackCone.mk_pt, cospan_right,
      PullbackCone.mk_π_app, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Category.comp_id, CategoryTheory.Limits.cospan_right, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.pullback.congrHom_hom
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this_1 : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
i j : 𝒰.I₀
this :
  Epi (X := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
refine_1 :
  Eq (α := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
    (CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
      (Iso.hom (pullback.congrHom ⋯ ⋯))
      (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i))
    (pullback.snd π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j)
⊢ Eq (α := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
    (CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
      (Iso.hom (pullback.congrHom ⋯ ⋯))
      (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i))
    (CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
      (Iso.hom (pullback.congrHom ⋯ ⋯))
      (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j))

Tactic:
conv_rhs =>
      simp only [pullback.congrHom_hom, limit.lift_π_assoc, PullbackCone.mk_pt, cospan_right,
      PullbackCone.mk_π_app, Category.comp_id]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Category.comp_id, CategoryTheory.Limits.cospan_right, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.pullback.congrHom_hom
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this_1 : Epi π
Z : Scheme
f : X ⟶ Z
hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), Eq (α := pullback π (𝒰.f i) ⟶ Z) (pullback.fst π (𝒰.f i) ≫ f) (pullback.snd π (𝒰.f i) ≫ u i)
i j : 𝒰.I₀
this :
  Epi (X := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
refine_1 :
  Eq (α := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
    (CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
        (Iso.hom (pullback.congrHom ⋯ ⋯) :
          pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶
            pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
        (CategoryStruct.comp (Y :=
            pullback (X := pullback π (𝒰.f i)) (Y := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd π (𝒰.f i))
              (pullback.fst (𝒰.f i) (𝒰.f j)))
            (Iso.inv (pullbackLeftPullbackSndIso π (𝒰.f i) (pullback.fst (𝒰.f i) (𝒰.f j))))
            (pullback.fst (pullback.snd π (𝒰.f i)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≫ pullback.fst π (𝒰.f i) ≫ f) :
          pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ⟶ Z) :
      pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
    (CategoryStruct.comp (Y :=
        pullback (X := pullback π (𝒰.f j)) (Y := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd π (𝒰.f j))
          (pullback.snd (𝒰.f i) (𝒰.f j)))
        (Iso.inv (pullbackLeftPullbackSndIso π (𝒰.f j) (pullback.snd (𝒰.f i) (𝒰.f j))))
        (pullback.fst (pullback.snd π (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≫ pullback.fst π (𝒰.f j) ≫ f) :
      pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
⊢ Eq (α := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ⟶ Z)
    (CategoryStruct.comp (Y := pullback (Y := pullback (𝒰.f i) (𝒰.f j)) π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
      (Iso.hom (pullback.congrHom ⋯ ⋯))
      (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i))
    (pullback.snd π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ≫ pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j)

Tactic:
rw [← pullbackLeftPullbackSndIso_inv_snd_snd, Category.assoc,
      ← pullbackLeftPullbackSndIso_inv_snd_snd, Category.assoc, ← pullback.condition_assoc,
      ← hfac i, ← pullback.condition_assoc, ← hfac j]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_snd_snd