awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X : Scheme
⊢ Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X : Scheme
refine_1 : Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)
refine_2 :
  ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
    Flat (Spec.map f) →
      Surjective (Spec.map f) → Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))
⊢ Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X : Scheme
⊢ Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)

Tactic:
GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X : Scheme
⊢ Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)

Tactic:
exact GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X : Scheme
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ IsRegularEpi (Spec.map f)

Tactic:
have : IsRegularEpi (Spec.map f) :=
      isRegularEpi_of_flat_of_surjective_of_isAffine _
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X : Scheme
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : IsRegularEpi (Spec.map f)
⊢ Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))

Tactic:
.singleton_of_isRepresentable_of_effectiveEpi _ _

Premises used: CategoryTheory.Presieve.IsSheafFor.singleton_of_isRepresentable_of_effectiveEpi
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X : Scheme
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : IsRegularEpi (Spec.map f)
⊢ Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))

Tactic:
exact .singleton_of_isRepresentable_of_effectiveEpi _ _
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
⊢ fppfTopology.Subcanonical

Tactic:
.of_le fppfTopology_le_fpqcTopology

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_le, AlgebraicGeometry.Scheme.fppfTopology_le_fpqcTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : LocallyOfFinitePresentation f
rw : (Presieve.ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ f) ∈ fppfPrecoverage.coverings Y
⊢ Presieve.singleton f ∈ fppfPrecoverage.coverings Y

Tactic:
rw [← Presieve.ofArrows_pUnit.{_, _, 0}]

Premises used: CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : LocallyOfFinitePresentation f
⊢ (Presieve.ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ f) ∈ fppfPrecoverage.coverings Y

Tactic:
(f.cover (P := @Flat ⊓ @LocallyOfFinitePresentation) ⟨‹_›, ‹_›⟩).mem₀

Premises used: Set.Mem, And.intro, CategoryTheory.Precoverage.ZeroHypercover.mem₀, AlgebraicGeometry.Scheme.Hom.cover
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : LocallyOfFinitePresentation f
⊢ (Presieve.ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ f) ∈ fppfPrecoverage.coverings Y

Tactic:
exact (f.cover (P := @Flat ⊓ @LocallyOfFinitePresentation) ⟨‹_›, ‹_›⟩).mem₀

Premises used: And.intro, CategoryTheory.Precoverage.ZeroHypercover.mem₀, AlgebraicGeometry.Scheme.Hom.cover
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : QuasiCompact f
⊢ Presieve.singleton f ∈ fpqcPrecoverage.coverings Y

Tactic:
Hom.singleton_mem_propQCPrecoverage ‹_›

Premises used: Set.Mem, AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : Surjective f
inst_2 : Flat f
rw : ∀ (Y_1 : Scheme.{u_1}), Presieve.IsSheafFor (Functor.obj yoneda Y_1) (Presieve.singleton f)
⊢ EffectiveEpi f

Tactic:
rw [← Sieve.effectiveEpimorphic_singleton,
    Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]

Premises used: CategoryTheory.Sieve.effectiveEpimorphic_singleton, CategoryTheory.Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : Surjective f
inst_2 : Flat f
Z : Scheme
⊢ Presieve.IsSheafFor (Functor.obj yoneda Z) (Presieve.singleton f)

Tactic:
(GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _).isSheafFor _
    (Precoverage.generate_mem_toGrothendieck f.singleton_mem_fpqcPrecoverage)

Premises used: AlgebraicGeometry.Scheme.Hom.singleton_mem_fpqcPrecoverage, CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable, CategoryTheory.Presieve.IsSheaf.isSheafFor
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : Surjective f
inst_2 : Flat f
Z : Scheme
⊢ Presieve.IsSheafFor (Functor.obj yoneda Z) (Presieve.singleton f)

Tactic:
exact (GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _).isSheafFor _
    (Precoverage.generate_mem_toGrothendieck f.singleton_mem_fpqcPrecoverage)

Premises used: AlgebraicGeometry.Scheme.Hom.singleton_mem_fpqcPrecoverage, CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable, CategoryTheory.Presieve.IsSheaf.isSheafFor
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Surjective f
inst_2 : Flat f
rw : ∀ (Y_1 : Scheme.{u_1}), Presieve.IsSheafFor (Functor.obj yoneda Y_1) (Presieve.singleton f)
⊢ EffectiveEpi f

Tactic:
rw [← Sieve.effectiveEpimorphic_singleton,
    Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]

Premises used: CategoryTheory.Sieve.effectiveEpimorphic_singleton, CategoryTheory.Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Surjective f
inst_2 : Flat f
Z : Scheme
⊢ Presieve.IsSheafFor (Functor.obj yoneda Z) (Presieve.singleton f)

Tactic:
(GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _).isSheafFor _
    (Precoverage.generate_mem_toGrothendieck f.singleton_mem_fppfPrecoverage)

Premises used: AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage, CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable, CategoryTheory.Presieve.IsSheaf.isSheafFor
-- Module: Mathlib.AlgebraicGeometry.Sites.Fpqc
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Surjective f
inst_2 : Flat f
Z : Scheme
⊢ Presieve.IsSheafFor (Functor.obj yoneda Z) (Presieve.singleton f)

Tactic:
exact (GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable _).isSheafFor _
    (Precoverage.generate_mem_toGrothendieck f.singleton_mem_fppfPrecoverage)

Premises used: AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage, CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable, CategoryTheory.Presieve.IsSheaf.isSheafFor
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
⊢ HasPullback g f

Tactic:
haveI : HasPullback g f := hasPullback_symmetry f g
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
obtain : ∀ (a : ↥(pullback g f)) (ha : (pullback.fst g f) a = y), ∃ (a : ↥(pullback f g)), (pullback.snd f g) a = y
⊢ ∃ (a : ↥(pullback f g)), (pullback.snd f g) a = y

Tactic:
obtain ⟨a, ha⟩ := exists_preimage_fst_triplet_of_prop hf y x h.symm

Premises used: Eq.symm, AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
h₁ : (pullback.snd f g) ((Iso.inv (pullbackSymmetry f g)) a : ↥(pullback f g)) = y
⊢ ∃ (a : ↥(pullback f g)), (pullback.snd f g) a = y

Tactic:
use (pullbackSymmetry f g).inv a

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
h₁ : (CategoryStruct.comp (Y := pullback f g) (Iso.inv (pullbackSymmetry f g)) (pullback.snd f g)) a = y
h₂ h₃ h₄ h₅ : (pullback.fst g f) a = y
⊢ (pullback.snd f g) ((Iso.inv (pullbackSymmetry f g)) a : ↥(pullback f g)) = y

Tactic:
rwa [← Scheme.Hom.comp_apply, pullbackSymmetry_inv_comp_snd]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
rw :
  ∃ (a : ↥(pullback f g)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
          (a : ↥(pullback f g)) → ↥X)
        a =
      x
⊢ ∃ (a : ↥(pullback f g)), (pullback.fst f g) a = x

Tactic:
rw [← show _ = (pullback.fst _ _ : pullback f g ⟶ _).base from
        PreservesPullback.iso_hom_fst Scheme.forgetToTop f g]

Premises used: CategoryTheory.Limits.PreservesPullback.iso_hom_fst, AlgebraicGeometry.Scheme.forgetToTop
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
rw : Membership.mem (γ := Set ↥X) {x : ↥X | ∃ (y : ↥Y), Eq (α := ↥S) (f x : ↥S) (g y : ↥S)} x
⊢ Membership.mem (γ := Set ↥X)
    (Set.range (ι := (↑(pullback f.base g.base) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X))
    x

Tactic:
rw [TopCat.pullback_fst_range f.base g.base]

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopCat.pullback_fst_range
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
w : ↥Y
h₁ : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
⊢ Membership.mem (γ := Set ↥X) {x : ↥X | ∃ (y : ↥Y), Eq (α := ↥S) (f x : ↥S) (g y : ↥S)} x

Tactic:
use y
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
⊢ Membership.mem (γ := Set ↥X)
    (Set.range (ι := (↑(pullback f.base g.base) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X))
    x

Tactic:
have : x ∈ Set.range (pullback.fst f.base g.base) := by
      rw [TopCat.pullback_fst_range f.base g.base]
      use y
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
this :
  Membership.mem (γ := Set ↥X)
    (Set.range (ι := (↑(pullback f.base g.base) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X))
    x
obtain :
  ∀ (a : (↑(pullback f.base g.base) : Type u_1))
    (ha :
      (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := pullback f.base g.base) (pullback.fst f.base g.base) :
            (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X)
          a =
        x),
    ∃ (a : ↥(pullback f g)),
      (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := (↑(pullback f g).toPresheafedSpace : TopCat))
              (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
                (Iso.hom (PreservesPullback.iso forgetToTop f g))
                (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
            (a : ↥(pullback f g)) → ↥X)
          a =
        x
⊢ ∃ (a : ↥(pullback f g)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
          (a : ↥(pullback f g)) → ↥X)
        a =
      x

Tactic:
obtain ⟨a, ha⟩ := this
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
a : (↑(pullback f.base g.base) : Type u_1)
ha :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := pullback f.base g.base) (pullback.fst f.base g.base) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X)
      a =
    x
h₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat))
          (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
            (Iso.hom (PreservesPullback.iso forgetToTop f g)) (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
        (a : ↥(pullback f g)) → ↥X)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := pullback (forgetToTop.map f) (forgetToTop.map g)) (Y :=
              forgetToTop.obj (pullback f g)) (Iso.inv (PreservesPullback.iso forgetToTop f g)) :
            (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) →
              (↑(forgetToTop.obj (pullback f g)) : Type u_1))
          a :
        (↑(forgetToTop.obj (pullback f g)) : Type u_1)) =
    x
⊢ ∃ (a : ↥(pullback f g)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
          (a : ↥(pullback f g)) → ↥X)
        a =
      x

Tactic:
use (PreservesPullback.iso Scheme.forgetToTop f g).inv a

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.PreservesPullback.iso, AlgebraicGeometry.Scheme.forgetToTop, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
a : (↑(pullback f.base g.base) : Type u_1)
ha :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := pullback f.base g.base) (pullback.fst f.base g.base) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X)
      a =
    x
h₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := pullback (forgetToTop.map f) (forgetToTop.map g))
          (CategoryStruct.comp (Y := (↑(pullback f g).toPresheafedSpace : TopCat))
            (Iso.inv (PreservesPullback.iso forgetToTop f g))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g)))) :
        (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) → ↥X)
      a =
    x
h₂ h₃ h₄ h₅ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := pullback (forgetToTop.map f) (forgetToTop.map g))
          (pullback.fst (forgetToTop.map f) (forgetToTop.map g)) :
        (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) → ↥X)
      a =
    x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat))
          (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
            (Iso.hom (PreservesPullback.iso forgetToTop f g)) (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
        (a : ↥(pullback f g)) → ↥X)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := pullback (forgetToTop.map f) (forgetToTop.map g)) (Y :=
              forgetToTop.obj (pullback f g)) (Iso.inv (PreservesPullback.iso forgetToTop f g)) :
            (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) →
              (↑(forgetToTop.obj (pullback f g)) : Type u_1))
          a :
        (↑(forgetToTop.obj (pullback f g)) : Type u_1)) =
    x

Tactic:
rwa [← TopCat.comp_app, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, TopCat.comp_app
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
simp_rw :
  Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    Presieve.ofArrows X f ∈ (Precoverage.comap forget Types.jointlySurjectivePrecoverage).coverings S ∧
      ∀ (i : ι), P (f i)
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    (∀ (x : ↥S), ∃ (i : ι), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥(X i)) ⇑(f i)) x) ∧ ∀ (i : ι), P (f i)

Tactic:
simp_rw [← Scheme.forget_map', ← Scheme.forget_obj,
    ← Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff]

Premises used: AlgebraicGeometry.Scheme.forget_obj, CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff, AlgebraicGeometry.Scheme.forget_map'
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    Presieve.ofArrows X f ∈ (Precoverage.comap forget Types.jointlySurjectivePrecoverage).coverings S ∧
      ∀ (i : ι), P (f i)

Tactic:
⟨fun hmem ↦ ⟨hmem.1, fun i ↦ hmem.2 ⟨i⟩⟩, fun h ↦ ⟨h.1, fun {Y} g ⟨i⟩ ↦ h.2 i⟩⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, And.right, And.left, And.intro, Iff.intro, _private.0.AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff.match_3
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔
    Presieve.ofArrows X f ∈ (Precoverage.comap forget Types.jointlySurjectivePrecoverage).coverings S ∧
      ∀ (i : ι), P (f i)

Tactic:
exact ⟨fun hmem ↦ ⟨hmem.1, fun i ↦ hmem.2 ⟨i⟩⟩, fun h ↦ ⟨h.1, fun {Y} g ⟨i⟩ ↦ h.2 i⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
rw :
  ((∀ (x : ↥S), ∃ (i : PUnit.{1}), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) x) ∧ ∀ (i : PUnit.{1}), P f) ↔
    Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f
⊢ Presieve.singleton f ∈ (precoverage P).coverings S ↔ Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f

Tactic:
rw [← Presieve.ofArrows_pUnit.{_, _, 0}, ofArrows_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ ((∀ (x : ↥S), ∃ (i : PUnit.{1}), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) x) ∧ ∀ (i : PUnit.{1}), P f) ↔
    Function.Surjective (α := ↥X) (β := ↥S) ⇑f ∧ P f

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : IsEmpty.{u + 1} ↥X
⊢ ⊥ ∈ (precoverage P).coverings X

Tactic:
⟨fun x ↦ ‹IsEmpty X›.elim x, P.bot_mem_precoverage _⟩

Premises used: Set.Mem, IsEmpty.elim, setOf, CategoryTheory.MorphismProperty.bot_mem_precoverage, Set.inter, And.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty
Goal:
P Q : MorphismProperty Scheme
h : P ≤ Q
grw : jointlySurjectivePrecoverage ⊓ P.precoverage ≤ precoverage Q
grw₁ : jointlySurjectivePrecoverage ⊓ P.precoverage ≤ jointlySurjectivePrecoverage ⊓ Q.precoverage
grw₂ grw₃ : jointlySurjectivePrecoverage ⊓ Q.precoverage ≤ jointlySurjectivePrecoverage ⊓ Q.precoverage
⊢ precoverage P ≤ precoverage Q

Tactic:
grw [precoverage, precoverage, MorphismProperty.precoverage_monotone h]

Premises used: CategoryTheory.MorphismProperty.precoverage_monotone, AlgebraicGeometry.Scheme.precoverage