awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
𝒰 : Cover.{v, u} (precoverage P) S
refine :
  ∀ (s : ↥S),
    ∃ (i :
      PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
        { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
      Membership.mem (γ := Set ↥S)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
              i))
        s
⊢ (∀ (x : ↥S),
      ∃ (i :
        PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
          { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
        Membership.mem (γ := Set ↥S)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                  f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                  f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
          { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
      P
        (PreZeroHypercover.f
          { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
            PreZeroHypercover.{v, u, u + 1} S }
          i)

Tactic:
refine ⟨fun s ↦ ?_, fun _ ↦ IsZariskiLocalAtSource.sigmaDesc 𝒰.map_prop⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
𝒰 : Cover.{v, u} (precoverage P) S
s : ↥S
obtain :
  ∀ (i : 𝒰.I₀) (y : ↥(𝒰.X i)),
    ∃ (i_1 :
      PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
        { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
      Membership.mem (α := ↥S) (γ := Set ↥S)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
              i_1))
          ⇑(PreZeroHypercover.f
              { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X,
                f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f : PreZeroHypercover.{v, u, u + 1} S }
              i_1))
        ((𝒰.f i) y : ↥S)
⊢ ∃ (i :
    PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
      { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
    Membership.mem (γ := Set ↥S)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i))
      s

Tactic:
obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq s

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
𝒰 : Cover.{v, u} (precoverage P) S
i : 𝒰.I₀
y : ↥(𝒰.X i)
⊢ Eq (α := ↥S)
    ((PreZeroHypercover.f
          { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }
          default)
        ((Sigma.ι 𝒰.X i) y : ↥(∐ 𝒰.X)) :
      ↥S)
    ((𝒰.f i) y : ↥S)

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
𝒰 : Cover.{v, u} (precoverage P) S
i : 𝒰.I₀
y : ↥(𝒰.X i)
⊢ ∃ (i_1 :
    PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := S)
      { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f }),
    Membership.mem (α := ↥S) (γ := Set ↥S)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i_1))
        ⇑(PreZeroHypercover.f
            { I₀ := PUnit.{v + 1}, X := fun (x : PUnit.{v + 1}) ↦ ∐ 𝒰.X, f := fun (x : PUnit.{v + 1}) ↦ Sigma.desc 𝒰.f :
              PreZeroHypercover.{v, u, u + 1} S }
            i_1))
      ((𝒰.f i) y : ↥S)

Tactic:
refine ⟨default, Sigma.ι 𝒰.X i y, by simp [← Scheme.Hom.comp_apply]⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
S : Scheme
𝒰 : Cover.{v, u} (precoverage P) S
⊢ PreZeroHypercover.presieve₀.{v, u, u + 1} 𝒰.sigma (P := P).toPreZeroHypercover =
    Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f)

Tactic:
le_antisymm ?_ fun T g ⟨⟩ ↦ ⟨⟨⟩⟩

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
S : Scheme
𝒰 : Cover.{v, u} (precoverage P) S
refine :
  PreZeroHypercover.presieve₀.{v, u, u + 1} 𝒰.sigma (P := P).toPreZeroHypercover ≤
    Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f)
⊢ PreZeroHypercover.presieve₀.{v, u, u + 1} 𝒰.sigma (P := P).toPreZeroHypercover =
    Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f)

Tactic:
refine le_antisymm ?_ fun T g ⟨⟩ ↦ ⟨⟨⟩⟩

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
S : Scheme
𝒰 : Cover.{v, u} (precoverage P) S
rw : ∀ (i : 𝒰.sigma (P := P).I₀), Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f) (𝒰.sigma (P := P).f i)
⊢ PreZeroHypercover.presieve₀.{v, u, u + 1} 𝒰.sigma (P := P).toPreZeroHypercover ≤
    Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f)

Tactic:
rw [Presieve.ofArrows_le_iff]

Premises used: CategoryTheory.Presieve.ofArrows_le_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
S : Scheme
𝒰 : Cover.{v, u} (precoverage P) S
i : 𝒰.sigma (P := P).I₀
⊢ Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f) (𝒰.sigma (P := P).f i)

Tactic:
Presieve.singleton_self _

Premises used: CategoryTheory.Presieve.singleton_self, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.desc
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
S : Scheme
𝒰 : Cover.{v, u} (precoverage P) S
i : 𝒰.sigma (P := P).I₀
⊢ Presieve.singleton (Y := ∐ 𝒰.X) (Sigma.desc 𝒰.f) (𝒰.sigma (P := P).f i)

Tactic:
exact Presieve.singleton_self _

Premises used: CategoryTheory.Presieve.singleton_self
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰 𝒱 : Cover.{v, u} (precoverage P) S
f : 𝒰 ⟶ 𝒱
x : 𝒰.sigma (P := P).I₀
⊢ ∀ (b : 𝒰.I₀),
    CategoryStruct.comp (Y := ∐ 𝒰.X) (Sigma.ι 𝒰.X b)
        (CategoryStruct.comp (Y := 𝒱.sigma (P := P).X default)
          (Sigma.desc fun (j : 𝒰.I₀) ↦ f.h₀ j ≫ Sigma.ι 𝒱.X (f.s₀ j)) (𝒱.sigma (P := P).f default)) =
      Sigma.ι 𝒰.X b ≫ 𝒰.sigma (P := P).f x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰_1 𝒱 𝒰 : Cover.{v, u} (precoverage P) S
simp : PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰)) = PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P)))
⊢ HEq (α :=
    (i : 𝒰.sigma (P := P).I₀) →
      𝒰.sigma (P := P).X i ⟶ 𝒰.sigma (P := P).X (PreZeroHypercover.Hom.s₀ (Hom.sigma (P := P) (𝟙 𝒰)) i))
    (PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰))) (PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P))))

Tactic:
simp only [sigma_I₀, sigma_X, heq_eq_eq]

Premises used: heq_eq_eq, AlgebraicGeometry.Scheme.Cover.sigma_X, AlgebraicGeometry.Scheme.Cover.sigma_I₀
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰_1 𝒱 𝒰 : Cover.{v, u} (precoverage P) S
h :
  ∀ (j : 𝒰.sigma (P := P).I₀),
    PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰)) j = PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P))) j
⊢ PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰)) = PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P)))

Tactic:
ext j : 1
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰_1 𝒱 𝒰 : Cover.{v, u} (precoverage P) S
j : 𝒰.sigma (P := P).I₀
⊢ ∀ (b : 𝒰.I₀),
    Sigma.ι 𝒰.X b ≫ PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰)) j =
      Sigma.ι 𝒰.X b ≫ PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P))) j

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : IsZariskiLocalAtSource P
inst_1 : UnivLE.{v, u}
inst_2 : P.IsMultiplicative
𝒰_1 𝒱 𝒰 : Cover.{v, u} (precoverage P) S
j : 𝒰.sigma (P := P).I₀
⊢ PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (𝟙 𝒰)) j = PreZeroHypercover.Hom.h₀ (𝟙 (𝒰.sigma (P := P))) j

Tactic:
exact Sigma.hom_ext _ _ (by simp)

Premises used: CategoryTheory.Limits.Sigma.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
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
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))
⊢ 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))

Tactic:
simp only [sigma_I₀, sigma_X, heq_eq_eq]

Premises used: heq_eq_eq, AlgebraicGeometry.Scheme.Cover.sigma_X, AlgebraicGeometry.Scheme.Cover.sigma_I₀
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
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
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)
⊢ 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:
ext j : 1
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
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
j : X.sigma (P := P).I₀
⊢ ∀ (b : X.I₀),
    Eq (α := X.X b ⟶ Z.sigma (P := P).X (PreZeroHypercover.Hom.s₀ (Hom.sigma (P := P) (f ≫ g)) j))
      (Sigma.ι X.X b ≫ PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) (f ≫ g)) j)
      (Sigma.ι X.X b ≫ PreZeroHypercover.Hom.h₀ (Hom.sigma (P := P) f ≫ Hom.sigma (P := P) g) j)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Sigma
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
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:
exact Sigma.hom_ext _ _ (by simp)

Premises used: CategoryTheory.Limits.Sigma.hom_ext
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : QuasiCompact f
rw : Topology.IsQuotientMap (X := ↥X) (Y := ↥Y) ⇑f
⊢ EffectiveEpi f.base

Tactic:
rw [TopCat.effectiveEpi_iff_isQuotientMap]

Premises used: TopCat.effectiveEpi_iff_isQuotientMap
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : QuasiCompact f
⊢ Topology.IsQuotientMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
Flat.isQuotientMap_of_surjective _

Premises used: AlgebraicGeometry.Flat.isQuotientMap_of_surjective
-- Module: Mathlib.AlgebraicGeometry.EffectiveEpi
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : QuasiCompact f
⊢ Topology.IsQuotientMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
exact Flat.isQuotientMap_of_surjective _

Premises used: AlgebraicGeometry.Flat.isQuotientMap_of_surjective
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
h :
  EffectiveEpi (X := AffineScheme.equivCommRingCat.functor.obj (AffineScheme.of Y)) (Y :=
    AffineScheme.equivCommRingCat.functor.obj (AffineScheme.of X))
    (AffineScheme.equivCommRingCat.functor.map (AffineScheme.ofHom π))
⊢ EffectiveEpi (X := AffineScheme.of Y) (Y := AffineScheme.of X) (AffineScheme.ofHom π)

Tactic:
apply AffineScheme.equivCommRingCat.functor.effectiveEpi_of_map

Premises used: CategoryTheory.Functor.effectiveEpi_of_map, CategoryTheory.Equivalence.functor, AlgebraicGeometry.AffineScheme.equivCommRingCat
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
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 π))))
⊢ 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 CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat

Premises used: CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
⊢ 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:
(Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine π).mp ⟨‹_›, ‹_›⟩

Premises used: AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, And.intro, Iff.mp
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
⊢ 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:
exact (Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine π).mp ⟨‹_›, ‹_›⟩

Premises used: AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine, And.intro, Iff.mp
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
⊢ 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 ⟨‹_›, ‹_›⟩
-- 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) (pullback.fst π π ≫ f) (pullback.snd π π ≫ f)
inst_4 : IsAffine S
this : EffectiveEpi (X := AffineScheme.of Y) (Y := AffineScheme.of X) (AffineScheme.ofHom π)
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
⊢ ∃ (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)

Premises used: CategoryTheory.IsPullback.of_map, CategoryTheory.IsRegularEpi.exists_of_isKernelPair, AlgebraicGeometry.AffineScheme.ofHom, CategoryTheory.InducedCategory.Hom.ext, AlgebraicGeometry.AffineScheme.forgetToScheme, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.Limits.pullback.condition
-- 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) (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
h : π ≫ u.hom = f
⊢ ∃ (u : Y ⟶ S), π ≫ u = f

Tactic:
use u.hom, InducedCategory.Hom.ext_iff.mp hu

Premises used: CategoryTheory.InducedCategory.Hom.ext_iff, Iff.mp, CategoryTheory.InducedCategory.Hom.hom
-- 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)
w :
  Eq (α := pullback π.base π.base ⟶ (↑S.toPresheafedSpace : TopCat)) (fst π.base π.base ≫ f.base)
    (snd π.base π.base ≫ f.base)
⊢ ∃ (u : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑S.toPresheafedSpace : TopCat)), π.base ≫ u = f.base

Tactic:
apply IsRegularEpi.exists_of_isKernelPair _ (IsPullback.of_hasPullback _ _)

Premises used: CategoryTheory.IsRegularEpi.exists_of_isKernelPair, CategoryTheory.IsPullback.of_hasPullback
-- 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)
⊢ Eq (α := forgetToTop.obj (pullback π π) ⟶ forgetToTop.obj S) (forgetToTop.map (fst π π ≫ f))
    (forgetToTop.map (snd π π ≫ f))

Tactic:
have := congr(Scheme.forgetToTop.map $hf)