awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
apply :
  ∃ (e :
    Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
        ((fun (t : ↥(pullback f g)) ↦
            (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) (Triplet.ofPoint t) (SpecOfPoint t) :
              (T : Triplet f g) × ↥(Spec T.tensor)))
          ((fun (T : (T : Triplet f g) × ↥(Spec T.tensor)) ↦
              (T.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)).SpecTensorTo
                  (T.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) :
                ↥(pullback f g)))
            (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p))) =
      Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
        (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)),
    Eq (α :=
      ↥(Spec
          (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
              (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)).tensor))
      ((Spec.map (Triplet.tensorCongr e).inv)
          (Sigma.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
            ((fun (t : ↥(pullback f g)) ↦
                (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) (Triplet.ofPoint t) (SpecOfPoint t) :
                  (T : Triplet f g) × ↥(Spec T.tensor)))
              ((fun (T : (T : Triplet f g) × ↥(Spec T.tensor)) ↦
                  (T.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)).SpecTensorTo
                      (T.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) :
                    ↥(pullback f g)))
                (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)))) :
        ↥(Spec
            (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
                (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)).tensor))
      (Sigma.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
          (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p) :
        ↥(Spec
            (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
                (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)).tensor))
⊢ Eq (α := (T : Triplet f g) × ↥(Spec T.tensor))
    ((fun (t : ↥(pullback f g)) ↦
        (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) (Triplet.ofPoint t) (SpecOfPoint t) :
          (T : Triplet f g) × ↥(Spec T.tensor)))
      ((fun (T : (T : Triplet f g) × ↥(Spec T.tensor)) ↦
          (T.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)).SpecTensorTo
              (T.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) :
            ↥(pullback f g)))
        (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)))
    (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)

Tactic:
apply carrierEquiv_eq_iff.mpr

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Eq (α := ↥(Spec ((pullback f g).residueField (T.SpecTensorTo p))))
    ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p)) ⊥) ⊥

Tactic:
have : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) (⊥ : PrimeSpectrum _) =
        (⊥ : PrimeSpectrum _) :=
      (PrimeSpectrum.instUnique).uniq _
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
this :
  Eq (α := ↥(Spec ((pullback f g).residueField (T.SpecTensorTo p))))
    ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p)) ⊥) ⊥
h :
  ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫ Spec.map (ofPointTensor (T.SpecTensorTo p))) ≫
        Spec.map (Triplet.tensorCongr ⋯).hom)
      ⊥ =
    p
⊢ Eq (α :=
    ↥(Spec
        (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
            (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)).tensor))
    ((Spec.map (Triplet.tensorCongr ⋯).inv)
        (Sigma.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
          ((fun (t : ↥(pullback f g)) ↦
              (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) (Triplet.ofPoint t) (SpecOfPoint t) :
                (T : Triplet f g) × ↥(Spec T.tensor)))
            ((fun (T : (T : Triplet f g) × ↥(Spec T.tensor)) ↦
                (T.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)).SpecTensorTo
                    (T.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))) :
                  ↥(pullback f g)))
              (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)))) :
      ↥(Spec
          (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
              (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)).tensor))
    (Sigma.snd (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
        (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p) :
      ↥(Spec
          (Sigma.fst (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor))
              (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p)).tensor))

Tactic:
simp only [SpecOfPoint, Triplet.tensorCongr_inv, ← this, ← Scheme.Hom.comp_apply,
      ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Pullback.SpecOfPoint, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_inv
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
this :
  Eq (α := ↥(Spec ((pullback f g).residueField (T.SpecTensorTo p))))
    ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p)) ⊥) ⊥
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫ Spec.map (ofPointTensor (T.SpecTensorTo p))) ≫
        Spec.map (Triplet.tensorCongr ⋯).hom)
      ⊥ =
    p

Tactic:
simp [Triplet.Spec_ofPointTensor_SpecTensorTo]

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.Spec_ofPointTensor_SpecTensorTo
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.fst f g)
      ((Equiv.symm carrierEquiv : (a : (T : Triplet f g) × ↥(Spec T.tensor)) → ↥(pullback f g))
          (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p) :
        ↥(pullback f g)) =
    T.x

Tactic:
simp [carrierEquiv]

Premises used: AlgebraicGeometry.Scheme.Pullback.carrierEquiv
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.snd f g)
      ((Equiv.symm carrierEquiv : (a : (T : Triplet f g) × ↥(Spec T.tensor)) → ↥(pullback f g))
          (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T p) :
        ↥(pullback f g)) =
    T.y

Tactic:
simp [carrierEquiv]

Premises used: AlgebraicGeometry.Scheme.Pullback.carrierEquiv
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (pullback.fst f g)
        ((Equiv.symm carrierEquiv : (a : (T : Triplet f g) × ↥(Spec T.tensor)) → ↥(pullback f g))
            (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T (Nonempty.some ⋯)) :
          ↥(pullback f g)) =
      T.x ∧
    (pullback.snd f g)
        ((Equiv.symm carrierEquiv : (a : (T : Triplet f g) × ↥(Spec T.tensor)) → ↥(pullback f g))
            (Sigma.mk (β := fun (T : Triplet f g) ↦ ↥(Spec T.tensor)) T (Nonempty.some ⋯)) :
          ↥(pullback f g)) =
      T.y

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
⊢ ∃ (z : ↥(pullback f g)), (pullback.fst f g) z = x ∧ (pullback.snd f g) z = y

Tactic:
(Pullback.Triplet.mk' x y h).exists_preimage

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.mk', AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsEmpty.{u + 1} ↥(pullback f g) ↔ Disjoint (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)

Tactic:
⟨?_, Scheme.isEmpty_pullback f g⟩

Premises used: Iff.intro, AlgebraicGeometry.Scheme.isEmpty_pullback
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
refine : IsEmpty.{u + 1} ↥(pullback f g) → Disjoint (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ IsEmpty.{u + 1} ↥(pullback f g) ↔ Disjoint (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)

Tactic:
refine ⟨?_, Scheme.isEmpty_pullback f g⟩
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
rw :
  IsEmpty.{u + 1} ↥(pullback f g) →
    ∀ ⦃a : ↥S⦄,
      Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) a →
        ∀ ⦃b : ↥S⦄, Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) b → a ≠ b
⊢ IsEmpty.{u + 1} ↥(pullback f g) → Disjoint (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)

Tactic:
rw [Set.disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
contrapose! :
  (∃ (a : ↥S),
      Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) a ∧
        ∃ (b : ↥S), Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) b ∧ a = b) →
    Nonempty.{u + 1} ↥(pullback f g)
⊢ IsEmpty.{u + 1} ↥(pullback f g) →
    ∀ ⦃a : ↥S⦄,
      Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) a →
        ∀ ⦃b : ↥S⦄, Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) b → a ≠ b

Tactic:
contrapose!
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
y : ↥Y
e : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
obtain : ∀ (z : ↥(pullback f g)), Nonempty.{u + 1} ↥(pullback f g)
⊢ Nonempty.{u + 1} ↥(pullback f g)

Tactic:
obtain ⟨z, -⟩ := exists_preimage_pullback x y e

Premises used: AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
y : ↥Y
e : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
z : ↥(pullback f g)
⊢ Nonempty.{u + 1} ↥(pullback f g)

Tactic:
⟨z⟩

Premises used: Nonempty.intro
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
y : ↥Y
e : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
z : ↥(pullback f g)
⊢ Nonempty.{u + 1} ↥(pullback f g)

Tactic:
exact ⟨z⟩
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : Nonempty.{u + 1} ↥X
inst_1 : Nonempty.{u + 1} ↥Y
inst_2 : Subsingleton.{u + 1} ↥S
⊢ Nonempty.{u + 1} ↥S

Tactic:
have : Nonempty S := .map f ‹_›
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : Nonempty.{u + 1} ↥X
inst_1 : Nonempty.{u + 1} ↥Y
inst_2 : Subsingleton.{u + 1} ↥S
this : Nonempty.{u + 1} ↥S
rw :
  ∃ (x : ↥S),
    Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) x ∧ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) x
⊢ Nonempty.{u + 1} ↥(pullback f g)

Tactic:
rw [← not_isEmpty_iff, AlgebraicGeometry.Scheme.isEmpty_pullback_iff, Set.not_disjoint_iff]

Premises used: AlgebraicGeometry.Scheme.isEmpty_pullback_iff, Set.not_disjoint_iff, not_isEmpty_iff
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : Nonempty.{u + 1} ↥X
inst_1 : Nonempty.{u + 1} ↥Y
inst_2 : Subsingleton.{u + 1} ↥S
this : Nonempty.{u + 1} ↥S
⊢ ∃ (x : ↥S),
    Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) x ∧ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) x

Tactic:
⟨Nonempty.some ‹_›, Function.surjective_to_subsingleton _ _,
    Function.surjective_to_subsingleton _ _⟩

Premises used: Nonempty.some, Function.surjective_to_subsingleton, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : Nonempty.{u + 1} ↥X
inst_1 : Nonempty.{u + 1} ↥Y
inst_2 : Subsingleton.{u + 1} ↥S
this : Nonempty.{u + 1} ↥S
⊢ ∃ (x : ↥S),
    Membership.mem (γ := Set ↥S) (Set.range (ι := ↥X) ⇑f) x ∧ Membership.mem (γ := Set ↥S) (Set.range (ι := ↥Y) ⇑g) x

Tactic:
exact ⟨Nonempty.some ‹_›, Function.surjective_to_subsingleton _ _,
    Function.surjective_to_subsingleton _ _⟩
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h :
  ∀ (x : ↥X),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x ↔
      Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) x
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g))
    (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x ↔
    Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) x

Tactic:
⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Membership.mem, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', _private.0.AlgebraicGeometry.Scheme.Pullback.range_fst.match_1, CategoryTheory.Limits.pullback.fst, Iff.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
h :
  Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x →
    Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) x
h₁ :
  Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) x →
    ∀ (y : ↥Y) (hy : Eq (α := ↥S) (g y : ↥S) (f x : ↥S)),
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x ↔
    Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) x

Tactic:
refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
h : ∃ (y : ↥Y), Eq (α := ↥S) (g y : ↥S) ((pullback.snd f g ≫ g) a : ↥S)
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g))
    ((pullback.fst f g) a : ↥X)

Tactic:
simp only [Set.mem_preimage, Set.mem_range, ← Scheme.Hom.comp_apply, pullback.condition]

Premises used: Set.mem_range, AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.pullback.condition, Set.mem_preimage
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
⊢ ∃ (y : ↥Y), Eq (α := ↥S) (g y : ↥S) ((pullback.snd f g ≫ g) a : ↥S)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
h_1 : Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) x
y : ↥Y
hy : Eq (α := ↥S) (g y : ↥S) (f x : ↥S)
h :
  ∀ (a : ↥(pullback f g))
    (ha : (pullback.fst f g) a = (Triplet.mk' x y ⋯).x ∧ (pullback.snd f g) a = (Triplet.mk' x y ⋯).y),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x

Tactic:
obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' x y hy.symm)

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.mk', AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
h_1 : Membership.mem (γ := Set ↥X) (Set.preimage (β := ↥S) (⇑f) (Set.range (ι := ↥Y) ⇑g)) x
y : ↥Y
hy : Eq (α := ↥S) (g y : ↥S) (f x : ↥S)
a : ↥(pullback f g)
ha : (pullback.fst f g) a = (Triplet.mk' x y ⋯).x ∧ (pullback.snd f g) a = (Triplet.mk' x y ⋯).y
w : ↥(pullback f g)
h : (pullback.fst f g) a = x
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g)) x

Tactic:
use a, ha.left

Premises used: And.left
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h :
  ∀ (x : ↥Y),
    Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x ↔
      Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f)) x
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g))
    (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
⊢ Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x ↔
    Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f)) x

Tactic:
⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩

Premises used: _private.0.AlgebraicGeometry.Scheme.Pullback.range_snd.match_1, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, Membership.mem, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Iff.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
h :
  Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x →
    Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f)) x
h₁ :
  Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f)) x →
    ∀ (y : ↥X) (hy : Eq (α := ↥S) (f y : ↥S) (g x : ↥S)),
      Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x
⊢ Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x ↔
    Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f)) x

Tactic:
refine ⟨?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
h : ∃ (y : ↥X), Eq (α := ↥S) (f y : ↥S) ((pullback.fst f g ≫ f) a : ↥S)
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f))
    ((pullback.snd f g) a : ↥Y)

Tactic:
simp only [Set.mem_preimage, Set.mem_range, ← Scheme.Hom.comp_apply, ← pullback.condition]

Premises used: Set.mem_range, AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.pullback.condition, Set.mem_preimage
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
⊢ ∃ (y : ↥X), Eq (α := ↥S) (f y : ↥S) ((pullback.fst f g ≫ f) a : ↥S)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
h_1 : Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f)) x
y : ↥X
hy : Eq (α := ↥S) (f y : ↥S) (g x : ↥S)
h :
  ∀ (a : ↥(pullback f g))
    (ha : (pullback.fst f g) a = (Triplet.mk' y x hy).x ∧ (pullback.snd f g) a = (Triplet.mk' y x hy).y),
    Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x
⊢ Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x

Tactic:
obtain ⟨a, ha⟩ := Triplet.exists_preimage (Triplet.mk' y x hy)

Premises used: AlgebraicGeometry.Scheme.Pullback.Triplet.mk', AlgebraicGeometry.Scheme.Pullback.Triplet.exists_preimage
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
h_1 : Membership.mem (γ := Set ↥Y) (Set.preimage (β := ↥S) (⇑g) (Set.range (ι := ↥X) ⇑f)) x
y : ↥X
hy : Eq (α := ↥S) (f y : ↥S) (g x : ↥S)
a : ↥(pullback f g)
ha : (pullback.fst f g) a = (Triplet.mk' y x hy).x ∧ (pullback.snd f g) a = (Triplet.mk' y x hy).y
w : ↥(pullback f g)
h : (pullback.snd f g) a = x
⊢ Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g)) x

Tactic:
use a, ha.right

Premises used: And.right
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Eq (α := Set ↥S) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)

Tactic:
simp [Set.range_comp, range_fst, Set.image_preimage_eq_range_inter]

Premises used: Set.range_comp, Set.image_preimage_eq_range_inter, AlgebraicGeometry.Scheme.Pullback.range_fst
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
rw :
  Eq (α := Set ↥S) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ rw₂ :
  Eq (α := Set ↥S) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g) (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥S) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)

Tactic:
rw [← pullback.condition, range_fst_comp]

Premises used: AlgebraicGeometry.Scheme.Pullback.range_fst_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst : Mono i₃
h :
  ∀ (z : ↥(pullback f' g')),
    Membership.mem (γ := Set ↥(pullback f' g'))
        (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z ↔
      Membership.mem (γ := Set ↥(pullback f' g'))
        (Set.preimage (β := ↥X') (⇑(pullback.fst f' g')) (Set.range (ι := ↥X) ⇑i₁) ∩
          Set.preimage (β := ↥Y') (⇑(pullback.snd f' g')) (Set.range (ι := ↥Y) ⇑i₂))
        z
⊢ Eq (α := Set ↥(pullback f' g')) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂))
    (Set.preimage (β := ↥X') (⇑(pullback.fst f' g')) (Set.range (ι := ↥X) ⇑i₁) ∩
      Set.preimage (β := ↥Y') (⇑(pullback.snd f' g')) (Set.range (ι := ↥Y) ⇑i₂))

Tactic:
ext z
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst : Mono i₃
z : ↥(pullback f' g')
h :
  Membership.mem (γ := Set ↥(pullback f' g'))
      (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z →
    Membership.mem (γ := Set ↥(pullback f' g'))
      (Set.preimage (β := ↥X') (⇑(pullback.fst f' g')) (Set.range (ι := ↥X) ⇑i₁) ∩
        Set.preimage (β := ↥Y') (⇑(pullback.snd f' g')) (Set.range (ι := ↥Y) ⇑i₂))
      z
h₁ :
  Membership.mem (γ := Set ↥(pullback f' g'))
      (Set.preimage (β := ↥X') (⇑(pullback.fst f' g')) (Set.range (ι := ↥X) ⇑i₁) ∩
        Set.preimage (β := ↥Y') (⇑(pullback.snd f' g')) (Set.range (ι := ↥Y) ⇑i₂))
      z →
    Membership.mem (γ := Set ↥(pullback f' g'))
      (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z
⊢ Membership.mem (γ := Set ↥(pullback f' g'))
      (Set.range (ι := ↥(pullback f g)) ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)) z ↔
    Membership.mem (γ := Set ↥(pullback f' g'))
      (Set.preimage (β := ↥X') (⇑(pullback.fst f' g')) (Set.range (ι := ↥X) ⇑i₁) ∩
        Set.preimage (β := ↥Y') (⇑(pullback.snd f' g')) (Set.range (ι := ↥Y) ⇑i₂))
      z

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.PullbackCarrier
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst : Mono i₃
t : ↥(pullback f g)
h :
  Membership.mem (α := ↥(pullback f' g')) (γ := Set ↥(pullback f' g'))
    (Set.preimage (β := ↥X') (⇑(pullback.fst f' g')) (Set.range (ι := ↥X) ⇑i₁))
    ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t : ↥(pullback f' g'))
h₁ :
  Membership.mem (α := ↥(pullback f' g')) (γ := Set ↥(pullback f' g'))
    (Set.preimage (β := ↥Y') (⇑(pullback.snd f' g')) (Set.range (ι := ↥Y) ⇑i₂))
    ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t : ↥(pullback f' g'))
⊢ Membership.mem (α := ↥(pullback f' g')) (γ := Set ↥(pullback f' g'))
    (Set.preimage (β := ↥X') (⇑(pullback.fst f' g')) (Set.range (ι := ↥X) ⇑i₁) ∩
      Set.preimage (β := ↥Y') (⇑(pullback.snd f' g')) (Set.range (ι := ↥Y) ⇑i₂))
    ((pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) t : ↥(pullback f' g'))

Tactic:
constructor