awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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)
⊢ Subset (α := Set ↥S)
    (Set.range (ι := ↥(pullback π (𝒰.f i)))
      (Function.comp (β := ↥X) (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥S)
        (⇑(TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (fst π (𝒰.f i)))))) :
          (a : ↥(pullback π (𝒰.f i))) → ↥X)))
    (Set.range (ι :=
      ↥(↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme))
      ⇑(Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S)))
have rw : Subset (α := Set ↥S)
  (Set.range (ι := ↥(pullback π (𝒰.f i)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(pullback π (𝒰.f i)).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (snd π (𝒰.f i) ≫ 𝒰.f i))) ≫ b)) :
      (a : ↥(pullback π (𝒰.f i))) → ↥S))
  (Set.range (ι :=
    ↥(↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme))
    ⇑(Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S)))
Tactic: rw [← hfac, ← TopCat.coe_comp, ← Scheme.Hom.comp_base_assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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)
⊢ Subset (α := Set ↥S)
    (Set.range (ι := ↥(pullback π (𝒰.f i)))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback π (𝒰.f i)).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (snd π (𝒰.f i) ≫ 𝒰.f i))) ≫ b)) :
        (a : ↥(pullback π (𝒰.f i))) → ↥S))
    (Set.range (ι :=
      ↥(↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme))
      ⇑(Opens.ι (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S)))
have simp : Subset (α := Set ↥Y) (Set.range (ι := ↥(𝒰.X i)) (⇑(TopCat.Hom.hom (𝒰.f i).base) : (a : ↥(𝒰.X i)) → ↥Y))
  ((⇑(TopCat.Hom.hom b) : (a : ↥Y) → ↥S) ⁻¹'
    (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Set ↥S))
Tactic: simp only [Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp,
      range_eq_univ, Set.image_univ, Opens.range_ι, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (hypothesis)
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) ⋯
⊢ ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
have 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) sorry sorry) (fst π π))
Tactic: have h1 : fst (snd π (𝒰.f i)) _ ≫ fst _ _ = map _ _ _ _ (fst _ _) (fst _ _) _
    condition.symm condition.symm ≫ fst π π := by simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (hypothesis)
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 π π))
⊢ ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
have 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) sorry sorry) (snd π π))
Tactic: have h2 : snd (snd π (𝒰.f i)) _ ≫ fst _ _ = map _ _ _ _ (fst _ _) (fst _ _) _
    condition.symm condition.symm ≫ snd π π := by simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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 ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
have 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)
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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)
have 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))
Tactic: refine ⟨u ≫ Scheme.Opens.ι _, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (hypothesis)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
⊢ IsRegularEpi π
have this : Epi π
Tactic: have : Epi π := Flat.epi_of_flat_of_surjective _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
π : X ⟶ Y
inst_2 : Surjective π
inst_3 : Flat π
this : Epi π
⊢ IsRegularEpi π
have refine : ∀ (Z : Scheme.{u}) (f : X ⟶ Z) (hf : Eq (α := pullback π π ⟶ Z) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)),
  ∃ (u : Y ⟶ Z), π ≫ u = f
Tactic: refine .of_epi_of_exists fun Z f hf ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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)
⊢ ∃ (u : Y ⟶ Z), π ≫ u = f
have 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
Tactic: obtain ⟨𝒰, h⟩ := EffectiveEpiConstruction.exists_openCover_exists π f hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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)
⊢ ∃ (u : Y ⟶ Z), π ≫ u = f
have 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
Tactic: choose u hfac using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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
have 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)
Tactic: refine ⟨𝒰.glueMorphisms u ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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)
⊢ ∃ (u : Y ⟶ Z), π ≫ u = f
have refine_2 : π ≫ Cover.glueMorphisms 𝒰 u sorry = f
Tactic: refine ⟨𝒰.glueMorphisms u ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (hypothesis)
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₀
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ Z) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j)
have 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))
Tactic: have : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) :=
      Flat.epi_of_flat_of_surjective _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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))
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ Z) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ u i) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ u j)
have 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 sorry sorry))
    (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 sorry sorry))
    (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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))
| 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)
have simp : pullback.snd π (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j) ≫ 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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))
⊢ 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))
have 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 sorry sorry))
    (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: conv_rhs =>
      simp only [pullback.congrHom_hom, limit.lift_π_assoc, PullbackCone.mk_pt, cospan_right,
      PullbackCone.mk_π_app, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
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))
⊢ 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)
have 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 sorry sorry) :
        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)
Tactic: rw [← pullbackLeftPullbackSndIso_inv_snd_snd, Category.assoc,
      ← pullbackLeftPullbackSndIso_inv_snd_snd, Category.assoc, ← pullback.condition_assoc,
      ← hfac i, ← pullback.condition_assoc, ← hfac j]