awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
h :
  (↑(Function.comp (β := (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) :
              (a : (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g))) →
                (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) →
                (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            z) :
        forget.obj X × forget.obj Y).1 =
    (↑x : forget.obj X × forget.obj Y).1
h₁ :
  (↑(Function.comp (β := (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) :
              (a : (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g))) →
                (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) →
                (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            z) :
        forget.obj X × forget.obj Y).2 =
    (↑x : forget.obj X × forget.obj Y).2
⊢ Function.comp (β := (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) :
        (a : (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g))) →
          (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) →
          (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
      z =
    x

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (forget.map f) (forget.map g)) :
        (a : pullback (forget.map f) (forget.map g)) → forget.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
            (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
          z :
        pullback (forget.map f) (forget.map g)) =
    (↑x : forget.obj X × forget.obj Y).1
⊢ (↑(Function.comp (β := (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) :
              (a : (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g))) →
                (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) →
                (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            z) :
        forget.obj X × forget.obj Y).1 =
    (↑x : forget.obj X × forget.obj Y).1

Tactic:
simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_fst]

Premises used: CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst, Function.comp_apply
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := pullback (forget.map f) (forget.map g)) (pullbackComparison forget f g)
            (pullback.fst (forget.map f) (forget.map g))) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj X))
      z =
    (↑x : forget.obj X × forget.obj Y).1
h₁ h₂ h₃ h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (pullback.fst f g)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj X))
      z =
    (↑x : forget.obj X × forget.obj Y).1
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.fst (forget.map f) (forget.map g)) :
        (a : pullback (forget.map f) (forget.map g)) → forget.obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
            (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
          z :
        pullback (forget.map f) (forget.map g)) =
    (↑x : forget.obj X × forget.obj Y).1

Tactic:
rwa [← types_comp_apply (g := pullback.fst _ _), pullbackComparison_comp_fst]

Premises used: CategoryTheory.Limits.pullback.fst, CategoryTheory.Limits.pullbackComparison_comp_fst, CategoryTheory.types_comp_apply
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.snd (forget.map f) (forget.map g)) :
        (a : pullback (forget.map f) (forget.map g)) → forget.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
            (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
          z :
        pullback (forget.map f) (forget.map g)) =
    (↑x : forget.obj X × forget.obj Y).2
⊢ (↑(Function.comp (β := (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom) :
              (a : (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g))) →
                (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g)))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) →
                (fun (X : Type u) ↦ X) (pullback (forget.map f) (forget.map g)))
            z) :
        forget.obj X × forget.obj Y).2 =
    (↑x : forget.obj X × forget.obj Y).2

Tactic:
simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_snd]

Premises used: CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd, Function.comp_apply
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : (fun (X : Type u) ↦ X) (Types.PullbackObj (forget.map f) (forget.map g))
z : ↥(pullback f g)
h1 : (pullback.fst f g) z = (↑x : forget.obj X × forget.obj Y).1
h2 : (pullback.snd f g) z = (↑x : forget.obj X × forget.obj Y).2
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := pullback (forget.map f) (forget.map g)) (pullbackComparison forget f g)
            (pullback.snd (forget.map f) (forget.map g))) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj Y))
      z =
    (↑x : forget.obj X × forget.obj Y).2
h₁ h₂ h₃ h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (pullback.snd f g)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj (pullback f g))) → (fun (X : Type u) ↦ X) (forget.obj Y))
      z =
    (↑x : forget.obj X × forget.obj Y).2
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (pullback.snd (forget.map f) (forget.map g)) :
        (a : pullback (forget.map f) (forget.map g)) → forget.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison forget f g) :
            (a : forget.obj (pullback f g)) → pullback (forget.map f) (forget.map g))
          z :
        pullback (forget.map f) (forget.map g)) =
    (↑x : forget.obj X × forget.obj Y).2

Tactic:
rwa [← types_comp_apply (g := pullback.snd _ _), pullbackComparison_comp_snd]

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullbackComparison_comp_snd, CategoryTheory.types_comp_apply
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi (X := forgetToTop.obj (pullback f g)) (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
    (pullbackComparison forgetToTop f g)

Tactic:
(CategoryTheory.forget TopCat).epi_of_epi_map ?_

Premises used: CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map, TopCat
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
refine :
  Epi (X :=
    Functor.obj
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (forgetToTop.obj (pullback f g)))
    (Y :=
    Functor.obj
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (pullback (forgetToTop.map f) (forgetToTop.map g)))
    (CategoryTheory.Functor.map
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (pullbackComparison forgetToTop f g))
⊢ Epi (X := forgetToTop.obj (pullback f g)) (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
    (pullbackComparison forgetToTop f g)

Tactic:
refine (CategoryTheory.forget TopCat).epi_of_epi_map ?_

Premises used: CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map, TopCat
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
rw :
  Function.Surjective (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
          TopCat.carrier))
        (forgetToTop.obj (pullback f g))))
    (β :=
    (fun (X : Type u) ↦ X)
      (pullback (X :=
        Functor.obj
          (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
            TopCat.carrier))
          (forgetToTop.obj X))
        (CategoryTheory.Functor.map
          (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
            TopCat.carrier))
          (forgetToTop.map f))
        (CategoryTheory.Functor.map
          (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
            TopCat.carrier))
          (forgetToTop.map g))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (pullbackComparison
            (forgetToTop ⋙
              CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier))
            f g)) :
      (a : (fun (X : Type u) ↦ X) ((CategoryTheory.forget TopCat).obj (forgetToTop.obj (pullback f g)))) →
        (fun (X : Type u) ↦ X)
          (pullback ((CategoryTheory.forget TopCat).map (forgetToTop.map f))
            ((CategoryTheory.forget TopCat).map (forgetToTop.map g))))
⊢ Epi (X :=
    Functor.obj
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (forgetToTop.obj (pullback f g)))
    (Y :=
    Functor.obj
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (pullback (forgetToTop.map f) (forgetToTop.map g)))
    (CategoryTheory.Functor.map
      (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
        TopCat.carrier))
      (pullbackComparison forgetToTop f g))

Tactic:
rw [← CategoryTheory.epi_comp_iff_of_isIso _
    (pullbackComparison (CategoryTheory.forget TopCat) (forgetToTop.map f) (forgetToTop.map g)),
    ← _root_.CategoryTheory.Limits.pullbackComparison_comp, epi_iff_surjective]

Premises used: CategoryTheory.epi_iff_surjective, AlgebraicGeometry.Scheme.forgetToTop, CategoryTheory.Functor.map, CategoryTheory.epi_comp_iff_of_isIso, CategoryTheory.forget, CategoryTheory.Limits.pullbackComparison_comp, TopCat, CategoryTheory.Limits.pullbackComparison
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Function.Surjective (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
          TopCat.carrier))
        (forgetToTop.obj (pullback f g))))
    (β :=
    (fun (X : Type u) ↦ X)
      (pullback (X :=
        Functor.obj
          (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
            TopCat.carrier))
          (forgetToTop.obj X))
        (CategoryTheory.Functor.map
          (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
            TopCat.carrier))
          (forgetToTop.map f))
        (CategoryTheory.Functor.map
          (CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
            TopCat.carrier))
          (forgetToTop.map g))))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (pullbackComparison
            (forgetToTop ⋙
              CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier))
            f g)) :
      (a : (fun (X : Type u) ↦ X) ((CategoryTheory.forget TopCat).obj (forgetToTop.obj (pullback f g)))) →
        (fun (X : Type u) ↦ X)
          (pullback ((CategoryTheory.forget TopCat).map (forgetToTop.map f))
            ((CategoryTheory.forget TopCat).map (forgetToTop.map g))))

Tactic:
apply Scheme.pullbackComparison_forget_surjective _ _

Premises used: AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
x : ↥X
y : ↥Y
hxy : Eq (α := ↥Z) (f x : ↥Z) (g y : ↥Z)
e : P ≅ pullback f g := h.isoPullback
obtain :
  ∀ (z : ↥(pullback f g)) (hzl : (pullback.fst f g) z = x) (hzr : (pullback.snd f g) z = y),
    ∃ (p : ↥P), fst p = x ∧ snd p = y
⊢ ∃ (p : ↥P), fst p = x ∧ snd p = y

Tactic:
obtain ⟨z, hzl, hzr⟩ := AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback x y hxy

Premises used: AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
x : ↥X
y : ↥Y
hxy : Eq (α := ↥Z) (f x : ↥Z) (g y : ↥Z)
e : P ≅ pullback f g := h.isoPullback
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
h₁ : fst ((Iso.inv h.isoPullback) z : ↥P) = x ∧ snd ((Iso.inv h.isoPullback) z : ↥P) = y
⊢ ∃ (p : ↥P), fst p = x ∧ snd p = y

Tactic:
use h.isoPullback.inv.base z

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.IsPullback.isoPullback, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
x : ↥X
y : ↥Y
hxy : Eq (α := ↥Z) (f x : ↥Z) (g y : ↥Z)
e : P ≅ pullback f g := h.isoPullback
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ fst ((Iso.inv h.isoPullback) z : ↥P) = x ∧ snd ((Iso.inv h.isoPullback) z : ↥P) = y

Tactic:
simp [← Scheme.Hom.comp_apply, hzl, hzr]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ Eq (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))

Tactic:
subset_antisymm ?_ (fun x hx ↦ ?_)

Premises used: subset_antisymm
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
refine_1 : Subset (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))
refine_2 :
  ∀ (x : ↥Y) (hx : Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s)) x),
    Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
⊢ Eq (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))

Tactic:
refine subset_antisymm ?_ (fun x hx ↦ ?_)

Premises used: subset_antisymm
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
refine_1 : Subset (α := Set ↥P) (⇑fst ⁻¹' s) (Set.preimage (β := ↥Z) (⇑(fst ≫ f)) (⇑f '' s))
⊢ Subset (α := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s))

Tactic:
rw [Set.image_subset_iff, ← Set.preimage_comp, ← TopCat.coe_comp, ← Hom.comp_base, ← h.1.1]

Premises used: Set.preimage_comp, CategoryTheory.IsPullback.toCommSq, Set.image_subset_iff, CategoryTheory.CommSq.w, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
refine_1 : Subset (α := Set ↥Z) (Set.image (α := ↥X) (⇑f) (Set.image (α := ↥P) (⇑fst) (⇑fst ⁻¹' s))) (⇑f '' s)
⊢ Subset (α := Set ↥P) (⇑fst ⁻¹' s) (Set.preimage (β := ↥Z) (⇑(fst ≫ f)) (⇑f '' s))

Tactic:
rw [Hom.comp_base, TopCat.coe_comp, ← Set.image_subset_iff, Set.image_comp]

Premises used: Set.image_comp, Set.image_subset_iff, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ Subset (α := Set ↥Z) (Set.image (α := ↥X) (⇑f) (Set.image (α := ↥P) (⇑fst) (⇑fst ⁻¹' s))) (⇑f '' s)

Tactic:
Set.image_mono (Set.image_preimage_subset _ _)

Premises used: Set.image_mono, Set.image_preimage_subset
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
⊢ Subset (α := Set ↥Z) (Set.image (α := ↥X) (⇑f) (Set.image (α := ↥P) (⇑fst) (⇑fst ⁻¹' s))) (⇑f '' s)

Tactic:
exact Set.image_mono (Set.image_preimage_subset _ _)

Premises used: Set.image_mono, Set.image_preimage_subset
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
hx : Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥Z) (⇑g) (⇑f '' s)) x
refine_2 :
  ∀ (y : ↥X) (hy : y ∈ s) (heq : Eq (α := ↥Z) (f y : ↥Z) (g x : ↥Z)),
    Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
⊢ Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x

Tactic:
obtain ⟨y, hy, heq⟩ := hx
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
y : ↥X
hy : y ∈ s
heq : Eq (α := ↥Z) (f y : ↥Z) (g x : ↥Z)
refine_2 :
  ∀ (o : ↥P) (hl : fst o = y) (hr : snd o = x), Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x
⊢ Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x

Tactic:
obtain ⟨o, hl, hr⟩ := exists_preimage_of_isPullback h y x heq

Premises used: AlgebraicGeometry.Scheme.exists_preimage_of_isPullback
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
y : ↥X
hy : y ∈ s
heq : Eq (α := ↥Z) (f y : ↥Z) (g x : ↥Z)
o : ↥P
hl : fst o = y
hr : snd o = x
h₁ : Membership.mem (γ := Set ↥P) (⇑fst ⁻¹' s) o ∧ snd o = x
⊢ Membership.mem (γ := Set ↥Y) (Set.image (α := ↥P) (⇑snd) (⇑fst ⁻¹' s)) x

Tactic:
use o
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
y : ↥X
hy : y ∈ s
heq : Eq (α := ↥Z) (f y : ↥Z) (g x : ↥Z)
o : ↥P
hl : fst o = y
hr : snd o = x
⊢ Membership.mem (γ := Set ↥P) (⇑fst ⁻¹' s) o ∧ snd o = x

Tactic:
simpa [hl, hr]
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
⊢ MorphismProperty.IsStableUnderBaseChange @Surjective

Tactic:
.mk' ?_

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk'
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
refine :
  ∀ (X Y S : Scheme.{u_1}) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Surjective g → Surjective (X := pullback f g) (pullback.fst f g)
⊢ MorphismProperty.IsStableUnderBaseChange @Surjective

Tactic:
refine .mk' ?_
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : HasPullback f g
hg : Surjective g
simp :
  ∀ (hg : Eq (α := Set ↥S) (Set.range (ι := ↥Y) ⇑g) Set.univ),
    Eq (α := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) Set.univ
⊢ Surjective (X := pullback f g) (pullback.fst f g)

Tactic:
simp only [surjective_iff, ← Set.range_eq_univ, Scheme.Pullback.range_fst] at hg ⊢

Premises used: Set.range_eq_univ, AlgebraicGeometry.surjective_iff, AlgebraicGeometry.Scheme.Pullback.range_fst
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : HasPullback f g
hg : Eq (α := Set ↥S) (Set.range (ι := ↥Y) ⇑g) Set.univ
rw : Eq (α := Set ↥X) (Set.preimage (β := ↥S) (⇑f) Set.univ) Set.univ
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set ↥X) Set.univ Set.univ
⊢ Eq (α := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) Set.univ

Tactic:
rw [hg, Set.preimage_univ]

Premises used: Set.preimage_univ
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : Surjective g
⊢ Surjective (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst _ _ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : Surjective f
⊢ Surjective (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd _ _ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
⊢ HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g

Tactic:
have : HasPullback (pullback.snd _ _ ≫ 𝒰.f i ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f j) (𝒰.f i) (𝒰.f i ≫ f) g
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this : HasPullback (X := pullback (𝒰.f j) (𝒰.f i)) (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
⊢ HasPullback (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g

Tactic:
have : HasPullback (pullback.snd _ _ ≫ 𝒰.f j ≫ f) g :=
    hasPullback_assoc_symm (𝒰.f i) (𝒰.f j) (𝒰.f j ≫ f) g