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)
this :
  Eq (α := forgetToTop.obj (pullback π π) ⟶ forgetToTop.obj S) (forgetToTop.map (fst π π ≫ f))
    (forgetToTop.map (snd π π ≫ f))
w :
  ∀
    (this :
      Eq (α := forgetToTop.obj (pullback π π) ⟶ forgetToTop.obj S) (forgetToTop.map (fst π π) ≫ forgetToTop.map f)
        (forgetToTop.map (snd π π ≫ f))),
    Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
      (snd π.base π.base ≫ f.base)
w₁ :
  ∀
    (this :
      Eq (α := forgetToTop.obj (pullback π π) ⟶ forgetToTop.obj S) (forgetToTop.map (fst π π) ≫ forgetToTop.map f)
        (forgetToTop.map (snd π π) ≫ forgetToTop.map f)),
    Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
      (snd π.base π.base ≫ f.base)
w₂ :
  ∀
    (this :
      Eq (α := forgetToTop.obj (pullback π π) ⟶ forgetToTop.obj S)
        (CategoryStruct.comp (Y := pullback (forgetToTop.map π) (forgetToTop.map π))
          (pullbackComparison forgetToTop π π) (fst (forgetToTop.map π) (forgetToTop.map π) ≫ forgetToTop.map f))
        (forgetToTop.map (snd π π) ≫ forgetToTop.map f)),
    Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
      (snd π.base π.base ≫ f.base)
w₃ :
  ∀
    (this :
      Eq (α := forgetToTop.obj (pullback π π) ⟶ forgetToTop.obj S)
        (CategoryStruct.comp (Y := pullback (forgetToTop.map π) (forgetToTop.map π))
          (pullbackComparison forgetToTop π π) (fst (forgetToTop.map π) (forgetToTop.map π) ≫ forgetToTop.map f))
        (CategoryStruct.comp (Y := pullback (forgetToTop.map π) (forgetToTop.map π))
          (pullbackComparison forgetToTop π π) (snd (forgetToTop.map π) (forgetToTop.map π) ≫ forgetToTop.map f))),
    Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
      (snd π.base π.base ≫ f.base)
w₄ w₅ w₆ w₇ :
  ∀
    (this :
      Eq (α := pullback (forgetToTop.map π) (forgetToTop.map π) ⟶ forgetToTop.obj S)
        (fst (forgetToTop.map π) (forgetToTop.map π) ≫ forgetToTop.map f)
        (snd (forgetToTop.map π) (forgetToTop.map π) ≫ forgetToTop.map f)),
    Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
      (snd π.base π.base ≫ f.base)
⊢ Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
    (snd π.base π.base ≫ f.base)

Tactic:
rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this

Premises used: CategoryTheory.Limits.pullbackComparison_comp_snd_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.Limits.pullbackComparison_comp_fst_assoc
-- 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)
obtain :
  ∀ (b : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑S.toPresheafedSpace : TopCat)) (hfac : π.base ≫ b = f.base),
    ∃ (𝒰 : Y.OpenCover),
      ∀ (i : 𝒰.I₀), ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
⊢ ∃ (𝒰 : Y.OpenCover),
    ∀ (i : 𝒰.I₀), ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)

Tactic:
obtain ⟨b, hfac⟩ : ∃ (u : Y.carrier ⟶ S.carrier), π.base ≫ u = f.base := by
    apply IsRegularEpi.exists_of_isKernelPair _ (IsPullback.of_hasPullback _ _)
    have := congr(Scheme.forgetToTop.map $hf)
    rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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)
    ⋯
⊢ ∃ (𝒰 : Y.OpenCover),
    ∀ (i : 𝒰.I₀), ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)

Tactic:
⟨𝒰, fun i ↦ ?_⟩

Premises used: Exists.intro
-- 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)
    ⋯
refine : ∀ (i : 𝒰.I₀), ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
⊢ ∃ (𝒰 : Y.OpenCover),
    ∀ (i : 𝒰.I₀), ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)

Tactic:
refine ⟨𝒰, fun i ↦ ?_⟩
-- 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₀
⊢ IsAffine.{u} (𝒰.X i)

Tactic:
have : IsAffine (𝒰.X i) := i.2.1
-- 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)
apply :
  Subset (α := Set ↥S) (Set.range (ι := ↥(pullback π (𝒰.f i))) ⇑(fst π (𝒰.f i) ≫ f))
    (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)))
⊢ pullback π (𝒰.f i) ⟶
    (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme)

Tactic:
apply IsOpenImmersion.lift (Scheme.Opens.ι i.1.2.1) (pullback.fst _ _ ≫ f)

Premises used: AlgebraicGeometry.IsOpenImmersion.lift, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Opens.ι, Subtype.val, Prod.snd
-- 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)
dsimp :
  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)))
⊢ Subset (α := Set ↥S) (Set.range (ι := ↥(pullback π (𝒰.f i))) ⇑(fst π (𝒰.f i) ≫ f))
    (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:
dsimp
-- 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)
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)))
⊢ 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)))

Tactic:
rw [← hfac, ← TopCat.coe_comp, ← Scheme.Hom.comp_base_assoc, pullback.condition]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_base_assoc, CategoryTheory.Limits.pullback.condition, TopCat.coe_comp
-- 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)
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))
⊢ 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:
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]

Premises used: Set.range_comp, Set.image_univ, ContinuousMap.coe_comp, AlgebraicGeometry.range_eq_univ, AlgebraicGeometry.Scheme.Opens.range_ι, Set.image_subset_iff, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.hom_comp
-- 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)
⊢ Set.range (ι := ↥(𝒰.X i)) (⇑(TopCat.Hom.hom (𝒰.f i).base) : (a : ↥(𝒰.X i)) → ↥Y) ⊆
    (↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).1 : Set ↥Y)

Tactic:
simp [𝒰]
-- 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)
⊢ 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:
exact trans (by simp [𝒰]) i.2.2
-- 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) ⋯
⊢ 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 π π))

Tactic:
simp
-- 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) ⋯
⊢ 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 π π))

Tactic:
have h1 : fst (snd π (𝒰.f i)) _ ≫ fst _ _ = map _ _ _ _ (fst _ _) (fst _ _) _
    condition.symm condition.symm ≫ fst π π := by simp
-- 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 π π))
⊢ 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 π π))

Tactic:
simp
-- 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 π π))
⊢ 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 π π))

Tactic:
have h2 : snd (snd π (𝒰.f i)) _ ≫ fst _ _ = map _ _ _ _ (fst _ _) (fst _ _) _
    condition.symm condition.symm ≫ snd π π := by simp