awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰 𝒱 X Y Z : Cover.{v, u} (precoverage P) S
f : X ⟶ Y
g : Y ⟶ Z
⊢ HEq (α :=
    (i : X.sigma (P := P).I₀) →
      X.sigma (P := P).X i ⟶ Z.sigma (P := P).X (PreZeroHypercover.Hom.s₀ (Hom.sigma (P := P) (f ≫ g)) i))
    (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (f ≫ g))) (β :=
    (i : X.sigma (P := P).I₀) →
      X.sigma (P := P).X i ⟶
        Z.sigma (P := P).X (PreZeroHypercover.Hom.s₀ (Hom.sigma (P := P) f ≫ Hom.sigma (P := P) g) i))
    (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) f ≫ Hom.sigma (P := P) g))
have simp : Eq (α := (i : PUnit.{v + 1}) → ∐ X.X ⟶ ∐ Z.X)
  (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (f ≫ g)) :
    (i : X.sigma (P := P).I₀) →
      X.sigma (P := P).X i ⟶ Z.sigma (P := P).X (PreZeroHypercover.Hom.s₀ (Hom.sigma (P := P) (f ≫ g)) i))
  (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) f ≫ Hom.sigma (P := P) g))
Tactic: simp only [sigma_I₀, sigma_X, heq_eq_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Sigma (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰 𝒱 X Y Z : Cover.{v, u} (precoverage P) S
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (i : PUnit.{v + 1}) → ∐ X.X ⟶ ∐ Z.X)
    (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (f ≫ g)) :
      (i : X.sigma (P := P).I₀) →
        X.sigma (P := P).X i ⟶ Z.sigma (P := P).X (PreZeroHypercover.Hom.s₀ (Hom.sigma (P := P) (f ≫ g)) i))
    (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) f ≫ Hom.sigma (P := P) g))
have h : ∀ (j : X.sigma (P := P).I₀),
  Eq (α := X.sigma (P := P).X j ⟶ Z.sigma (P := P).X (PreZeroHypercover.Hom.s₀ (Hom.sigma (P := P) (f ≫ g)) j))
    (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (f ≫ g)) j)
    (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) f ≫ Hom.sigma (P := P) g) j)
Tactic: ext j : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EffectiveEpi (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : QuasiCompact f
⊢ EffectiveEpi f.base
have rw : Topology.IsQuotientMap (X := ↥X) (Y := ↥Y) ⇑f
Tactic: rw [TopCat.effectiveEpi_iff_isQuotientMap]
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
⊢ EffectiveEpi (X := AffineScheme.of Y) (Y := AffineScheme.of X) (AffineScheme.ofHom π)
have h : EffectiveEpi (X := AffineScheme.equivCommRingCat.functor.obj (AffineScheme.of Y)) (Y :=
  AffineScheme.equivCommRingCat.functor.obj (AffineScheme.of X))
  (AffineScheme.equivCommRingCat.functor.map (AffineScheme.ofHom π))
Tactic: apply AffineScheme.equivCommRingCat.functor.effectiveEpi_of_map
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
⊢ EffectiveEpi (X := AffineScheme.equivCommRingCat.functor.obj (AffineScheme.of Y)) (Y :=
    AffineScheme.equivCommRingCat.functor.obj (AffineScheme.of X))
    (AffineScheme.equivCommRingCat.functor.map (AffineScheme.ofHom π))
have h : RingHom.FaithfullyFlat (R := (↑(unop (AffineScheme.equivCommRingCat.functor.obj (AffineScheme.of Y))) : Type u)) (S :=
  (↑(unop (AffineScheme.equivCommRingCat.functor.obj (AffineScheme.of X))) : Type u))
  (CommRingCat.Hom.hom (Quiver.Hom.unop (AffineScheme.equivCommRingCat.functor.map (AffineScheme.ofHom π))))
Tactic: apply CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
⊢ ∃ (u : Y ⟶ S), π ≫ u = f
have this : EffectiveEpi (X := AffineScheme.of Y) (Y := AffineScheme.of X) (AffineScheme.ofHom π)
Tactic: have : EffectiveEpi (AffineScheme.ofHom π) := by
    apply AffineScheme.equivCommRingCat.functor.effectiveEpi_of_map
    apply CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat
    exact (Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine π).mp ⟨‹_›, ‹_›⟩
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
this : EffectiveEpi (X := AffineScheme.of Y) (Y := AffineScheme.of X) (AffineScheme.ofHom π)
⊢ ∃ (u : Y ⟶ S), π ≫ u = f
have obtain : ∀ (u : AffineScheme.of Y ⟶ AffineScheme.of S)
  (hu : Eq (α := AffineScheme.of X ⟶ AffineScheme.of S) (AffineScheme.ofHom π ≫ u) (AffineScheme.ofHom f)),
  ∃ (u : Y ⟶ S), π ≫ u = f
Tactic: obtain ⟨u, hu⟩ := IsRegularEpi.exists_of_isKernelPair
    (AffineScheme.ofHom π)
    (IsPullback.of_map (f := AffineScheme.ofHom (pullback.fst π π)) (AffineScheme.forgetToScheme)
      (InducedCategory.Hom.ext pullback.condition) (.of_hasPullback _ _))
    (AffineScheme.ofHom f) (InducedCategory.Hom.ext 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
this : EffectiveEpi (X := AffineScheme.of Y) (Y := AffineScheme.of X) (AffineScheme.ofHom π)
u : AffineScheme.of Y ⟶ AffineScheme.of S
hu : Eq (α := AffineScheme.of X ⟶ AffineScheme.of S) (AffineScheme.ofHom π ≫ u) (AffineScheme.ofHom f)
⊢ ∃ (u : Y ⟶ S), π ≫ u = f
have w : Y ⟶ S
Tactic: use u.hom, InducedCategory.Hom.ext_iff.mp hu
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
this : EffectiveEpi (X := AffineScheme.of Y) (Y := AffineScheme.of X) (AffineScheme.ofHom π)
u : AffineScheme.of Y ⟶ AffineScheme.of S
hu : Eq (α := AffineScheme.of X ⟶ AffineScheme.of S) (AffineScheme.ofHom π ≫ u) (AffineScheme.ofHom f)
w : Y ⟶ S
⊢ ∃ (u : Y ⟶ S), π ≫ u = f
have h : π ≫ u.hom = f
Tactic: use u.hom, InducedCategory.Hom.ext_iff.mp hu
-- 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)
⊢ ∃ (u : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑S.toPresheafedSpace : TopCat)), π.base ≫ u = f.base
have w : Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
  (snd π.base π.base ≫ f.base)
Tactic: apply IsRegularEpi.exists_of_isKernelPair _ (IsPullback.of_hasPullback _ _)
-- 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)
⊢ Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
    (snd π.base π.base ≫ f.base)
have this : Eq (α := forgetToTop.obj (pullback π π) ⟶ forgetToTop.obj S) (forgetToTop.map (fst π π ≫ f))
  (forgetToTop.map (snd π π ≫ f))
Tactic: have := congr(Scheme.forgetToTop.map $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)
this :
  Eq (α := forgetToTop.obj (pullback π π) ⟶ forgetToTop.obj S) (forgetToTop.map (fst π π ≫ f))
    (forgetToTop.map (snd π π ≫ f))
⊢ Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
    (snd π.base π.base ≫ f.base)
have 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)
Tactic: rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this
Cleared hypotheses: this
-- 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)
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)
⊢ Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
    (snd π.base π.base ≫ f.base)
have 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)
Tactic: rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this
Cleared hypotheses: this
-- 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)
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)
⊢ Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
    (snd π.base π.base ≫ f.base)
have 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)
Tactic: rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this
Cleared hypotheses: this
-- 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)
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)
⊢ Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
    (snd π.base π.base ≫ f.base)
have 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)
Tactic: rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this
Cleared hypotheses: this
-- 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)
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)
⊢ Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
    (snd π.base π.base ≫ f.base)
have 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)
Tactic: rwa [Functor.map_comp, Functor.map_comp, ← pullbackComparison_comp_fst_assoc,
      ← pullbackComparison_comp_snd_assoc, cancel_epi] at this
Cleared hypotheses: this
-- 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)
⊢ ∃ (𝒰 : Y.OpenCover),
    ∀ (i : 𝒰.I₀), ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
have 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)
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
-- 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)
    ⋯
⊢ ∃ (𝒰 : Y.OpenCover),
    ∀ (i : 𝒰.I₀), ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
have refine : ∀ (i : 𝒰.I₀), ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
Tactic: refine ⟨𝒰, fun i ↦ ?_⟩
-- 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₀
⊢ ∃ (u : 𝒰.X i ⟶ S), Eq (α := pullback π (𝒰.f i) ⟶ S) (fst π (𝒰.f i) ≫ f) (snd π (𝒰.f i) ≫ u)
have this : IsAffine.{u} (𝒰.X i)
Tactic: have : IsAffine (𝒰.X i) := i.2.1
-- 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)
⊢ pullback π (𝒰.f i) ⟶
    (↑(↑(↑i : TopologicalSpace.Opens ↥Y × (↑S.affineOpens : Type u)).2 : TopologicalSpace.Opens ↥S) : Scheme)
have 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)))
Tactic: apply IsOpenImmersion.lift (Scheme.Opens.ι i.1.2.1) (pullback.fst _ _ ≫ f)
-- 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))) ⇑(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)))
have 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)))
Tactic: dsimp